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..361a9f012ef7b5 --- /dev/null +++ b/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 }⟩⟩ 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},