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,199 @@
+/-
+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 the complementary to `PresentedGroup rels`, which constructs the group presented by a set of
+generators and relations.
+
+## Main definitions
+
+* `Group.Generators G α`: a family `val : α → G`, indexed by `α`, with `FreeGroup.lift val`
+  surjective.
+* `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 `α` such that the induced
+homomorphism `FreeGroup.lift val : FreeGroup α →* G` is surjective. -/
+structure Group.Generators (G : Type*) [Group G] (α : Type*) where
+  /-- Identify the generating family `α` with elements of `G` via index set `val`. -/
+  val : α → G
+  /-- The induced map from the free group over the identified elements of `G` via `val`,
+  `FreeGroup.lift val` is surjective onto `G`. -/
+  lift_surjective : Function.Surjective (FreeGroup.lift val)
+
+namespace Group.Generators
+
+variable (P : Group.Generators G α)
+
+/-- The generators of a group generate the whole group under subgroup closure. -/
+theorem closure_range_val_eq_top : Subgroup.closure (Set.range P.val) = ⊤ := by
+  rw [← FreeGroup.range_lift_eq_closure, MonoidHom.range_eq_top]
+  exact P.lift_surjective
+
+/-- Builds a generating set using the index set `val` and a hypothesis that the subgroup closure is
+the whole group. -/
+def ofClosureEqTop (val : α → G) (h : Subgroup.closure (Set.range val) = ⊤) :
+    Group.Generators G α where
+  val := val
+  lift_surjective := by rw [← MonoidHom.range_eq_top, FreeGroup.range_lift_eq_closure]; exact h
+
+/-- The index set built by the generating set `ofClosureEqTop` using `val` is itself. -/
+@[simp]
+theorem val_ofClosureEqTop (val : α → G) (h : Subgroup.closure (Set.range val) = ⊤) :
+    (ofClosureEqTop 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 :=
+  ofClosureEqTop id (by rw [Set.range_id]; exact Subgroup.closure_univ)
+
+/-- The index set `val` given by taking `G` as the generating family for `G` is given by
+the identity map. -/
+@[simp]
+theorem 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 finite generating set. -/
+theorem Group.fg_iff_nonempty_finite_generators :
+    Group.FG G ↔ ∃ (α : Type) (_ : Finite α), Nonempty (Group.Generators G α) := by
+  rw [Group.fg_iff_exists_freeGroup_hom_surjective_finite]
+  constructor
+  · rintro ⟨α, hα, φ, hφ⟩
+    obtain ⟨v, rfl⟩ := FreeGroup.lift.surjective φ
+    exact ⟨α, hα, ⟨v, hφ⟩⟩
+  · rintro ⟨α, hα, ⟨P⟩⟩
+    exact ⟨α, hα, FreeGroup.lift P.val, P.lift_surjective⟩
+
+/-- A group presentation is given by a generating family (`val : α → G`)
+and a family of relators (`rel : ρ → FreeGroup α`) such that the kernel of the free group over
+the generators `FreeGroup.lift val` is given by the normal closure of the relations. -/
+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 the
+  full 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
+
+/-- The canonical map `lift : FreeGroup α →* G` induced by the presentation is surjective.
+This is a restatement of the surjective statement on the generators, hence the `'`. -/
+theorem lift_surjective' : Function.Surjective P.lift := P.lift_surjective
+
+/-- The induced map `lift` sends the free-group generator `FreeGroup.of a` to the corresponding
+generator `val a` of `G`. -/
+@[simp]
+theorem lift_of (a : α) : P.lift (FreeGroup.of a) = P.val a := FreeGroup.lift_apply_of
+
+/-- The range of `lift : FreeGroup α →* G` is all of `G`. -/
+@[simp]
+theorem range_lift_eq_top : P.lift.range = ⊤ :=
+  MonoidHom.range_eq_top.mpr P.lift_surjective'
+
+/-- Each relator `rel r` belongs to the relator set `relSet`. -/
+theorem rel_mem_relSet (r : ρ) : P.rel r ∈ P.relSet := ⟨r, rfl⟩
+
+/-- The relator set of a presentation with finitely many relators is finite. -/
+theorem relSet_finite [Finite ρ] : P.relSet.Finite := Set.finite_range P.rel
+
+/-- Instance form of `relSet_finite`: typeclass search cannot unfold `relSet` to `Set.range rel`,
+so the `Finite ↥(Set.range _)` instance does not apply to `↥relSet` on its own. -/
+instance [Finite ρ] : Finite P.relSet := P.relSet_finite.to_subtype
+
+/-- The kernel of `lift` is the normal closure of the relator set `relSet`: the presentation's
+defining condition `ker_eq_normalClosure`, restated in terms of `lift` and `relSet`. -/
+theorem ker_lift : P.lift.ker = Subgroup.normalClosure P.relSet := P.ker_eq_normalClosure
+
+/-- A relator `r ∈ relSet` maps to the identity in `G` through the canonical surjection from the
+free group. -/
+theorem lift_eq_one_of_mem_relSet {r : FreeGroup α} (hr : r ∈ P.relSet) : P.lift r = 1 :=
+  MonoidHom.mem_ker.mp (by rw [P.ker_lift]; exact Subgroup.subset_normalClosure hr)
+
+/-- Every relator `rel r` of the presentation maps to the identity in `G` through
+the canonical surjection from the free group. -/
+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')
+
+/-- `PresentedGroup.of a` corresponds to the generator `val a` of `G`. -/
+@[simp]
+theorem 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 `Group.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,
+    ⟨{ val := v
+       lift_surjective := hφ
+       rel := Subtype.val
+       ker_eq_normalClosure := by rw [Subtype.range_val]; 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},