feat(Group Theory/Presentation): define group presentations

Mathlib.lean

@@ -4853,6 +4853,7 @@ public import Mathlib.GroupTheory.Perm.Sign
 public import Mathlib.GroupTheory.Perm.Subgroup
 public import Mathlib.GroupTheory.Perm.Support
 public import Mathlib.GroupTheory.Perm.ViaEmbedding
+public import Mathlib.GroupTheory.Presentation
 public import Mathlib.GroupTheory.PresentedGroup
 public import Mathlib.GroupTheory.PushoutI
 public import Mathlib.GroupTheory.QuotientGroup.Basic

Mathlib/GroupTheory/Presentation.lean

@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2026 Hang Lu Su, Valerio Proietti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Hang Lu Su, Valerio Proietti
+-/
+module
+
+public import Mathlib.GroupTheory.FinitelyPresentedGroup
+
+/-!
+# Group presentations as data
+
+`Group.Presentation` packages a chosen presentation of a given group `G`:
+a generating family together with relators (words `r`, each read as `r = 1`) whose
+generated normal subgroup is exactly the kernel of `FreeGroup.lift val : FreeGroup α →* G`.
+This is complementary to `PresentedGroup rels`, which constructs the group presented by a given set
+of generators and relations.
+
+## Main definitions
+
+* `Group.Generators G α`: a family `val : α → G`, indexed by `α`, whose range generates `G`.
+* `Group.Presentation G α ρ`: a presentation `⟨α | rel⟩` of `G`, extending `Group.Generators G α`
+
+## Main results
+
+* `Group.Generators.fg` and `Group.fg_iff_nonempty_finite_generators`: a finite generating family
+  witnesses `Group.FG`, and conversely.
+* `Group.Presentation.isFinitelyPresented` and
+  `Group.isFinitelyPresented_iff_nonempty_finite_presentation`: a finite presentation witnesses
+  `Group.IsFinitelyPresented`, and conversely.
+
+## Design notes
+
+* Finiteness is expressed by instance arguments rather than bundled fields: a generating family is
+  finite when `[Finite α]`, a presentation when `[Finite α] [Finite ρ]`.
+* This file is multiplicative only: `PresentedGroup` has no additive counterpart and there is no
+`to_additive`-generated `AddGroup.Presentation` so far.
+
+## References
+
+* [D. F. Holt, S. Rees, C. E. Röver, *Groups, Languages and Automata*][HoltReesRover2017], §1
+
+## Tags
+
+group presentation, generators and relations
+-/
+
+@[expose] public section
+
+variable {G α ρ : Type*} [Group G]
+
+/-- The generators of a group are given by a generating family indexed by `α` whose range generates
+`G`, or equivalently such that the induced homomorphism `FreeGroup.lift val : FreeGroup α →* G` is
+surjective. -/
+structure Group.Generators (G : Type*) [Group G] (α : Type*) where
+  /-- The generating family itself: `val a` is the element of `G` indexed by `a : α`. -/
+  val : α → G
+  /-- The subgroup closure of the generators generate the whole group. -/
+  closure_eq_top : Subgroup.closure (Set.range val) = ⊤
+
+namespace Group.Generators
+
+variable (P : Group.Generators G α)
+
+@[simp]
+lemma range_lift_eq_top : (FreeGroup.lift P.val).range = ⊤ := by
+  rw [FreeGroup.range_lift_eq_closure, P.closure_eq_top]
+
+lemma lift_surjective : Function.Surjective (FreeGroup.lift P.val) :=
+  MonoidHom.range_eq_top.mp P.range_lift_eq_top
+
+/-- Builds a `Group.Generators` from a family `val : α → G` together with a proof that the induced
+map `FreeGroup.lift val` is surjective. -/
+def ofLiftSurjective (val : α → G) (h : Function.Surjective (FreeGroup.lift val)) :
+    Group.Generators G α where
+  val := val
+  closure_eq_top := by rw [← FreeGroup.range_lift_eq_closure, MonoidHom.range_eq_top.mpr h]
+
+@[simp]
+lemma val_ofLiftSurjective (val : α → G) (h : Function.Surjective (FreeGroup.lift val)) :
+    (ofLiftSurjective val h).val = val := rfl
+
+/-- `G` as a generating set generates itself via taking `val` as the identity map. -/
+def self (G : Type*) [Group G] : Group.Generators G G where
+  val := id
+  closure_eq_top := by rw [Set.range_id, Subgroup.closure_univ]
+
+@[simp]
+lemma val_self : (self G).val = id := rfl
+
+/-- If G is generated by a finite generating set `α`, then `G` is finitely generated. -/
+theorem fg [Finite α] (P : Group.Generators G α) : Group.FG G :=
+  Group.fg_of_surjective P.lift_surjective
+
+end Group.Generators
+
+/-- A group is finitely generated if and only if it admits a generating family indexed by
+a finite generating set, which then indexes itself. -/
+theorem Group.fg_iff_nonempty_finite_generators :
+    Group.FG G ↔ ∃ (S : Set G) (_ : S.Finite), Nonempty (Group.Generators G S) := by
+  constructor
+  · rintro ⟨S, hS⟩
+    exact ⟨S, S.finite_toSet, ⟨⟨Subtype.val, by rwa [Subtype.range_coe]⟩⟩⟩
+  · rintro ⟨S, hS, ⟨P⟩⟩
+    have := hS.to_subtype
+    exact P.fg
+
+/-- A group presentation is given by a generating family (`val : α → G`) and a family of relators
+(`rel : ρ → FreeGroup α`) such that the normal subgroup generated by the relators is exactly the
+kernel of the canonical map `FreeGroup.lift val` from the free group on the generators to `G`. -/
+structure Group.Presentation (G : Type*) [Group G] (α ρ : Type*)
+    extends Group.Generators G α where
+  /-- The family of relators, as words in the free group; each `rel r` is read as `rel r = 1`
+  in the sense that it is meant to map to the kernel in `G`. -/
+  rel : ρ → FreeGroup α
+  /-- The relators are exactly the defining relations: the normal subgroup they generate is
+  exactly the kernel of `FreeGroup.lift val`, so no relation holds in `G` beyond their
+  consequences. -/
+  ker_eq_normalClosure :
+    (FreeGroup.lift val).ker = Subgroup.normalClosure (Set.range rel)
+
+namespace Group.Presentation
+
+variable (P : Group.Presentation G α ρ)
+
+/-- The canonical surjection from free group on the generators of the presentation to `G`. -/
+def lift : FreeGroup α →* G := FreeGroup.lift P.val
+
+/-- The set of relators of the presentation, as words in the free group. This is written because
+`PresentedGroup` takes a set of relations as `Set (FreeGroup α)`. -/
+def relSet : Set (FreeGroup α) := Set.range P.rel
+
+lemma lift_surjective' : Function.Surjective P.lift := P.lift_surjective
+
+@[simp]
+lemma lift_of (a : α) : P.lift (FreeGroup.of a) = P.val a := FreeGroup.lift_apply_of
+
+@[simp]
+lemma range_lift_eq_top : P.lift.range = ⊤ :=
+  MonoidHom.range_eq_top.mpr P.lift_surjective'
+
+lemma rel_mem_relSet (r : ρ) : P.rel r ∈ P.relSet := ⟨r, rfl⟩
+
+lemma relSet_finite [Finite ρ] : P.relSet.Finite := Set.finite_range P.rel
+
+instance [Finite ρ] : Finite P.relSet := P.relSet_finite.to_subtype
+
+lemma ker_lift : P.lift.ker = Subgroup.normalClosure P.relSet := P.ker_eq_normalClosure
+
+lemma lift_eq_one_of_mem_relSet {r : FreeGroup α} (hr : r ∈ P.relSet) : P.lift r = 1 :=
+  MonoidHom.mem_ker.mp (by simpa [P.ker_lift] using Subgroup.subset_normalClosure hr)
+
+theorem lift_rel (r : ρ) : P.lift (P.rel r) = 1 :=
+  P.lift_eq_one_of_mem_relSet (P.rel_mem_relSet r)
+
+/-- The `G` with presentation `P` is isomorphic to the `PresentedGroup` given by `P.relSet`. -/
+noncomputable def presentedGroupEquiv : PresentedGroup P.relSet ≃* G :=
+  (QuotientGroup.quotientMulEquivOfEq P.ker_lift.symm).trans
+    (QuotientGroup.quotientKerEquivOfSurjective P.lift P.lift_surjective')
+
+@[simp]
+lemma presentedGroupEquiv_of (a : α) :
+    P.presentedGroupEquiv (PresentedGroup.of a) = P.val a := P.lift_of a
+
+/-- A finite presentation is finitely presented. -/
+theorem isFinitelyPresented [Finite α] [Finite ρ] (P : Group.Presentation G α ρ) :
+    Group.IsFinitelyPresented G := IsFinitelyPresented.equiv P.presentedGroupEquiv
+
+end Group.Presentation
+
+/-- A group is finitely presented if and only if it admits a presentation
+with finitely many generators and finitely many relators. -/
+theorem Group.isFinitelyPresented_iff_nonempty_finite_presentation :
+    Group.IsFinitelyPresented G ↔
+      ∃ (α ρ : Type) (_ : Finite α) (_ : Finite ρ), Nonempty (Group.Presentation G α ρ) := by
+  refine ⟨fun h ↦ ?_, fun ⟨_, _, _, _, ⟨P⟩⟩ ↦ P.isFinitelyPresented⟩
+  obtain ⟨n, φ, hφ, s, hs, hsφ⟩ := h.out
+  obtain ⟨v, rfl⟩ := FreeGroup.lift.surjective φ
+  exact ⟨Fin n, s, inferInstance, hs.to_subtype,
+    ⟨{ toGenerators := Group.Generators.ofLiftSurjective v hφ
+       rel := Subtype.val
+       ker_eq_normalClosure := by rw [Subtype.range_coe]; exact hsφ.symm }⟩⟩

docs/references.bib

@@ -3069,6 +3069,18 @@ @Article{         hollom2025
   url           = {https://arxiv.org/abs/2411.16844}
 }
 
+@Book{            HoltReesRover2017,
+  author        = {Holt, Derek F. and Rees, Sarah and R\"over, Claas E.},
+  title         = {Groups, languages and automata},
+  series        = {London Mathematical Society Student Texts},
+  volume        = {88},
+  publisher     = {Cambridge University Press, Cambridge},
+  year          = {2017},
+  pages         = {xi+294},
+  isbn          = {978-1-107-15235-9; 978-1-316-60652-0},
+  doi           = {10.1017/9781316588246}
+}
+
 @Article{         hong2014,
   title         = {On the Euclidean dimension of graphs},
   author        = {Jin Hyup Hong and Dan Ismailescu},