English
For an additive submonoid S of a module, S is finitely generated iff there exists n and an additive monoid hom from (Fin n → ℕ) onto S.
Русский
Для подмоноида S в модуле характеристика: конечна порождается, если существует n и аддитивный моноид-гомоморфизм из (Fin n → ℕ) на S.
LaTeX
$$$\\forall M [\\text{AddCommMonoid } M], S: AddSubmonoid M, S.FG \\iff \\exists n (f : (Fin n \to ℕ) \to_+ M), AddMonoidHom.mrange f = S.$$$
Lean4
theorem fg_iff_exists_fin_addMonoidHom {M : Type*} [AddCommMonoid M] {S : AddSubmonoid M} :
S.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = S :=
by
rw [← S.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg, Submodule.fg_iff_exists_fin_linearMap]
exact
exists_congr fun n =>
⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubmonoid _⟩, fun ⟨f, hf⟩ =>
⟨f.toNatLinearMap, Submodule.toAddSubmonoid_inj.mp <| hf ▸ LinearMap.range_toAddSubmonoid _⟩⟩
