The Jacobian criterion at a point of a local model

Hironaka proves that simple points are manifold points "by means of jacobian criterion and the implicit function theorem" [Hir64, Ch. 0, §1, p. 121]. The Jacobian criterion, at a point z of the local model X = V(f₁, …, f_k) ⊆ G ⊆ Kⁿ (isRegularLocalRing_stalk_iff_jacobian): the stalk 𝒪_{X,z} ≅ 𝒜_{Kⁿ,z}/(f)_z is regular iff some n − d of the f_i, d = dim 𝒪_{X,z}, have linearly independent differentials at z. The proof is the commutative algebra of regular systems of parameters (Hironaka/Algebra/Local/) read through the differential: if the quotient is regular, (f)_z is generated by an initial segment x₁, …, x_c of a regular system of parameters (exists_span_eq_of_isRegularLocalRing_stalk), whose classes in 𝔪/𝔪² are independent and span the image of (f)_z; the classes of the f_i span the same c-dimensional space, so c of them are independent. Conversely c of the f_i with independent differentials are an initial segment of a regular system of parameters, 𝒜/(f_σ) is regular of dimension n − c (Hironaka/AnalyticSpace/RegularParameters.lean), and the surjection 𝒜/(f_σ) → 𝒜/(f) between local rings of the same dimension n − c, from a domain, is an isomorphism (Ideal.eq_bot_of_ringKrullDim_quotient_eq, Hironaka/Algebra/Local/QuotientParameters.lean). The dimension clause is essential: V(y, y − x²) ⊆ K² has rank 1 and stalk K[x]/(x²). Used by Hironaka/AnalyticSpace/RegPoints.lean and Hironaka/AnalyticSpace/DimensionLemmas.lean.

noncomputable def AnalyticSpace.stalkEquivQuotientF {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} (z : ↑↑(localModel K n G f).toPresheafedSpace) : ↑((localModel K n G f).presheaf.stalk z) ≃+* ↑((affine K n).presheaf.stalk ↑↑z) ⧸ Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f j))

The stalk of the local model at z, read in 𝒜_{Kⁿ,z}: 𝒪_{X,z} ≅ 𝒜_{Kⁿ,z}/(f)_z (QuotientSpace.stalkEquiv and Mathlib's restrictStalkIso).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.span_germ_le_maximalIdeal {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} (z : ↑↑(localModel K n G f).toPresheafedSpace) : Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f j)) ≤ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk ↑↑z)

The germs of the f j at a point of the support lie in 𝔪; hence (f)_z ≤ 𝔪_z.

theorem AnalyticSpace.smul_toCotangent_eq {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) (a : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (g : ↥(IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q))) : a • (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent g = (Manifold.eval K (Kn K n) (Kn K n) q) a • (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent g

In the cotangent space 𝔪/𝔪² of 𝒜_{Kⁿ,q}, a germ acts through its value: a • [g] = a(q) • [g].

theorem AnalyticSpace.exists_span_eq_of_isRegularLocalRing_stalk {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) (hreg : IsRegularLocalRing ↑((localModel K n G f).presheaf.stalk z)) : ∃ (c : ℕ) (h : Fin c → ↑((affine K n).presheaf.stalk ↑↑z)), Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f j)) = Ideal.span (Set.range h) ∧ (LinearIndependent K fun (j : Fin c) => (dlin K n ↑↑z) (h j)) ∧ ↑c + ringKrullDim ↑((localModel K n G f).presheaf.stalk z) = ↑n

The algebraic core of → in the Jacobian criterion: if 𝒪_{X,z} is regular, (f)_z is generated by c germs with independent differentials, with c + dim 𝒪_{X,z} = n (regular systems of parameters through the identification 𝒪_{X,z} ≅ 𝒜_{Kⁿ,z}/(f)_z; independence of the differentials from independence in 𝔪/𝔪²).

theorem AnalyticSpace.toCotangent_mem_span_of_mem_span {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) {ι : Type u_1} [Finite ι] (g : ι → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hg : ∀ (i : ι), g i ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) {s : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (h : s ∈ Ideal.span (Set.range g)) : (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨s, hs⟩ ∈ Submodule.span K (Set.range fun (i : ι) => (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨g i, ⋯⟩)

A germ of 𝔪_q in the ideal generated by germs g i ∈ 𝔪_q has its cotangent class in the K-span of theirs (the coefficients act through their values).

theorem AnalyticSpace.cotangentClass_eq_toCotangent {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) {s : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)} (hs : s ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : Manifold.cotangentClass (Kn K n) q s = (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨s, hs⟩

The cotangent class of a germ of 𝔪_q, as Manifold.cotangentClass.

theorem AnalyticSpace.linearIndependent_dlin_iff_toCotangent {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) {ι : Type u_1} [Finite ι] (h : ι → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (i : ι), h i ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : (LinearIndependent K fun (i : ι) => (dlin K n q) (h i)) ↔ LinearIndependent K fun (i : ι) => (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨h i, ⋯⟩

Independence of differentials of germs of 𝔪_q is independence of their classes in 𝔪/𝔪² over K.

theorem AnalyticSpace.isRegularLocalRing_stalk_iff_jacobian {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : IsRegularLocalRing ↑((localModel K n G f).presheaf.stalk z) ↔ ∃ (c : ℕ) (σ : Fin c ↪ Fin k), ↑c + ringKrullDim ↑((localModel K n G f).presheaf.stalk z) = ↑n ∧ LinearIndependent K fun (j : Fin c) => (dlin K n ↑↑z) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f (σ j)))

The Jacobian criterion (the criterion Hironaka invokes at [Hir64, Ch. 0, §1, p. 121]): at a point z of the local model X = V(f₁, …, f_k) ⊆ G ⊆ Kⁿ the stalk 𝒪_{X,z} is regular iff some n − d of the f_i, d = dim 𝒪_{X,z}, have linearly independent differentials at z.