Regular systems of parameters: the basis of 𝔪/𝔪² and the size of a generating system

Two facts of commutative algebra about a regular local ring R with maximal ideal 𝔪. In a regular local ring of dimension m, the classes in 𝔪/𝔪² of m generators of 𝔪 are linearly independent over the residue field, since they span a space of dimension m (linearIndependent_toCotangent_of_span_eq); and two families of elements of 𝔪 with linearly independent classes generating the same ideal have the same size, by the dimension count of [TSPA, Tag 00NQ] (quotient_span_range_of_linearIndependent) applied to both families (card_eq_of_span_range_eq). Not stated as such in the sources; they are the algebra behind the comparison of two systems of local coordinates cutting out the same subspace.

Used by the submanifold and normal-crossings criteria of Hironaka/Manifold/Snc/ and Space/.

theorem IsRegularLocalRing.linearIndependent_toCotangent_of_span_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {m : ℕ} (z : Fin m → R) (hz : ∀ (i : Fin m), z i ∈ IsLocalRing.maximalIdeal R) (hspan : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R) (hdim : ↑m = ringKrullDim R) : LinearIndependent (IsLocalRing.ResidueField R) fun (i : Fin m) => (IsLocalRing.maximalIdeal R).toCotangent ⟨z i, ⋯⟩

In a regular local ring of dimension m, the classes in 𝔪/𝔪² of m generators of 𝔪 are linearly independent over the residue field (they span a space of dimension m).

theorem IsRegularLocalRing.card_eq_of_span_range_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (f : ι → R) (g : κ → R) (hf : ∀ (i : ι), f i ∈ IsLocalRing.maximalIdeal R) (hg : ∀ (j : κ), g j ∈ IsLocalRing.maximalIdeal R) (hfl : LinearIndependent (IsLocalRing.ResidueField R) fun (i : ι) => (IsLocalRing.maximalIdeal R).toCotangent ⟨f i, ⋯⟩) (hgl : LinearIndependent (IsLocalRing.ResidueField R) fun (j : κ) => (IsLocalRing.maximalIdeal R).toCotangent ⟨g j, ⋯⟩) (heq : Ideal.span (Set.range f) = Ideal.span (Set.range g)) : Fintype.card ι = Fintype.card κ

Two families of elements of 𝔪 with linearly independent classes in 𝔪/𝔪² generating the same ideal have the same size: the dimension count of [TSPA, Tag 00NQ] (quotient_span_range_of_linearIndependent) applied to both families.