Closure properties of finitely generated groups

Mathlib has a substantial theory of finitely generated commutative groups in Mathlib/GroupTheory/FiniteAbelian/Basic.lean — the structure theorem, finite_of_fg_isMulTorsion, and Subgroup.finiteIndex_range_powMonoidHom_of_fg, which is the finiteness of G ⧸ Gⁿ. Three closure properties it does not carry are collected here.

Main results

• AddSubgroup.fg_of_addCommGroup and Subgroup.fg_of_commGroup: a subgroup of a finitely generated commutative group is finitely generated. The argument is Noetherianity of ℤ, so the additive statement is the foundational one and the multiplicative statement is transported from it through Additive; to_additive cannot relate them — it would have to translate the ℤ-module argument itself — so the pair is written out by hand and registered with to_additive existing. Both are instances, matching how Mathlib states its other FG closure properties (Group.fg_range, QuotientGroup.fg, Subgroup.fg_of_index_ne_zero).
• Subgroup.fg_of_fg_map_of_fg_inf_ker: a subgroup K whose image K.map φ and whose intersection K ⊓ φ.ker with the kernel are finitely generated is itself finitely generated. This is the Subgroup analogue of Mathlib's Submodule.fg_of_fg_map_of_fg_inf_ker, an absence Mathlib records explicitly — a comment in Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean restructures a proof "due to no Subgroup version of Submodule.fg_of_fg_map_of_fg_inf_ker existing". It carries the generator argument, and needs no commutativity.
• Group.fg_of_fg_ker_of_fg_range: an extension of finitely generated groups is finitely generated — if the kernel and the range of φ : G →* H are finitely generated then so is G. It is the K = ⊤ case of the previous result, and is derived from it. It is a plain theorem rather than an instance, because φ is an explicit argument that typeclass resolution cannot infer.

Both are @[to_additive], and both are steps towards the S-unit group being finitely generated, which TauCetiRoadmap/EllipticCurves/README.md §Layer 6 names as an input to the weak Mordell–Weil theorem: the group of S-units sits in an extension whose kernel is the unit group of the base and whose range is a subgroup of a free group of rank |S|, so establishing finite generation needs exactly these two facts. The finiteness that the descent then applies to it is Mathlib's Subgroup.finiteIndex_range_powMonoidHom_of_fg, read through Subgroup.finiteIndex_iff_finite_quotient; nothing here reproves it.

AddSubgroup.fg_of_addCommGroup, Subgroup.fg_of_commGroup and Group.fg_of_fg_ker_of_fg_range are adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SelmerGroup.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll). Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

Subgroup.fg_of_fg_map_of_fg_inf_ker is new here, with no counterpart in that source, which has only the K = ⊤ case; Mathlib records the general statement's absence in the comment at Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean quoted above. The generator argument is Stoll's, restated for a subgroup.

That source file also carries finite_modPow, finite_of_fg_of_pow_eq_one and two ℤ-module translation helpers. None of them is ported: all four are now in Mathlib — as Subgroup.finiteIndex_range_powMonoidHom_of_fg, CommGroup.finite_of_fg_isMulTorsion, the instance AddMonoid.FG.to_moduleFinite_int, and Module.Finite.iff_addGroup_fg composed with AddGroup.fg_iff_mul_fg. The source predates those additions, some of which its own author upstreamed, so check Mathlib again before porting anything further from it.

Concurrent work upstream. The open Mathlib pull request mathlib4#40791 ("dirichlet's s-unit theorem", by vvvv-ops, open since 2026-06-19) carries two of the results here as file-local helpers of Mathlib/RingTheory/DedekindDomain/SUnit.lean, under different names: Subgroup.fg_of_commGroup as Subgroup.fg_of_fg_commGroup, and Group.fg_of_fg_ker_of_fg_range as CommGroup.fg_of_fg_ker_of_fg_range — the latter CommGroup-only, where the version here needs no commutativity. On a bump that lands #40791, drop Subgroup.fg_of_commGroup in favour of upstream's; the extension lemma here is strictly more general, and Subgroup.fg_of_fg_map_of_fg_inf_ker has no counterpart there at all.

@[instance 100]

instance AddSubgroup.fg_of_addCommGroup {G : Type u_1} [AddCommGroup G] [AddGroup.FG G] (H : AddSubgroup G) : AddGroup.FG ↥H

A subgroup of a finitely generated additive commutative group is finitely generated. The additive form of Subgroup.fg_of_commGroup.

@[instance 100]

instance Subgroup.fg_of_commGroup {G : Type u_1} [CommGroup G] [Group.FG G] (H : Subgroup G) : Group.FG ↥H

A subgroup of a finitely generated commutative group is finitely generated. The multiplicative form of AddSubgroup.fg_of_addCommGroup.

theorem Subgroup.fg_of_fg_map_of_fg_inf_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) {K : Subgroup G} (h₁ : (map φ K).FG) (h₂ : (K ⊓ φ.ker).FG) : K.FG

A subgroup whose image and whose intersection with the kernel are finitely generated is itself finitely generated. The Subgroup analogue of Mathlib's Submodule.fg_of_fg_map_of_fg_inf_ker, whose absence Mathlib records explicitly: a comment in Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean restructures a proof "due to no Subgroup version of Submodule.fg_of_fg_map_of_fg_inf_ker existing".

Group.fg_of_fg_ker_of_fg_range is its K = ⊤ case.

theorem AddSubgroup.fg_of_fg_map_of_fg_inf_ker {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (φ : G →+ H) {K : AddSubgroup G} (h₁ : (map φ K).FG) (h₂ : (K ⊓ φ.ker).FG) : K.FG

An additive subgroup whose image and whose intersection with the kernel are finitely generated is itself finitely generated. The AddSubgroup analogue of Mathlib's Submodule.fg_of_fg_map_of_fg_inf_ker. AddGroup.fg_of_fg_ker_of_fg_range is its K = ⊤ case.

theorem Group.fg_of_fg_ker_of_fg_range {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) [FG ↥φ.ker] [FG ↥φ.range] : FG G

An extension of finitely generated groups is finitely generated: if the kernel and the range of φ : G →* H are finitely generated, then so is G. This is the K = ⊤ case of Subgroup.fg_of_fg_map_of_fg_inf_ker.

theorem AddGroup.fg_of_fg_ker_of_fg_range {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (φ : G →+ H) [FG ↥φ.ker] [FG ↥φ.range] : FG G

An extension of finitely generated additive groups is finitely generated: if the kernel and the range of φ : G →+ H are finitely generated, then so is G. This is the K = ⊤ case of AddSubgroup.fg_of_fg_map_of_fg_inf_ker.