Generating families and the least number of generators

For a finitely generated submodule, its least number of generators is at most n exactly when it has a generating family indexed by Fin n; a shorter family can be padded with zeros.

If p ≤ q are submodules with p finitely generated, the spanFinrank of q is bounded by those of p and the image of q in M ⧸ p. When q is finitely generated, this bounds its least number of generators: generators of p together with lifts of generators of the image generate q. For a non-finitely-generated submodule, spanFinrank is defined to be 0.

Main results

• Submodule.FG.spanFinrank_le_iff_exists_fin_generating_family: p.spanFinrank ≤ n exactly when p is spanned by a family indexed by Fin n.
• Submodule.spanFinrank_span_list_le_length: the span of a list needs at most as many generators as the list's length.
• Submodule.spanFinrank_restrictScalars_eq: restricting scalars along a surjective algebraMap preserves spanFinrank.
• Submodule.spanFinrank_le_spanFinrank_map_mkQ_add_spanFinrank: for p ≤ q with p finitely generated, q.spanFinrank ≤ (q.map p.mkQ).spanFinrank + p.spanFinrank.

References

• The bound through a quotient is the generator-lifting step in the proof of Stacks Project, Lemma 10.106.7. It is ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Bounding/PrincipalQuotientRegular.lean, and generalizes its Pcf.spanFinrank_maximalIdeal_le_add_one_of_principal_kernel from a principal kernel and the maximal ideal of a local ring to any submodules p ≤ q with p finitely generated.

theorem Submodule.FG.spanFinrank_le_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (hp : p.FG) (n : ℕ) : p.spanFinrank ≤ n ↔ ∃ (f : Fin n → M), span R (Set.range f) = p

A finitely generated submodule has at most n generators exactly when it is spanned by a family of length n. Zero entries may pad a shorter generating family.

theorem Submodule.spanFinrank_span_list_le_length {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (l : List M) : (span R {x : M | x ∈ l}).spanFinrank ≤ l.length

The span of the entries of a list needs at most as many generators as the list has entries.

theorem Submodule.spanFinrank_restrictScalars_eq {R : Type u_3} {S : Type u_4} {M : Type u} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (H : Function.Surjective ⇑(algebraMap R S)) (N : Submodule S M) : (restrictScalars R N).spanFinrank = N.spanFinrank

Along a surjective algebraMap R S, restricting scalars does not change the least number of generators of an S-submodule.

theorem Submodule.spanFinrank_le_spanFinrank_map_mkQ_add_spanFinrank {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p q : Submodule R M} (hpq : p ≤ q) (hp : p.FG) : q.spanFinrank ≤ (map p.mkQ q).spanFinrank + p.spanFinrank

If p ≤ q are submodules with p finitely generated, then q.spanFinrank is at most the sum of the spanFinranks of p and of the image of q in M ⧸ p. When q is finitely generated, this is a generator bound: generators of p and lifts of generators of the image generate q. For non-finitely-generated q, q.spanFinrank is defined to be 0.