English
Let A be a semiring and M an A-module with a submodule N ⊆ M. Then N is finitely generated as an A-submodule if and only if there exists a finite index set G and a function g: G → M such that N is the span of the image of g, i.e. N = span_A(range g).
Русский
Пусть A — полупрямой кольцо и M — A-модуль, пусть N ⊆ M — подмодуль. Тогда N конечно порождается как A-подмодуль тогда и только тогда, когда существует конечный множитель G и функция g: G → M такая, что N = span_A(range g).
LaTeX
$$$N.FG \iff \exists G \ (Finite\ G) \ (g : G \to M), \ \operatorname{span}_A(\operatorname{range} g) = N$$$
Lean4
theorem fg_iff_exists_finite_generating_family {A : Type u} [Semiring A] {M : Type v} [AddCommMonoid M] [Module A M]
{N : Submodule A M} : N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), Submodule.span A (Set.range g) = N :=
by
constructor
· intro hN
obtain ⟨n, f, h⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hN
refine ⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩
convert h
ext x
simp only [Set.mem_range, Function.comp_apply, ULift.exists]
· rintro ⟨G, _, g, hg⟩
have := Fintype.ofFinite (range g)
exact ⟨(range g).toFinset, by simpa using hg⟩
