Non-singular subspaces are locally closed submanifolds

Hironaka's simple points [Hir64, p. 121]: "by means of the Jacobian criterion and the implicit function theorem", a point x of an analytic K-space X is simple iff a neighbourhood of x in X is isomorphic to an open subset G of some K^d with its sheaf of analytic functions. For the closed analytic subspace X of the manifold M defined by an ideal sheaf J (IsNonsingular: every point of the support has a regular local ring 𝒪_{M,x}/J_x) this is the dictionary isNonsingular_iff: near every point of its support, J is generated by part of the coordinates of a chart adapted to the support.

• (→): 𝒪_{M,x} is regular and 𝒪_{M,x}/J_x is regular, so J_x is generated by the first c members z_1, …, z_c of a regular system of parameters z_1, …, z_m of 𝒪_{M,x} ([TSPA, Tag 00NR]; IsRegularLocalRing.exists_span_eq_maximalIdeal_and_eq_span_image_lt). The classes of m generators of 𝔪_x in the m-dimensional residue-field vector space 𝔪_x/𝔪_x² are a basis (IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq), so the z_j have independent differentials (through the cotangent classes of Hironaka/Manifold/Chart/Cotangent.lean, after passing from the residue field to 𝕜), and the chart-extension theorem exists_chart_extending makes them the coordinates σ 1, …, σ c of a chart e at x. The stalk identity J_x = (z_{σ j}) spreads to a neighbourhood W of x by the finite generation of both sides (IdealSheaf.exists_opens_stalkIdeal_eq_span); on e|_W the support of J is the coordinate subspace {z_{σ j} = 0} — J_y ≠ ⊤ iff no z_{σ j} is a unit at y — so e|_W is adapted.
• (←): the coordinates z_{σ j} vanishing at x are part of a regular system of parameters of 𝒪_{M,x} (their classes are part of the basis of 𝔪_x/𝔪_x² formed by the centred coordinates), so 𝒪_{M,x}/(z_{σ j}) is regular (IsRegularLocalRing.quotient_span_range_of_linearIndependent; [TSPA, Tag 00NQ]).

The dictionary is how the non-singularity clause of the main theorems is verified for the centres and read off on analytic spaces (Hironaka/AnalyticSpace/SncBoundaryChart.lean).

From the residue field to 𝕜: cotangent classes of germs vanishing at the point

theorem Manifold.linearIndependent_cotangentClass_of_residueField {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {a : M} {ι : Type u_2} [Finite ι] (v : ι → ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (hv : ∀ (i : ι), v i ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (hli : LinearIndependent (IsLocalRing.ResidueField ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) fun (i : ι) => (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)).toCotangent ⟨v i, ⋯⟩) : LinearIndependent 𝕜 fun (i : ι) => cotangentClass E a (v i)

Germs vanishing at a whose classes in 𝔪_a/𝔪_a² are linearly independent over the residue field have linearly independent cotangent classes (cotangentClass) over 𝕜: the 𝕜-action factors through the residue field, on which 𝕜 → 𝒪_a → 𝒪_a/𝔪_a is injective.

The coordinates of a chart as a regular system of parameters

theorem Manifold.linearIndependent_toCotangent_coord_sub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) : LinearIndependent (IsLocalRing.ResidueField ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) fun (i : Fin n) => (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)).toCotangent ⟨coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i)), ⋯⟩

The classes of the centred coordinates z_i − z_i(a) form a basis of 𝔪_a/𝔪_a² over the residue field (they generate 𝔪_a, and dim 𝒪_{M,a} = n).

theorem Manifold.linearIndependent_toCotangent_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {c : ℕ} (σ : Fin c ↪ Fin n) (h0 : ∀ (i : Fin c), ψ (↑φ a) (σ i) = 0) : LinearIndependent (IsLocalRing.ResidueField ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) fun (i : Fin c) => (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)).toCotangent ⟨coord E ψ φ hφ ha (σ i), ⋯⟩

The classes of coordinates vanishing at a are linearly independent over the residue field (a subfamily of the basis of the centred coordinates).

theorem Manifold.isRegularLocalRing_quotient_span_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {c : ℕ} (σ : Fin c ↪ Fin n) (h0 : ∀ (i : Fin c), ψ (↑φ a) (σ i) = 0) : IsRegularLocalRing (↑((structureSheaf 𝕜 E M).presheaf.stalk a) ⧸ Ideal.span (Set.range fun (i : Fin c) => coord E ψ φ hφ ha (σ i)))

The quotient of 𝒪_{M,a} by coordinates vanishing at a is a regular local ring ([TSPA, Tag 00NQ]).

The forward direction: a regular quotient stalk gives an adapted chart

theorem Manifold.exists_adaptedChart_of_isRegularLocalRing_quotient {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (J : IdealSheaf (structureSheaf 𝕜 E M)) {x : M} (hreg : IsRegularLocalRing (↑((structureSheaf 𝕜 E M).presheaf.stalk x) ⧸ J.stalkIdeal x)) : ∃ (c : ℕ) (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n) (hφ : IsAdaptedChart ψ J.support φ σ), x ∈ φ.source ∧ ∀ (y : M) (hy : y ∈ φ.source), J.stalkIdeal y = Ideal.span (Set.range fun (i : Fin c) => coord E ψ φ ⋯ hy (σ i))

At a point x where 𝒪_{M,x}/J_x is regular (so x lies in the support), there is a chart adapted to the support of J on whose source J is generated by the adapted coordinates ([Hir64, p. 121]; [TSPA, Tag 00NR], the chart-extension theorem and the spreading of the stalk identity).

The dictionary on bundled manifolds

theorem Manifold.isNonsingular_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (J : N.IdealSheaf) : J.IsNonsingular ↔ ∀ x ∈ IdealSheaf.support J, ∃ (c : ℕ) (φ : OpenPartialHomeomorph N.carrier E) (σ : Fin c ↪ Fin n) (hφ : IsAdaptedChart ψ (IdealSheaf.support J) φ σ), x ∈ φ.source ∧ ∀ (y : N.carrier) (hy : y ∈ φ.source), IdealSheaf.stalkIdeal J y = Ideal.span (Set.range fun (i : Fin c) => coord E ψ φ ⋯ hy (σ i))

Hironaka's simple points, by the Jacobian criterion and the implicit function theorem [Hir64, p. 121]: the subspace defined by J is non-singular iff, near every point of it, J is the ideal sheaf of a closed submanifold — for some codimension c and a chart adapted to the support, the stalks of J at every point of the chart's source are spanned by the adapted coordinates.