From b48a9df7117172e98f2d333858aec8138c0f81be Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Mon, 20 Jul 2026 16:37:08 +0100 Subject: [PATCH 1/6] add presentation as structure --- Mathlib.lean | 1 + Mathlib/GroupTheory/Presentation.lean | 199 ++++++++++++++++++++++++++ docs/references.bib | 12 ++ 3 files changed, 212 insertions(+) create mode 100644 Mathlib/GroupTheory/Presentation.lean diff --git a/Mathlib.lean b/Mathlib.lean index ce7026455fc354..ccb3171b3ecdf4 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean new file mode 100644 index 00000000000000..49aaf876c3ebb0 --- /dev/null +++ b/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 }⟩⟩ diff --git a/docs/references.bib b/docs/references.bib index c72b34d1b8d66a..f5a309870aaa13 100644 --- a/docs/references.bib +++ b/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}, From 9dc97a82a0ce019aef9bebc2f379cf97afe3e83b Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Mon, 20 Jul 2026 17:21:45 +0100 Subject: [PATCH 2/6] changed definition --- Mathlib/GroupTheory/Presentation.lean | 60 ++++++++++++++------------- 1 file changed, 32 insertions(+), 28 deletions(-) diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean index 49aaf876c3ebb0..666007630cfda2 100644 --- a/Mathlib/GroupTheory/Presentation.lean +++ b/Mathlib/GroupTheory/Presentation.lean @@ -13,13 +13,12 @@ public import Mathlib.GroupTheory.FinitelyPresentedGroup `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. +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 `α`, with `FreeGroup.lift val` - surjective. +* `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 @@ -50,42 +49,48 @@ group presentation, generators and relations 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. -/ +/-- 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 - /-- Identify the generating family `α` with elements of `G` via index set `val`. -/ + /-- The generating family itself: `val a` is the element of `G` indexed by `a : α`. -/ 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) + /-- 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 α) -/-- 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 +/-- The range of the free group over the generators, `FreeGroup.lift val`, is the whole group. -/ +@[simp] +theorem range_lift_eq_top : (FreeGroup.lift P.val).range = ⊤ := by + rw [FreeGroup.range_lift_eq_closure]; exact P.closure_eq_top + +/-- The induced map from the free group over the identified elements of `G` via `val`, +`FreeGroup.lift val`, is surjective onto `G`. -/ +theorem lift_surjective : Function.Surjective (FreeGroup.lift P.val) := + MonoidHom.range_eq_top.mp P.range_lift_eq_top -/-- 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) = ⊤) : +/-- 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 - lift_surjective := by rw [← MonoidHom.range_eq_top, FreeGroup.range_lift_eq_closure]; exact h + closure_eq_top := by rw [← FreeGroup.range_lift_eq_closure, MonoidHom.range_eq_top]; exact h -/-- The index set built by the generating set `ofClosureEqTop` using `val` is itself. -/ +/-- The generating family underlying `ofLiftSurjective val h` is `val` itself. -/ @[simp] -theorem val_ofClosureEqTop (val : α → G) (h : Subgroup.closure (Set.range val) = ⊤) : - (ofClosureEqTop val h).val = val := rfl +theorem 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 := - ofClosureEqTop id (by rw [Set.range_id]; exact Subgroup.closure_univ) +def self (G : Type*) [Group G] : Group.Generators G G where + val := id + closure_eq_top := 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. -/ +/-- The generating family underlying `self G`, taking `G` as its own generating family, is the +identity map. -/ @[simp] theorem val_self : (self G).val = id := rfl @@ -102,7 +107,7 @@ theorem Group.fg_iff_nonempty_finite_generators : constructor · rintro ⟨α, hα, φ, hφ⟩ obtain ⟨v, rfl⟩ := FreeGroup.lift.surjective φ - exact ⟨α, hα, ⟨v, hφ⟩⟩ + exact ⟨α, hα, ⟨Group.Generators.ofLiftSurjective v hφ⟩⟩ · rintro ⟨α, hα, ⟨P⟩⟩ exact ⟨α, hα, FreeGroup.lift P.val, P.lift_surjective⟩ @@ -193,7 +198,6 @@ theorem Group.isFinitelyPresented_iff_nonempty_finite_presentation : 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φ + ⟨{ toGenerators := Group.Generators.ofLiftSurjective v hφ rel := Subtype.val ker_eq_normalClosure := by rw [Subtype.range_val]; exact hsφ.symm }⟩⟩ From fc6363e3b093de26c317c8734f68aca5bbe1c378 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Mon, 20 Jul 2026 17:25:55 +0100 Subject: [PATCH 3/6] removed abundant docstrings and converted dosctring-less theorems into lemmas --- Mathlib/GroupTheory/Presentation.lean | 48 +++++++-------------------- 1 file changed, 12 insertions(+), 36 deletions(-) diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean index 666007630cfda2..de9e518d675d7f 100644 --- a/Mathlib/GroupTheory/Presentation.lean +++ b/Mathlib/GroupTheory/Presentation.lean @@ -62,37 +62,28 @@ namespace Group.Generators variable (P : Group.Generators G α) -/-- The range of the free group over the generators, `FreeGroup.lift val`, is the whole group. -/ @[simp] -theorem range_lift_eq_top : (FreeGroup.lift P.val).range = ⊤ := by +lemma range_lift_eq_top : (FreeGroup.lift P.val).range = ⊤ := by rw [FreeGroup.range_lift_eq_closure]; exact P.closure_eq_top -/-- The induced map from the free group over the identified elements of `G` via `val`, -`FreeGroup.lift val`, is surjective onto `G`. -/ -theorem lift_surjective : Function.Surjective (FreeGroup.lift P.val) := +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]; exact h -/-- The generating family underlying `ofLiftSurjective val h` is `val` itself. -/ @[simp] -theorem val_ofLiftSurjective (val : α → G) (h : Function.Surjective (FreeGroup.lift val)) : +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]; exact Subgroup.closure_univ -/-- The generating family underlying `self G`, taking `G` as its own generating family, is the -identity map. -/ @[simp] -theorem val_self : (self G).val = id := rfl +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 := @@ -135,42 +126,27 @@ def lift : FreeGroup α →* G := FreeGroup.lift P.val `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 +lemma 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 +lemma 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 = ⊤ := +lemma 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⟩ +lemma 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 +lemma 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 +lemma 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 := +lemma 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 := +lemma 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`. -/ From a1801692eb6b4f330bb39630408faaddca48f292 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Mon, 20 Jul 2026 18:34:49 +0100 Subject: [PATCH 4/6] transport `rw`, quantify over `Set` for `Group.FG` bridge --- Mathlib/GroupTheory/Presentation.lean | 33 +++++++++++++++------------ 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean index de9e518d675d7f..5773afe689e5e4 100644 --- a/Mathlib/GroupTheory/Presentation.lean +++ b/Mathlib/GroupTheory/Presentation.lean @@ -64,23 +64,26 @@ variable (P : Group.Generators G α) @[simp] lemma range_lift_eq_top : (FreeGroup.lift P.val).range = ⊤ := by - rw [FreeGroup.range_lift_eq_closure]; exact P.closure_eq_top + 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]; exact h + 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]; exact Subgroup.closure_univ + closure_eq_top := by rw [Set.range_id, Subgroup.closure_univ] @[simp] lemma val_self : (self G).val = id := rfl @@ -91,16 +94,16 @@ theorem fg [Finite α] (P : Group.Generators G α) : Group.FG G := end Group.Generators -/-- A group is finitely generated if and only if it admits a finite generating set. -/ +/-- 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 ↔ ∃ (α : Type) (_ : Finite α), Nonempty (Group.Generators G α) := by - rw [Group.fg_iff_exists_freeGroup_hom_surjective_finite] + Group.FG G ↔ ∃ (S : Set G) (_ : S.Finite), Nonempty (Group.Generators G S) := by constructor - · rintro ⟨α, hα, φ, hφ⟩ - obtain ⟨v, rfl⟩ := FreeGroup.lift.surjective φ - exact ⟨α, hα, ⟨Group.Generators.ofLiftSurjective v hφ⟩⟩ - · rintro ⟨α, hα, ⟨P⟩⟩ - exact ⟨α, hα, FreeGroup.lift P.val, P.lift_surjective⟩ + · 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 kernel of the free group over @@ -144,9 +147,9 @@ 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 rw [P.ker_lift]; exact Subgroup.subset_normalClosure hr) + MonoidHom.mem_ker.mp (by simpa [P.ker_lift] using Subgroup.subset_normalClosure hr) -lemma lift_rel (r : ρ) : P.lift (P.rel r) = 1 := +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`. -/ @@ -170,10 +173,10 @@ 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⟩ + 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_val]; exact hsφ.symm }⟩⟩ + ker_eq_normalClosure := by rw [Subtype.range_coe]; exact hsφ.symm }⟩⟩ From 5a49e3f7dda9d0c0ea7059a7f1b644f492cc1213 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Mon, 20 Jul 2026 23:26:52 +0100 Subject: [PATCH 5/6] doc: polish Group.Presentation docstrings, make presentedGroupEquiv_of a lemma Reword the `Group.Presentation` structure and `ker_eq_normalClosure` docstrings for clarity, simplify the `isFinitelyPresented_iff` docstring, and change `presentedGroupEquiv_of` from `theorem` to `lemma`. Co-Authored-By: Claude Opus 4.8 (1M context) --- Mathlib/GroupTheory/Presentation.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean index 5773afe689e5e4..361a9f012ef7b5 100644 --- a/Mathlib/GroupTheory/Presentation.lean +++ b/Mathlib/GroupTheory/Presentation.lean @@ -105,16 +105,17 @@ theorem Group.fg_iff_nonempty_finite_generators : 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 kernel of the free group over -the generators `FreeGroup.lift val` is given by the normal closure of the relations. -/ +/-- 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 the - full kernel of `FreeGroup.lift val`, so no relation holds in `G` beyond their consequences. -/ + /-- 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) @@ -157,9 +158,8 @@ 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 : α) : +lemma presentedGroupEquiv_of (a : α) : P.presentedGroupEquiv (PresentedGroup.of a) = P.val a := P.lift_of a /-- A finite presentation is finitely presented. -/ @@ -168,7 +168,7 @@ theorem isFinitelyPresented [Finite α] [Finite ρ] (P : Group.Presentation G α end Group.Presentation -/-- A group is finitely presented if and only if it admits a `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 ↔ From 6eb8cdb866d0ae4228089c1ed6944ca6f2d92d65 Mon Sep 17 00:00:00 2001 From: Hang Lu Su Date: Wed, 22 Jul 2026 09:09:23 +0100 Subject: [PATCH 6/6] change `Presentation` def to `rel: Set` --- Mathlib/GroupTheory/Presentation.lean | 61 +++++++++++---------------- 1 file changed, 24 insertions(+), 37 deletions(-) diff --git a/Mathlib/GroupTheory/Presentation.lean b/Mathlib/GroupTheory/Presentation.lean index 361a9f012ef7b5..aac45e05fa6b2d 100644 --- a/Mathlib/GroupTheory/Presentation.lean +++ b/Mathlib/GroupTheory/Presentation.lean @@ -19,20 +19,20 @@ 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 α` +* `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_iff_exists_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 ρ]`. + finite when `[Finite α]`, a presentation when `[Finite α] [Finite P.rel]`. * This file is multiplicative only: `PresentedGroup` has no additive counterpart and there is no `to_additive`-generated `AddGroup.Presentation` so far. @@ -47,7 +47,7 @@ group presentation, generators and relations @[expose] public section -variable {G α ρ : Type*} [Group G] +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 @@ -105,31 +105,27 @@ theorem Group.fg_iff_nonempty_finite_generators : 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 +/-- A group presentation is given by a generating family (`val : α → G`) and a set of relators +(`rel : Set (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*) +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 set of relators, as words in the free group; each `r ∈ rel` is read as `r = 1` + in the sense that it is meant to evaluate to the identity in `G`. -/ + rel : Set (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) + (FreeGroup.lift val).ker = Subgroup.normalClosure rel namespace Group.Presentation -variable (P : Group.Presentation G α ρ) +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] @@ -139,22 +135,13 @@ lemma lift_of (a : α) : P.lift (FreeGroup.of a) = P.val a := FreeGroup.lift_app 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.rel := P.ker_eq_normalClosure -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 := +theorem lift_eq_one_of_mem_rel {r : FreeGroup α} (hr : r ∈ P.rel) : 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 := +/-- The `G` with presentation `P` is isomorphic to the `PresentedGroup` given by `P.rel`. -/ +noncomputable def presentedGroupEquiv : PresentedGroup P.rel ≃* G := (QuotientGroup.quotientMulEquivOfEq P.ker_lift.symm).trans (QuotientGroup.quotientKerEquivOfSurjective P.lift P.lift_surjective') @@ -163,20 +150,20 @@ 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 α ρ) : +theorem isFinitelyPresented [Finite α] (P : Group.Presentation G α) [Finite P.rel] : 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 : +theorem Group.isFinitelyPresented_iff_exists_finite_presentation : Group.IsFinitelyPresented G ↔ - ∃ (α ρ : Type) (_ : Finite α) (_ : Finite ρ), Nonempty (Group.Presentation G α ρ) := by - refine ⟨fun h ↦ ?_, fun ⟨_, _, _, _, ⟨P⟩⟩ ↦ P.isFinitelyPresented⟩ + ∃ (α : Type) (_ : Finite α) (P : Group.Presentation G α), P.rel.Finite := by + refine ⟨fun h ↦ ?_, fun ⟨_, _, P, hP⟩ ↦ have := hP.to_subtype; 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 }⟩⟩ + exact ⟨Fin n, inferInstance, + { toGenerators := Group.Generators.ofLiftSurjective v hφ + rel := s + ker_eq_normalClosure := hsφ.symm }, hs⟩