Finitely generated lattices in a finite module

Let M be a finite A-module and also an R-module. Then M contains a finitely generated R-submodule spanning M over A: the R-span of any finite A-generating set. The typical case is a subring R of A, such as a ring of definition of a Huber ring, where such a submodule is a lattice of M over R whose filtrations describe the natural topology of M.

Main results

• TauCeti.Module.Finite.exists_fg_span_eq_top: a finite A-module has a finitely generated R-submodule spanning it over A.

theorem TauCeti.Module.Finite.exists_fg_span_eq_top (R : Type u_1) {A : Type u_2} {M : Type u_3} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [Module.Finite A M] : ∃ (M₀ : Submodule R M), M₀.FG ∧ Submodule.span A ↑M₀ = ⊤

A finite A-module that is also an R-module has a finitely generated R-submodule spanning it over A.