From b0aae27376031a3d40e77c114d68ad1de144068e Mon Sep 17 00:00:00 2001 From: Julian-Kuelshammer Date: Sat, 13 Feb 2021 22:35:47 +0000 Subject: [PATCH] feat(algebra/category/Group/adjunctions): free_group-forgetful adjunction (#6190) Furthermore, a module doc for `group_theory/free_group` is provided and a few lines in this file are split. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com> --- src/algebra/category/Group/adjunctions.lean | 35 ++++++++-- src/group_theory/free_group.lean | 75 ++++++++++++++++----- 2 files changed, 88 insertions(+), 22 deletions(-) diff --git a/src/algebra/category/Group/adjunctions.lean b/src/algebra/category/Group/adjunctions.lean index 3d20b876b8351..20615c2de1223 100644 --- a/src/algebra/category/Group/adjunctions.lean +++ b/src/algebra/category/Group/adjunctions.lean @@ -14,15 +14,19 @@ category of abelian groups. ## Main definitions -* `free`: constructs the functor associating to a type `X` the free abelian group with generators - `x : X` +* `AddCommGroup.free`: constructs the functor associating to a type `X` the free abelian group with + generators `x : X`. +* `Group.free`: constructs the functor associating to a type `X` the free group with + generators `x : X`. * `abelianize`: constructs the functor which associates to a group `G` its abelianization `Gᵃᵇ`. ## Main statements -* `AddCommGroup.adj` proves that `free` is the left adjoint of the forgetful functor from abelian - groups to types. -* `abelianize_adj` proves that `abelianize` is left adjoint to the forgetful functor from +* `AddCommGroup.adj`: proves that `AddCommGroup.free` is the left adjoint of the forgetful functor + from abelian groups to types. +* `Group.adj`: proves that `Group.free` is the left adjoint of the forgetful functor from groups to + types. +* `abelianize_adj`: proves that `abelianize` is left adjoint to the forgetful functor from abelian groups to groups. -/ @@ -73,6 +77,25 @@ example {G H : AddCommGroup.{u}} (f : G ⟶ H) [mono f] : function.injective f : end AddCommGroup +namespace Group + +/-- The free functor `Type u ⥤ Group` sending a type `X` to the free group with generators `x : X`. +-/ +def free : Type u ⥤ Group := +{ obj := λ α, of (free_group α), + map := λ X Y, free_group.map, + map_id' := by { intros, ext1, refl }, + map_comp' := by { intros, ext1, refl } } + +/-- The free-forgetful adjunction for groups. +-/ +def adj : free ⊣ forget Group.{u} := +adjunction.mk_of_hom_equiv +{ hom_equiv := λ X G, (free_group.lift X G).symm, + hom_equiv_naturality_left_symm' := λ X Y G f g, begin ext1, refl end } + +end Group + section abelianization /-- The abelianization functor `Group ⥤ CommGroup` sending a group `G` to its abelianization `Gᵃᵇ`. @@ -83,7 +106,7 @@ def abelianize : Group.{u} ⥤ CommGroup.{u} := map_one' := by simp, map_mul' := by simp } ), map_id' := by { intros, simp only [monoid_hom.mk_coe, coe_id], ext1, refl }, - map_comp' := by { intros, simp, ext1, refl } } + map_comp' := by { intros, simp only [coe_comp], ext1, refl } } /-- The abelianization-forgetful adjuction from `Group` to `CommGroup`.-/ def abelianize_adj : abelianize ⊣ forget₂ CommGroup.{u} Group.{u} := diff --git a/src/group_theory/free_group.lean b/src/group_theory/free_group.lean index 8a4fb7bdb48c9..a44c6c866963b 100644 --- a/src/group_theory/free_group.lean +++ b/src/group_theory/free_group.lean @@ -2,19 +2,45 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau +-/ +import data.fintype.basic +import group_theory.subgroup + +/-! +# Free groups + +This file defines free groups over a type. Furthermore, it is shown that the free group construction +is an instance of a monad. For the result that `free_group` is the left adjoint to the forgetful +functor from groups to types, see `algebra/category/Group/adjunctions`. + +## Main definitions + +* `free_group`: the free group associated to a type `α` defined as the words over `a : α × bool ` + modulo the relation `a * x * x⁻¹ * b = a * b`. +* `mk`: the canonical quotient map `list (α × bool) → free_group α`. +* `of`: the canoical injection `α → free_group α`. +* `to_group f`: the canonical group homomorphism `free_group α →* G` given a group `G` and a + function `f : α → G`. + +## Main statements -Free groups as a quotient over the reduction relation `a * x * x⁻¹ * b = a * b`. +* `church_rosser`: The Church-Rosser theorem for word reduction (also known as Newman's diamond + lemma). +* `free_group_unit_equiv_int`: The free group over the one-point type is isomorphic to the integers. +* The free group construction is an instance of a monad. -First we introduce the one step reduction relation - `free_group.red.step`: w * x * x⁻¹ * v ~> w * v -its reflexive transitive closure: - `free_group.red.trans` -and proof that its join is an equivalence relation. +## Implementation details -Then we introduce `free_group α` as a quotient over `free_group.red.step`. +First we introduce the one step reduction relation `free_group.red.step`: +`w * x * x⁻¹ * v ~> w * v`, its reflexive transitive closure `free_group.red.trans` +and prove that its join is an equivalence relation. Then we introduce `free_group α` as a quotient +over `free_group.red.step`. + +## Tags + +free group, Newman's diamond lemma, Church-Rosser theorem -/ -import data.fintype.basic -import group_theory.subgroup + open relation universes u v w @@ -126,7 +152,8 @@ lemma step.to_red : step L₁ L₂ → red L₁ L₂ := refl_trans_gen.single /-- Church-Rosser theorem for word reduction: If `w1 w2 w3` are words such that `w1` reduces to `w2` -and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4` respectively. -/ +and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4` +respectively. This is also known as Newman's diamond lemma. -/ theorem church_rosser : red L₁ L₂ → red L₁ L₃ → join red L₂ L₃ := relation.church_rosser (assume a b c hab hac, match b, c, red.step.diamond hab hac rfl with @@ -173,11 +200,13 @@ iff.intro { exact ⟨_, _, eq.symm, by refl, by refl⟩ }, { cases h with s e a b, rcases list.append_eq_append_iff.1 eq with ⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩, - { have : L₁ ++ (s' ++ ((a, b) :: (a, bnot b) :: e)) = (L₁ ++ s') ++ ((a, b) :: (a, bnot b) :: e), + { have : L₁ ++ (s' ++ ((a, b) :: (a, bnot b) :: e)) = + (L₁ ++ s') ++ ((a, b) :: (a, bnot b) :: e), { simp }, rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩, exact ⟨w₁, w₂, rfl, h₁, h₂.tail step.bnot⟩ }, - { have : (s ++ ((a, b) :: (a, bnot b) :: e')) ++ L₂ = s ++ ((a, b) :: (a, bnot b) :: (e' ++ L₂)), + { have : (s ++ ((a, b) :: (a, bnot b) :: e')) ++ L₂ = + s ++ ((a, b) :: (a, bnot b) :: (e' ++ L₂)), { simp }, rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩, exact ⟨w₁, w₂, rfl, h₁.tail step.bnot, h₂⟩ }, } @@ -351,7 +380,7 @@ instance : group (free_group α) := mul_left_inv := by rintros ⟨L⟩; exact (list.rec_on L rfl $ λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih) } -/-- `of x` is the canonical injection from the type to the free group over that type by sending each +/-- `of` is the canonical injection from the type to the free group over that type by sending each element to the equivalence class of the letter that is the element. -/ def of (x : α) : free_group α := mk [(x, tt)] @@ -453,6 +482,18 @@ set.subset.antisymm end to_group +section +variables (X : Type*) (G : Type*) [group G] + +/-- The bijection underlying the free-forgetful adjunction for groups. -/ +@[simps] +def lift : (X → G) ≃ (free_group X →* G) := +{ to_fun := λ g, to_group g, + inv_fun := λ f, f.1 ∘ of, + left_inv := by { intros x, ext1, simp }, + right_inv := by { intros x, ext1, simp } } +end + section map variables {β : Type v} (f : α → β) {x y : free_group α} @@ -592,7 +633,7 @@ def free_group_empty_equiv_unit : free_group empty ≃ unit := right_inv := λ ⟨⟩, rfl } /-- The bijection between the free group on a singleton, and the integers. -/ -def free_group_unit_equiv_int : free_group unit ≃ int := +def free_group_unit_equiv_int : free_group unit ≃ ℤ := { to_fun := λ x, sum begin revert x, apply monoid_hom.to_fun, apply map (λ _, (1 : ℤ)), @@ -648,7 +689,8 @@ to_group.of @[simp] lemma one_bind (f : α → free_group β) : 1 >>= f = 1 := (to_group f).map_one -@[simp] lemma mul_bind (f : α → free_group β) (x y : free_group α) : x * y >>= f = (x >>= f) * (y >>= f) := +@[simp] lemma mul_bind (f : α → free_group β) (x y : free_group α) : + x * y >>= f = (x >>= f) * (y >>= f) := (to_group f).map_mul _ _ @[simp] lemma inv_bind (f : α → free_group β) (x : free_group α) : x⁻¹ >>= f = (x >>= f)⁻¹ := @@ -713,7 +755,8 @@ begin exact red.cons_cons ih } } } end -theorem reduce.not {p : Prop} : ∀ {L₁ L₂ L₃ : list (α × bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → p +theorem reduce.not {p : Prop} : + ∀ {L₁ L₂ L₃ : list (α × bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → p | [] L2 L3 _ _ := λ h, by cases L2; injections | ((x,b)::L1) L2 L3 x' b' := begin dsimp,