Generators of modules over a local ring

Over a local ring R, a free module of rank one is generated by a single element of any spanning set. For instance, if Ω[A⁄k] is free of rank one over a local ring A, then it is generated by a single differential d a. This is how a free module of differentials of rank one at a point of a curve gives a local coordinate whose differential generates it.

More generally, a family of n elements of a free module of rank n whose coordinates are linearly independent over the residue field is a basis. Applied to the differentials of a local ring, this changes coordinates.

A finite module M over a local ring (R, 𝔪, k) is the quotient of R ^ μ, with μ the dimension of k ⊗ M, by a submodule of 𝔪 • R ^ μ: lifting a k-basis of k ⊗ M gives generators of M (Nakayama) whose relations all have coefficients in 𝔪. Iterating such minimal covers is how minimal free resolutions are built.

Main results

• TauCeti.IsLocalRing.exists_mem_span_singleton_eq_top_of_finrank_eq_one: a free module of rank one over a local ring is spanned by one element of any spanning set.
• TauCeti.IsLocalRing.exists_basis_of_linearIndependent_residue_coord: a family of n elements of a free module of rank n whose coordinates have linearly independent residues is a basis.
• TauCeti.IsLocalRing.exists_surjective_ker_le_maximalIdeal_smul: a finite module over a local ring (R, 𝔪, k) is a quotient of R ^ dim_k (k ⊗ M) by a submodule of 𝔪 • R ^ dim_k (k ⊗ M).
• TauCeti.IsLocalRing.exists_linearMap_quotient_eq_one: an element of a module M outside 𝔪 • M is sent to 1 by a linear map M → R ⧸ 𝔪.
• Module.free_of_projective_of_isLocalRing: a finitely generated projective module over a local ring is free, for any AddCommMonoid module.

References

• The Stacks Project, Lemma 10.20.1 (00DV), for Nakayama's lemma in the form used here.

theorem TauCeti.IsLocalRing.exists_mem_span_singleton_eq_top_of_finrank_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] [Module.Free R M] (h : Module.finrank R M = 1) {s : Set M} (hs : Submodule.span R s = ⊤) : ∃ m ∈ s, R ∙ m = ⊤

A free module of rank one over a local ring is generated by one element of any spanning set: if M is free of rank one over the local ring R and s spans M, then some m ∈ s spans M.

theorem TauCeti.IsLocalRing.exists_basis_of_linearIndependent_residue_coord {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] (b : Module.Basis ι R M) {v : κ → M} (hcard : Fintype.card κ = Fintype.card ι) (h : LinearIndependent (IsLocalRing.ResidueField R) fun (k : κ) (i : ι) => (IsLocalRing.residue R) ((b.coord i) (v k))) : ∃ (b' : Module.Basis κ R M), ∀ (k : κ), b' k = v k

A family with linearly independent residues is a basis. If M has a basis b indexed by ι, and v is a family of |ι| elements whose coordinates in b, read in the residue field, are linearly independent, then v is a basis of M.

theorem TauCeti.IsLocalRing.exists_surjective_ker_le_maximalIdeal_smul (R : Type u_1) (M : Type u_2) [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (f : (Fin (Module.finrank (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) M)) → R) →ₗ[R] M), Function.Surjective ⇑f ∧ f.ker ≤ IsLocalRing.maximalIdeal R • ⊤

Minimal generators of a finite module over a local ring. If M is a finite module over a local ring (R, 𝔪, k), then M is the image of a surjection R ^ μ → M, with μ = dim_k (k ⊗ M) the minimal number of generators of M, whose kernel is contained in 𝔪 • R ^ μ.

theorem TauCeti.IsLocalRing.exists_surjective_ker_le_maximalIdeal_smul_shrink {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (g : (Fin n → Shrink.{v, u} R) →ₗ[R] M), Function.Surjective ⇑g ∧ g.ker ≤ IsLocalRing.maximalIdeal R • ⊤

A finite module over a local ring is a quotient of a finite free module, with free module in the universe of the module, by a submodule contained in 𝔪 • ⊤.

theorem TauCeti.IsLocalRing.exists_linearMap_quotient_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {m : M} (hm : m ∉ IsLocalRing.maximalIdeal R • ⊤) : ∃ (r : M →ₗ[R] R ⧸ IsLocalRing.maximalIdeal R), r m = 1

An element of a module over a local ring outside 𝔪 • M is sent to 1 by a linear map to the residue field, since its class in the vector space M ⧸ 𝔪 • M is nonzero.

theorem Module.free_of_projective_of_isLocalRing {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Projective R M] : Free R M

A finitely generated projective module over a local ring is free. This is Module.free_of_flat_of_isLocalRing, once the module carries the additive group structure that it asks for.