Skip to content

Commit ac81fdb

Browse files
jjaassoonnjjaassoonn
committed
feat: port Algebra.Category.Group.FilteredColimits (#4274)
1 parent 8161656 commit ac81fdb

File tree

2 files changed

+306
-0
lines changed

2 files changed

+306
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ import Mathlib.Algebra.Bounds
3333
import Mathlib.Algebra.Category.GroupCat.Basic
3434
import Mathlib.Algebra.Category.GroupCat.EpiMono
3535
import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup
36+
import Mathlib.Algebra.Category.GroupCat.FilteredColimits
3637
import Mathlib.Algebra.Category.GroupCat.Injective
3738
import Mathlib.Algebra.Category.GroupCat.Limits
3839
import Mathlib.Algebra.Category.GroupCat.Preadditive

‎Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean‎

Lines changed: 305 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,305 @@
1+
/-
2+
Copyright (c) 2021 Justus Springer. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Justus Springer
5+
6+
! This file was ported from Lean 3 source module algebra.category.Group.filtered_colimits
7+
! leanprover-community/mathlib commit c43486ecf2a5a17479a32ce09e4818924145e90e
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Algebra.Category.GroupCat.Basic
12+
import Mathlib.Algebra.Category.Mon.FilteredColimits
13+
14+
/-!
15+
# The forgetful functor from (commutative) (additive) groups preserves filtered colimits.
16+
17+
Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
18+
to preserve _filtered_ colimits.
19+
20+
In this file, we start with a small filtered category `J` and a functor `F : J ⥤ Group`.
21+
We show that the colimit of `F ⋙ forget₂ Group Mon` (in `Mon`) carries the structure of a group,
22+
thereby showing that the forgetful functor `forget₂ Group Mon` preserves filtered colimits. In
23+
particular, this implies that `forget Group` preserves filtered colimits. Similarly for `AddGroup`,
24+
`CommGroup` and `AddCommGroup`.
25+
26+
-/
27+
28+
29+
universe v u
30+
31+
noncomputable section
32+
33+
open Classical
34+
35+
open CategoryTheory
36+
37+
open CategoryTheory.Limits
38+
39+
open CategoryTheory.IsFiltered renaming max → max'
40+
41+
-- avoid name collision with `_root_.max`.
42+
namespace GroupCat.FilteredColimits
43+
44+
section
45+
46+
open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
47+
48+
-- We use parameters here, mainly so we can have the abbreviations `G` and `G.mk` below, without
49+
-- passing around `F` all the time.
50+
variable {J : Type v}[SmallCategory J] [IsFiltered J] (F : J ⥤ GroupCat.{max v u})
51+
52+
/-- The colimit of `F ⋙ forget₂ Group Mon` in the category `Mon`.
53+
In the following, we will show that this has the structure of a group.
54+
-/
55+
@[to_additive
56+
"The colimit of `F ⋙ forget₂ AddGroup AddMon` in the category `AddMon`.
57+
In the following, we will show that this has the structure of an additive group."]
58+
noncomputable abbrev G : MonCat :=
59+
MonCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ GroupCat MonCat.{max v u})
60+
set_option linter.uppercaseLean3 false in
61+
#align Group.filtered_colimits.G GroupCat.FilteredColimits.G
62+
set_option linter.uppercaseLean3 false in
63+
#align AddGroup.filtered_colimits.G AddGroupCat.FilteredColimits.G
64+
65+
/-- The canonical projection into the colimit, as a quotient type. -/
66+
@[to_additive "The canonical projection into the colimit, as a quotient type."]
67+
abbrev G.mk : (Σ j, F.obj j) → G.{v, u} F :=
68+
Quot.mk (Types.Quot.Rel.{v, u} (F ⋙ forget GroupCat.{max v u}))
69+
set_option linter.uppercaseLean3 false in
70+
#align Group.filtered_colimits.G.mk GroupCat.FilteredColimits.G.mk
71+
set_option linter.uppercaseLean3 false in
72+
#align AddGroup.filtered_colimits.G.mk AddGroupCat.FilteredColimits.G.mk
73+
74+
@[to_additive]
75+
theorem G.mk_eq (x y : Σ j, F.obj j)
76+
(h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
77+
G.mk.{v, u} F x = G.mk F y :=
78+
Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget GroupCat) x y h)
79+
set_option linter.uppercaseLean3 false in
80+
#align Group.filtered_colimits.G.mk_eq GroupCat.FilteredColimits.G.mk_eq
81+
set_option linter.uppercaseLean3 false in
82+
#align AddGroup.filtered_colimits.G.mk_eq AddGroupCat.FilteredColimits.G.mk_eq
83+
84+
/-- The "unlifted" version of taking inverses in the colimit. -/
85+
@[to_additive "The \"unlifted\" version of negation in the colimit."]
86+
def colimitInvAux (x : Σ j, F.obj j) : G.{v, u} F :=
87+
G.mk F ⟨x.1, x.2⁻¹⟩
88+
set_option linter.uppercaseLean3 false in
89+
#align Group.filtered_colimits.colimit_inv_aux GroupCat.FilteredColimits.colimitInvAux
90+
set_option linter.uppercaseLean3 false in
91+
#align AddGroup.filtered_colimits.colimit_neg_aux AddGroupCat.FilteredColimits.colimitNegAux
92+
93+
@[to_additive]
94+
theorem colimitInvAux_eq_of_rel (x y : Σ j, F.obj j)
95+
(h : Types.FilteredColimit.Rel.{v, u} (F ⋙ forget GroupCat) x y) :
96+
colimitInvAux.{v, u} F x = colimitInvAux F y := by
97+
apply G.mk_eq
98+
obtain ⟨k, f, g, hfg⟩ := h
99+
use k, f, g
100+
rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
101+
exact hfg
102+
set_option linter.uppercaseLean3 false in
103+
#align Group.filtered_colimits.colimit_inv_aux_eq_of_rel GroupCat.FilteredColimits.colimitInvAux_eq_of_rel
104+
set_option linter.uppercaseLean3 false in
105+
#align AddGroup.filtered_colimits.colimit_neg_aux_eq_of_rel AddGroupCat.FilteredColimits.colimitNegAux_eq_of_rel
106+
107+
/-- Taking inverses in the colimit. See also `colimit_inv_aux`. -/
108+
@[to_additive "Negation in the colimit. See also `colimit_neg_aux`."]
109+
instance colimitInv : Inv (G.{v, u} F) where
110+
inv x := by
111+
refine' Quot.lift (colimitInvAux.{v, u} F) _ x
112+
intro x y h
113+
apply colimitInvAux_eq_of_rel
114+
apply Types.FilteredColimit.rel_of_quot_rel
115+
exact h
116+
set_option linter.uppercaseLean3 false in
117+
#align Group.filtered_colimits.colimit_has_inv GroupCat.FilteredColimits.colimitInv
118+
set_option linter.uppercaseLean3 false in
119+
#align AddGroup.filtered_colimits.colimit_has_neg AddGroupCat.FilteredColimits.colimitNeg
120+
121+
@[to_additive (attr := simp)]
122+
theorem colimit_inv_mk_eq (x : Σ j, F.obj j) : (G.mk.{v, u} F x)⁻¹ = G.mk F ⟨x.1, x.2⁻¹⟩ :=
123+
rfl
124+
set_option linter.uppercaseLean3 false in
125+
#align Group.filtered_colimits.colimit_inv_mk_eq GroupCat.FilteredColimits.colimit_inv_mk_eq
126+
set_option linter.uppercaseLean3 false in
127+
#align AddGroup.filtered_colimits.colimit_neg_mk_eq AddGroupCat.FilteredColimits.colimit_neg_mk_eq
128+
129+
@[to_additive]
130+
noncomputable instance colimitGroup : Group (G.{v, u} F) :=
131+
{ colimitInv.{v, u} F, (G.{v, u} F).str with
132+
mul_left_inv := fun x => by
133+
refine Quot.inductionOn x ?_; clear x; intro x
134+
cases' x with j x
135+
erw [colimit_inv_mk_eq,
136+
colimit_mul_mk_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
137+
colimit_one_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) j]
138+
dsimp
139+
erw [CategoryTheory.Functor.map_id, mul_left_inv] }
140+
set_option linter.uppercaseLean3 false in
141+
#align Group.filtered_colimits.colimit_group GroupCat.FilteredColimits.colimitGroup
142+
set_option linter.uppercaseLean3 false in
143+
#align AddGroup.filtered_colimits.colimit_add_group AddGroupCat.FilteredColimits.colimitAddGroup
144+
145+
/-- The bundled group giving the filtered colimit of a diagram. -/
146+
@[to_additive "The bundled additive group giving the filtered colimit of a diagram."]
147+
noncomputable def colimit : GroupCat.{max v u} :=
148+
GroupCat.of (G.{v, u} F)
149+
set_option linter.uppercaseLean3 false in
150+
#align Group.filtered_colimits.colimit GroupCat.FilteredColimits.colimit
151+
set_option linter.uppercaseLean3 false in
152+
#align AddGroup.filtered_colimits.colimit AddGroupCat.FilteredColimits.colimit
153+
154+
/-- The cocone over the proposed colimit group. -/
155+
@[to_additive "The cocone over the proposed colimit additive group."]
156+
noncomputable def colimitCocone : Cocone F where
157+
pt := colimit.{v, u} F
158+
ι := { (MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ GroupCat MonCat.{max v u})).ι with }
159+
set_option linter.uppercaseLean3 false in
160+
#align Group.filtered_colimits.colimit_cocone GroupCat.FilteredColimits.colimitCocone
161+
set_option linter.uppercaseLean3 false in
162+
#align AddGroup.filtered_colimits.colimit_cocone AddGroupCat.FilteredColimits.colimitCocone
163+
164+
/-- The proposed colimit cocone is a colimit in `Group`. -/
165+
@[to_additive "The proposed colimit cocone is a colimit in `AddGroup`."]
166+
def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
167+
desc t :=
168+
MonCat.FilteredColimits.colimitDesc.{v, u} (F ⋙ forget₂ GroupCat MonCat.{max v u})
169+
((forget₂ GroupCat MonCat).mapCocone t)
170+
fac t j :=
171+
FunLike.coe_injective <|
172+
(Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget GroupCat)).fac
173+
((forget GroupCat).mapCocone t) j
174+
uniq t _ h :=
175+
FunLike.coe_injective' <|
176+
(Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget GroupCat)).uniq
177+
((forget GroupCat).mapCocone t) _
178+
fun j => funext fun x => FunLike.congr_fun (h j) x
179+
set_option linter.uppercaseLean3 false in
180+
#align Group.filtered_colimits.colimit_cocone_is_colimit GroupCat.FilteredColimits.colimitCoconeIsColimit
181+
set_option linter.uppercaseLean3 false in
182+
#align AddGroup.filtered_colimits.colimit_cocone_is_colimit AddGroupCat.FilteredColimits.colimitCoconeIsColimit
183+
184+
@[to_additive forget₂AddMonPreservesFilteredColimits]
185+
noncomputable instance forget₂MonPreservesFilteredColimits :
186+
PreservesFilteredColimits.{u} (forget₂ GroupCat.{u} MonCat.{u}) where
187+
preserves_filtered_colimits := fun x hx1 _ => letI : Category.{u, u} x := hx1
188+
⟨fun {F} => preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
189+
(MonCat.FilteredColimits.colimitCoconeIsColimit.{u, u} _)⟩
190+
set_option linter.uppercaseLean3 false in
191+
#align Group.filtered_colimits.forget₂_Mon_preserves_filtered_colimits GroupCat.FilteredColimits.forget₂MonPreservesFilteredColimits
192+
set_option linter.uppercaseLean3 false in
193+
#align AddGroup.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits AddGroupCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits
194+
195+
@[to_additive]
196+
noncomputable instance forgetPreservesFilteredColimits :
197+
PreservesFilteredColimits (forget GroupCat.{u}) :=
198+
Limits.compPreservesFilteredColimits (forget₂ GroupCat MonCat) (forget MonCat.{u})
199+
set_option linter.uppercaseLean3 false in
200+
#align Group.filtered_colimits.forget_preserves_filtered_colimits GroupCat.FilteredColimits.forgetPreservesFilteredColimits
201+
set_option linter.uppercaseLean3 false in
202+
#align AddGroup.filtered_colimits.forget_preserves_filtered_colimits AddGroupCat.FilteredColimits.forgetPreservesFilteredColimits
203+
204+
end
205+
206+
end GroupCat.FilteredColimits
207+
208+
namespace CommGroupCat.FilteredColimits
209+
210+
section
211+
212+
-- We use parameters here, mainly so we can have the abbreviation `G` below, without
213+
-- passing around `F` all the time.
214+
variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ CommGroupCat.{max v u})
215+
216+
/-- The colimit of `F ⋙ forget₂ CommGroup Group` in the category `Group`.
217+
In the following, we will show that this has the structure of a _commutative_ group.
218+
-/
219+
@[to_additive
220+
"The colimit of `F ⋙ forget₂ AddCommGroup AddGroup` in the category `AddGroup`.
221+
In the following, we will show that this has the structure of a _commutative_ additive group."]
222+
noncomputable abbrev G : GroupCat.{max v u} :=
223+
GroupCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ CommGroupCat.{max v u} GroupCat.{max v u})
224+
set_option linter.uppercaseLean3 false in
225+
#align CommGroup.filtered_colimits.G CommGroupCat.FilteredColimits.G
226+
set_option linter.uppercaseLean3 false in
227+
#align AddCommGroup.filtered_colimits.G AddCommGroupCat.FilteredColimits.G
228+
229+
@[to_additive]
230+
noncomputable instance colimitCommGroup : CommGroup.{max v u} (G.{v, u} F) :=
231+
{ (G F).str,
232+
CommMonCat.FilteredColimits.colimitCommMonoid
233+
(F ⋙ forget₂ CommGroupCat CommMonCat.{max v u}) with }
234+
set_option linter.uppercaseLean3 false in
235+
#align CommGroup.filtered_colimits.colimit_comm_group CommGroupCat.FilteredColimits.colimitCommGroup
236+
set_option linter.uppercaseLean3 false in
237+
#align AddCommGroup.filtered_colimits.colimit_add_comm_group AddCommGroupCat.FilteredColimits.colimitAddCommGroup
238+
239+
/-- The bundled commutative group giving the filtered colimit of a diagram. -/
240+
@[to_additive "The bundled additive commutative group giving the filtered colimit of a diagram."]
241+
noncomputable def colimit : CommGroupCat :=
242+
CommGroupCat.of (G.{v, u} F)
243+
set_option linter.uppercaseLean3 false in
244+
#align CommGroup.filtered_colimits.colimit CommGroupCat.FilteredColimits.colimit
245+
set_option linter.uppercaseLean3 false in
246+
#align AddCommGroup.filtered_colimits.colimit AddCommGroupCat.FilteredColimits.colimit
247+
248+
/-- The cocone over the proposed colimit commutative group. -/
249+
@[to_additive "The cocone over the proposed colimit additive commutative group."]
250+
noncomputable def colimitCocone : Cocone F where
251+
pt := colimit.{v, u} F
252+
ι :=
253+
{
254+
(GroupCat.FilteredColimits.colimitCocone
255+
(F ⋙ forget₂ CommGroupCat GroupCat.{max v u})).ι with }
256+
set_option linter.uppercaseLean3 false in
257+
#align CommGroup.filtered_colimits.colimit_cocone CommGroupCat.FilteredColimits.colimitCocone
258+
set_option linter.uppercaseLean3 false in
259+
#align AddCommGroup.filtered_colimits.colimit_cocone AddCommGroupCat.FilteredColimits.colimitCocone
260+
261+
/-- The proposed colimit cocone is a colimit in `CommGroup`. -/
262+
@[to_additive "The proposed colimit cocone is a colimit in `AddCommGroup`."]
263+
def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
264+
desc t :=
265+
(GroupCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
266+
(F ⋙ forget₂ CommGroupCat GroupCat.{max v u})).desc
267+
((forget₂ CommGroupCat GroupCat.{max v u}).mapCocone t)
268+
fac t j :=
269+
FunLike.coe_injective <|
270+
(Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommGroupCat)).fac
271+
((forget CommGroupCat).mapCocone t) j
272+
uniq t _ h :=
273+
FunLike.coe_injective <|
274+
(Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommGroupCat)).uniq
275+
((forget CommGroupCat).mapCocone t) _ fun j => funext fun x => FunLike.congr_fun (h j) x
276+
set_option linter.uppercaseLean3 false in
277+
#align CommGroup.filtered_colimits.colimit_cocone_is_colimit CommGroupCat.FilteredColimits.colimitCoconeIsColimit
278+
set_option linter.uppercaseLean3 false in
279+
#align AddCommGroup.filtered_colimits.colimit_cocone_is_colimit AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit
280+
281+
@[to_additive]
282+
noncomputable instance forget₂GroupPreservesFilteredColimits :
283+
PreservesFilteredColimits (forget₂ CommGroupCat GroupCat.{u})
284+
where preserves_filtered_colimits J hJ1 _ := letI : Category J := hJ1
285+
{ preservesColimit := fun {F} =>
286+
preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
287+
(GroupCat.FilteredColimits.colimitCoconeIsColimit.{u, u}
288+
(F ⋙ forget₂ CommGroupCat GroupCat.{u})) }
289+
set_option linter.uppercaseLean3 false in
290+
#align CommGroup.filtered_colimits.forget₂_Group_preserves_filtered_colimits CommGroupCat.FilteredColimits.forget₂GroupPreservesFilteredColimits
291+
set_option linter.uppercaseLean3 false in
292+
#align AddCommGroup.filtered_colimits.forget₂_AddGroup_preserves_filtered_colimits AddCommGroupCat.FilteredColimits.forget₂AddGroupPreservesFilteredColimits
293+
294+
@[to_additive]
295+
noncomputable instance forgetPreservesFilteredColimits :
296+
PreservesFilteredColimits (forget CommGroupCat.{u}) :=
297+
Limits.compPreservesFilteredColimits (forget₂ CommGroupCat GroupCat) (forget GroupCat.{u})
298+
set_option linter.uppercaseLean3 false in
299+
#align CommGroup.filtered_colimits.forget_preserves_filtered_colimits CommGroupCat.FilteredColimits.forgetPreservesFilteredColimits
300+
set_option linter.uppercaseLean3 false in
301+
#align AddCommGroup.filtered_colimits.forget_preserves_filtered_colimits AddCommGroupCat.FilteredColimits.forgetPreservesFilteredColimits
302+
303+
end
304+
305+
end CommGroupCat.FilteredColimits

0 commit comments

Comments
 (0)