-
Notifications
You must be signed in to change notification settings - Fork 238
/
Adjunctions.lean
225 lines (187 loc) · 7.76 KB
/
Adjunctions.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johannes Hölzl
-/
import Mathlib.Algebra.Category.GroupCat.Basic
import Mathlib.GroupTheory.FreeAbelianGroup
#align_import algebra.category.Group.adjunctions from "leanprover-community/mathlib"@"ecef68622cf98f6d42c459e5b5a079aeecdd9842"
/-!
# Adjunctions regarding the category of (abelian) groups
This file contains construction of basic adjunctions concerning the category of groups and the
category of abelian groups.
## Main definitions
* `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 `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.
-/
set_option linter.uppercaseLean3 false -- `AddCommGroup`
noncomputable section
universe u
open CategoryTheory
namespace AddCommGroupCat
open scoped Classical
/-- The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
free abelian group with generators `x : X`.
-/
def free : Type u ⥤ AddCommGroupCat where
obj α := of (FreeAbelianGroup α)
map := FreeAbelianGroup.map
map_id _ := AddMonoidHom.ext FreeAbelianGroup.map_id_apply
map_comp _ _ := AddMonoidHom.ext FreeAbelianGroup.map_comp_apply
#align AddCommGroup.free AddCommGroupCat.free
@[simp]
theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = FreeAbelianGroup α :=
rfl
#align AddCommGroup.free_obj_coe AddCommGroupCat.free_obj_coe
@[simp]
theorem free_map_coe {α β : Type u} {f : α → β} (x : FreeAbelianGroup α) :
(free.map f) x = f <$> x :=
rfl
#align AddCommGroup.free_map_coe AddCommGroupCat.free_map_coe
/-- The free-forgetful adjunction for abelian groups.
-/
def adj : free ⊣ forget AddCommGroupCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun X G => FreeAbelianGroup.lift.symm
-- Porting note: used to be just `by intros; ext; rfl`.
homEquiv_naturality_left_symm := by
intros
ext
simp only [Equiv.symm_symm]
apply FreeAbelianGroup.lift_comp }
#align AddCommGroup.adj AddCommGroupCat.adj
instance : IsRightAdjoint (forget AddCommGroupCat.{u}) :=
⟨_, adj⟩
/-- As an example, we now give a high-powered proof that
the monomorphisms in `AddCommGroup` are just the injective functions.
(This proof works in all universes.)
-/
-- Porting note: had to elaborate instance of Mono rather than just using `apply_instance`.
example {G H : AddCommGroupCat.{u}} (f : G ⟶ H) [Mono f] : Function.Injective f :=
(mono_iff_injective (FunLike.coe f)).mp (Functor.map_mono (forget AddCommGroupCat) f)
end AddCommGroupCat
namespace GroupCat
/-- The free functor `Type u ⥤ Group` sending a type `X` to the free group with generators `x : X`.
-/
def free : Type u ⥤ GroupCat where
obj α := of (FreeGroup α)
map := FreeGroup.map
map_id := by
intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
map_comp := by
intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
#align Group.free GroupCat.free
/-- The free-forgetful adjunction for groups.
-/
def adj : free ⊣ forget GroupCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun X G => FreeGroup.lift.symm
-- Porting note: used to be just `by intros; ext1; rfl`.
homEquiv_naturality_left_symm := by
intros
ext1
simp only [Equiv.symm_symm]
apply Eq.symm
apply FreeGroup.lift.unique
intros
apply FreeGroup.lift.of }
#align Group.adj GroupCat.adj
instance : IsRightAdjoint (forget GroupCat.{u}) :=
⟨_, adj⟩
end GroupCat
section Abelianization
/-- The abelianization functor `Group ⥤ CommGroup` sending a group `G` to its abelianization `Gᵃᵇ`.
-/
def abelianize : GroupCat.{u} ⥤ CommGroupCat.{u} where
obj G :=
{ α := Abelianization G
str := by infer_instance }
map f :=
Abelianization.lift
{ toFun := fun x => Abelianization.of (f x)
map_one' := by simp
map_mul' := by simp }
map_id := by
intros; simp only [MonoidHom.mk_coe, coe_id]
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr; rfl
map_comp := by
intros; simp only [coe_comp];
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr; rfl
#align abelianize abelianize
/-- The abelianization-forgetful adjuction from `Group` to `CommGroup`.-/
def abelianizeAdj : abelianize ⊣ forget₂ CommGroupCat.{u} GroupCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun G A => Abelianization.lift.symm
-- Porting note: used to be just `by intros; ext1; rfl`.
homEquiv_naturality_left_symm := by
intros
ext1
simp only [Equiv.symm_symm]
apply Eq.symm
apply Abelianization.lift.unique
intros
apply Abelianization.lift.of }
#align abelianize_adj abelianizeAdj
end Abelianization
/-- The functor taking a monoid to its subgroup of units. -/
@[simps]
def MonCat.units : MonCat.{u} ⥤ GroupCat.{u} where
obj R := GroupCat.of Rˣ
map f := GroupCat.ofHom <| Units.map f
map_id _ := MonoidHom.ext fun _ => Units.ext rfl
map_comp _ _ := MonoidHom.ext fun _ => Units.ext rfl
#align Mon.units MonCat.units
/-- The forgetful-units adjunction between `Group` and `Mon`. -/
def GroupCat.forget₂MonAdj : forget₂ GroupCat MonCat ⊣ MonCat.units.{u} where
homEquiv X Y :=
{ toFun := fun f => MonoidHom.toHomUnits f
invFun := fun f => (Units.coeHom Y).comp f
left_inv := fun f => MonoidHom.ext fun _ => rfl
right_inv := fun f => MonoidHom.ext fun _ => Units.ext rfl }
unit :=
{ app := fun X => { (@toUnits X _).toMonoidHom with }
naturality := fun X Y f => MonoidHom.ext fun x => Units.ext rfl }
counit :=
{ app := fun X => Units.coeHom X
naturality := by intros; exact MonoidHom.ext fun x => rfl }
homEquiv_unit := MonoidHom.ext fun _ => Units.ext rfl
homEquiv_counit := MonoidHom.ext fun _ => rfl
#align Group.forget₂_Mon_adj GroupCat.forget₂MonAdj
instance : IsRightAdjoint MonCat.units.{u} :=
⟨_, GroupCat.forget₂MonAdj⟩
/-- The functor taking a monoid to its subgroup of units. -/
@[simps]
def CommMonCat.units : CommMonCat.{u} ⥤ CommGroupCat.{u} where
obj R := CommGroupCat.of Rˣ
map f := CommGroupCat.ofHom <| Units.map f
map_id _ := MonoidHom.ext fun _ => Units.ext rfl
map_comp _ _ := MonoidHom.ext fun _ => Units.ext rfl
#align CommMon.units CommMonCat.units
/-- The forgetful-units adjunction between `CommGroup` and `CommMon`. -/
def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMonCat ⊣ CommMonCat.units.{u} where
homEquiv X Y :=
{ toFun := fun f => MonoidHom.toHomUnits f
invFun := fun f => (Units.coeHom Y).comp f
left_inv := fun f => MonoidHom.ext fun _ => rfl
right_inv := fun f => MonoidHom.ext fun _ => Units.ext rfl }
unit :=
{ app := fun X => { (@toUnits X _).toMonoidHom with }
naturality := fun X Y f => MonoidHom.ext fun x => Units.ext rfl }
counit :=
{ app := fun X => Units.coeHom X
naturality := by intros; exact MonoidHom.ext fun x => rfl }
homEquiv_unit := MonoidHom.ext fun _ => Units.ext rfl
homEquiv_counit := MonoidHom.ext fun _ => rfl
#align CommGroup.forget₂_CommMon_adj CommGroupCat.forget₂CommMonAdj
instance : IsRightAdjoint CommMonCat.units.{u} :=
⟨_, CommGroupCat.forget₂CommMonAdj⟩