English
For an additive submonoid S of an additive group M, S.FG iff there exists n and an AddMonoidHom from (Fin n → ℕ) onto S.
Русский
Для подмоноида S в аддитивной группе M, S.FG тогда и только тогда, когда существует n и аддитивный моноид-гомоморфизм из (Fin n → ℕ) на S.
LaTeX
$$$\\forall M [\\text{AddCommGroup } 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*} [AddCommGroup M] {H : AddSubgroup M} :
H.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M), AddMonoidHom.range f = H :=
by
rw [← H.toIntSubmodule_toAddSubgroup, ← Submodule.fg_iff_addSubgroup_fg, Submodule.fg_iff_exists_fin_linearMap]
refine
exists_congr fun n =>
⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubgroup _⟩, fun ⟨f, hf⟩ =>
⟨f.toIntLinearMap, Submodule.toAddSubmonoid_inj.mp ?_⟩⟩
simp [hf]
