Germs with independent differentials are part of a regular system of parameters

Germs h₁, …, h_c ∈ 𝔪_q of 𝒜_{Kⁿ,q} are part of a regular system of parameters iff their differentials dh_{1,q}, …, dh_{c,q} are linearly independent — the analytic form of the standard fact about regular local rings [TSPA, Tag 00NQ]. The proof runs through the cotangent space 𝔪_q/𝔪_q²: the K-linear independence of the differentials is that of the cotangent classes (linearIndependent_cotangentClass_iff_linearPart); the classes live in the CotangentSpace, a vector space over the residue field κ = 𝒜_{Kⁿ,q}/𝔪_q, and K → κ is an isomorphism (every germ is a constant modulo 𝔪_q, a nonzero constant is a unit), so K-independence and κ-independence agree (linearIndependent_residueField_iff_of_algebra); and a family of 𝔪_q is a minimal generating system — a regular system of parameters, 𝒜_{Kⁿ,q} being regular of dimension n — iff its classes are a κ-basis (IsLocalRing.span_eq_maximalIdeal_and_card_eq_spanFinrank_iff, IsLocalRing.exists_basis_cotangentSpace_of_span_eq). Independent classes extend to a basis (Module.Basis.sumExtend), whose new members are lifted to 𝔪_q. The theorem isRegularLocalRing_quotient_span_range_and_ringKrullDim gives the regularity and the dimension n − c of the quotient of 𝒜_{Kⁿ,q} by such germs, the algebraic core of the fact that the common zero set of c functions with independent differentials is a submanifold of codimension c.

theorem Module.Basis.sumExtend_inl {F : Type u_1} {V : Type u_2} {ι : Type u_3} [Field F] [AddCommGroup V] [Module F V] {v : ι → V} (hs : LinearIndependent F v) (i : ι) : (sumExtend hs) (Sum.inl i) = v i

Module.Basis.sumExtend keeps the given vectors at the inl indices.

theorem AnalyticSpace.linearIndependent_residueField_iff_of_algebra {F : Type u_1} [Field F] {R : Type u_2} [CommRing R] [IsLocalRing R] [Algebra F R] (hsurj : ∀ (r : R), ∃ (c : F), r - (algebraMap F R) c ∈ IsLocalRing.maximalIdeal R) (hinj : ∀ (c : F), (algebraMap F R) c ∈ IsLocalRing.maximalIdeal R → c = 0) {ι : Type u_3} [Finite ι] (v : ι → IsLocalRing.CotangentSpace R) : LinearIndependent (IsLocalRing.ResidueField R) v ↔ LinearIndependent F v

Linear independence in the cotangent space 𝔪/𝔪² over the residue field κ = R/𝔪 and over a field of constants F → R agree when F → κ is an isomorphism (every element of R is a constant modulo 𝔪, and a constant in 𝔪 is zero).

theorem AnalyticSpace.exists_sub_algebraMap_mem_maximalIdeal (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (r : ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : ∃ (c : K), r - (algebraMap K ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) c ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)

Every germ of 𝒜_{Kⁿ,q} is a constant modulo 𝔪_q (its value at q).

theorem AnalyticSpace.algebraMap_mem_maximalIdeal_imp (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) (c : K) (hc : (algebraMap K ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) c ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : c = 0

A constant of 𝒜_{Kⁿ,q} lying in 𝔪_q is zero.

theorem AnalyticSpace.exists_span_eq_maximalIdeal_of_equiv (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hli : LinearIndependent (IsLocalRing.ResidueField ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) fun (j : Fin c) => (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨h j, ⋯⟩) (e : Fin c ⊕ ↑(Module.Basis.sumExtendIndex hli) ≃ Fin n) : ∃ (x : Fin n → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)), IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) = Ideal.span (Set.range x) ∧ ∀ (j : Fin c), x (e (Sum.inl j)) = h j

Independent cotangent classes of h₁, …, h_c ∈ 𝔪_q extend to a regular system of parameters x indexed by Fin n through any bijection e of Fin c ⊕ (new indices) with Fin n, with x (e (inl j)) = h j.

theorem AnalyticSpace.card_sumExtendIndex (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hli : LinearIndependent (IsLocalRing.ResidueField ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) fun (j : Fin c) => (IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)).toCotangent ⟨h j, ⋯⟩) [Fintype ↑(Module.Basis.sumExtendIndex hli)] : c + Fintype.card ↑(Module.Basis.sumExtendIndex hli) = n

The count: c independent classes plus the new basis vectors make n = dim 𝔪_q/𝔪_q².

theorem AnalyticSpace.exists_span_eq_maximalIdeal_extending_iff' (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) : (∃ (x : Fin n → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (σ : Fin c ↪ Fin n), IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) = Ideal.span (Set.range x) ∧ ↑n = ringKrullDim ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) ∧ ∀ (j : Fin c), x (σ j) = h j) ↔ LinearIndependent K fun (j : Fin c) => (Manifold.linearPart (Kn K n) ContinuousLinearEquiv.ulift (chartAt (Kn K n) q) ⋯ ⋯) (h j)

Germs h₁, …, h_c ∈ 𝔪_q are part of a regular system of parameters of 𝒜_{Kⁿ,q} iff their linear parts are linearly independent, in the structure-sheaf presentation of the stalk.

theorem AnalyticSpace.exists_span_eq_maximalIdeal_castLE (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hli : LinearIndependent K fun (j : Fin c) => (Manifold.linearPart (Kn K n) ContinuousLinearEquiv.ulift (chartAt (Kn K n) q) ⋯ ⋯) (h j)) : ∃ (hcn : c ≤ n) (x : Fin n → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)), IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) = Ideal.span (Set.range x) ∧ ∀ (j : Fin c), x (Fin.castLE hcn j) = h j

Germs h₁, …, h_c ∈ 𝔪_q with independent differentials are the initial segment of a regular system of parameters x of 𝒜_{Kⁿ,q}: x (castLE j) = h j.

theorem AnalyticSpace.isRegularLocalRing_quotient_span_range_and_ringKrullDim (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q)) (hli : LinearIndependent K fun (j : Fin c) => (Manifold.linearPart (Kn K n) ContinuousLinearEquiv.ulift (chartAt (Kn K n) q) ⋯ ⋯) (h j)) : IsRegularLocalRing (↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) ⧸ Ideal.span (Set.range h)) ∧ ringKrullDim (↑((Manifold.structureSheaf K (Kn K n) (Kn K n)).presheaf.stalk q) ⧸ Ideal.span (Set.range h)) + ↑c = ↑n

The quotient of 𝒜_{Kⁿ,q} by c germs of 𝔪_q with independent differentials is a regular local ring of dimension n − c: the germs are an initial segment of a regular system of parameters, and the quotient of a regular local ring by an initial segment of a regular system of parameters is regular of the complementary dimension (IsLocalRing.isRegularLocalRing_quotient_span_image_lt_and_ringKrullDim).

theorem AnalyticSpace.exists_span_eq_maximalIdeal_extending_iff (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) {c : ℕ} (h : Fin c → ↑((affine K n).presheaf.stalk q)) (hm : ∀ (j : Fin c), h j ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk q)) : (∃ (x : Fin n → ↑((affine K n).presheaf.stalk q)) (σ : Fin c ↪ Fin n), IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk q) = Ideal.span (Set.range x) ∧ ↑n = ringKrullDim ↑((affine K n).presheaf.stalk q) ∧ ∀ (j : Fin c), x (σ j) = h j) ↔ LinearIndependent K fun (j : Fin c) => (dlin K n q) (h j)

Germs h₁, …, h_c ∈ 𝔪_q are part of a regular system of parameters of 𝒜_{Kⁿ,q} iff their differentials are linearly independent.