Linear independence in the conormal module

For an ideal I of a commutative ring R, elements x₁, …, xₙ ∈ I have linearly independent images in the conormal module I/I² over R/I exactly when a relation ∑ rᵢ xᵢ ∈ I² forces every coefficient rᵢ into I. In a free R-module F the same elements then detect I² F coordinatewise: ∑ xᵢ fᵢ ∈ I² F forces every fᵢ ∈ I F.

For the maximal ideal 𝔪 of a local ring, such xᵢ are lifts of linearly independent vectors of the cotangent space 𝔪/𝔪², for instance part of a minimal system of generators of 𝔪. This is the form in which minimal generators enter the comparison between a Koszul complex and a minimal free resolution of the residue field (Stacks, Lemma 10.110.3).

Main results

• Ideal.linearIndependent_toCotangent_iff: linear independence in I/I² in terms of relations modulo I².
• Ideal.mem_smul_top_of_sum_smul_mem_sq_smul_top: in a free module, ∑ xᵢ fᵢ ∈ I² F forces fᵢ ∈ I F when the xᵢ are linearly independent in I/I².

References

• The Stacks Project, Lemma 10.110.3

theorem Ideal.linearIndependent_toCotangent_iff {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} [Fintype ι] (x : ι → ↥I) : (LinearIndependent (R ⧸ I) fun (i : ι) => I.toCotangent (x i)) ↔ ∀ (r : ι → R), ∑ i : ι, r i * ↑(x i) ∈ I ^ 2 → ∀ (i : ι), r i ∈ I

Elements xᵢ ∈ I have linearly independent images in I/I² over R/I exactly when ∑ rᵢ xᵢ ∈ I² forces every coefficient rᵢ into I.

theorem Ideal.mem_smul_top_of_sum_smul_mem_sq_smul_top {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_2} [Fintype ι] {x : ι → ↥I} (hx : LinearIndependent (R ⧸ I) fun (i : ι) => I.toCotangent (x i)) {F : Type u_3} [AddCommGroup F] [Module R F] [Module.Free R F] {f : ι → F} (hf : ∑ i : ι, ↑(x i) • f i ∈ I ^ 2 • ⊤) (i : ι) : f i ∈ I • ⊤

Let xᵢ ∈ I have linearly independent images in I/I². In a free module F, if ∑ xᵢ fᵢ ∈ I² F then every fᵢ lies in I F.