Skip to content

Commit 87c4a75

Browse files
TwoFXint-y1mattrobballkim-emfpvandoorn
committed
feat: port Algebra.Category.Mon.Limits (#3073)
Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
1 parent 18c085a commit 87c4a75

File tree

5 files changed

+295
-4
lines changed

5 files changed

+295
-4
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ import Mathlib.Algebra.Category.ModuleCat.EpiMono
4141
import Mathlib.Algebra.Category.ModuleCat.Products
4242
import Mathlib.Algebra.Category.ModuleCat.Tannaka
4343
import Mathlib.Algebra.Category.MonCat.Basic
44+
import Mathlib.Algebra.Category.MonCat.Limits
4445
import Mathlib.Algebra.Category.Ring.Basic
4546
import Mathlib.Algebra.CharP.Algebra
4647
import Mathlib.Algebra.CharP.Basic

‎Mathlib/Algebra/Category/MonCat/Basic.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl
9494
lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
9595

9696
-- porting note: added
97-
@[simp] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl
97+
@[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl
9898

9999
@[to_additive (attr := ext)]
100100
lemma ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -402,6 +402,7 @@ set_option linter.uppercaseLean3 false in
402402
-- porting note: this was added in order to ensure that `forget₂ CommMonCat MonCat`
403403
-- automatically reflects isomorphisms
404404
-- we could have used `CategoryTheory.ConcreteCategory.ReflectsIso` alternatively
405-
instance : Full (forget₂ CommMonCat MonCat) where preimage f := f
405+
@[to_additive]
406+
instance CommMonCat.forget₂Full : Full (forget₂ CommMonCat MonCat) where preimage f := f
406407

407408
example : ReflectsIsomorphisms (forget₂ CommMonCat MonCat) := inferInstance

‎Mathlib/Algebra/Category/MonCat/Limits.lean‎

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
/-
2+
Copyright (c) 2020 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module algebra.category.Mon.limits
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.MonCat.Basic
12+
import Mathlib.Algebra.Group.Pi
13+
import Mathlib.CategoryTheory.Limits.Creates
14+
import Mathlib.CategoryTheory.Limits.Types
15+
import Mathlib.GroupTheory.Submonoid.Operations
16+
17+
/-!
18+
# The category of (commutative) (additive) monoids has all limits
19+
20+
Further, these limits are preserved by the forgetful functor --- that is,
21+
the underlying types are just the limits in the category of types.
22+
23+
-/
24+
25+
set_option linter.uppercaseLean3 false -- `Mon`
26+
27+
noncomputable section
28+
29+
open CategoryTheory
30+
31+
open CategoryTheory.Limits
32+
33+
universe v u
34+
35+
-- Porting note: typemax hack to fix universe complaints
36+
/-- An alias for `MonCat.{max u v}`, to deal around unification issues. -/
37+
@[to_additive (attr := nolint checkUnivs) AddMonCatMax
38+
"An alias for `AddMonCat.{max u v}`, to deal around unification issues."]
39+
abbrev MonCatMax.{u1, u2} := MonCat.{max u1 u2}
40+
41+
namespace MonCat
42+
43+
variable {J : Type v} [SmallCategory J]
44+
45+
@[to_additive]
46+
instance monoidObj (F : J ⥤ MonCatMax.{u,v} ) (j) : Monoid ((F ⋙ forget MonCat).obj j) := by
47+
change Monoid (F.obj j)
48+
infer_instance
49+
#align Mon.monoid_obj MonCat.monoidObj
50+
#align AddMon.add_monoid_obj AddMonCat.addMonoidObj
51+
52+
/-- The flat sections of a functor into `MonCat` form a submonoid of all sections.
53+
-/
54+
@[to_additive
55+
"The flat sections of a functor into `AddMonCat` form an additive submonoid of all sections."]
56+
def sectionsSubmonoid (F : J ⥤ MonCatMax.{u,v}) : Submonoid (∀ j, F.obj j) where
57+
carrier := (F ⋙ forget MonCat).sections
58+
one_mem' {j} {j'} f := by simp
59+
mul_mem' {a} {b} ah bh {j} {j'} f := by
60+
simp only [Functor.comp_map, MonoidHom.map_mul, Pi.mul_apply]
61+
dsimp [Functor.sections] at ah bh
62+
rw [← ah f, ← bh f, forget_map, map_mul]
63+
#align Mon.sections_submonoid MonCat.sectionsSubmonoid
64+
#align AddMon.sections_add_submonoid AddMonCat.sectionsAddSubmonoid
65+
66+
@[to_additive]
67+
instance limitMonoid (F : J ⥤ MonCatMax.{u,v}) :
68+
Monoid (Types.limitCone.{v, u} (F ⋙ forget MonCatMax.{u,v})).pt :=
69+
(sectionsSubmonoid.{v, u} F).toMonoid
70+
#align Mon.limit_monoid MonCat.limitMonoid
71+
#align AddMon.limit_add_monoid AddMonCat.limitAddMonoid
72+
73+
/-- `limit.π (F ⋙ forget MonCat) j` as a `MonoidHom`. -/
74+
@[to_additive "`limit.π (F ⋙ forget AddMonCat) j` as an `AddMonoidHom`."]
75+
def limitπMonoidHom (F : J ⥤ MonCatMax.{u, v}) (j : J) :
76+
(Types.limitCone.{v, u} (F ⋙ forget MonCatMax.{u, v})).pt →*
77+
((F ⋙ forget MonCat.{max v u}).obj j) :=
78+
{ toFun := (Types.limitCone.{v, u} (F ⋙ forget MonCatMax.{u, v})).π.app j,
79+
map_one' := rfl
80+
map_mul' := fun _ _ => rfl }
81+
#align Mon.limit_π_monoid_hom MonCat.limitπMonoidHom
82+
#align AddMon.limit_π_add_monoid_hom AddMonCat.limitπAddMonoidHom
83+
84+
namespace HasLimits
85+
86+
-- The next two definitions are used in the construction of `HasLimits MonCat`.
87+
-- After that, the limits should be constructed using the generic limits API,
88+
-- e.g. `limit F`, `limit.cone F`, and `limit.isLimit F`.
89+
/-- Construction of a limit cone in `MonCat`.
90+
(Internal use only; use the limits API.)
91+
-/
92+
@[to_additive "(Internal use only; use the limits API.)"]
93+
def limitCone (F : J ⥤ MonCatMax.{u,v}) : Cone F :=
94+
{ pt := MonCat.of (Types.limitCone (F ⋙ forget _)).pt
95+
π :=
96+
{ app := limitπMonoidHom F
97+
naturality := fun _ _ f =>
98+
set_option linter.deprecated false in
99+
MonoidHom.coe_inj ((Types.limitCone (F ⋙ forget _)).π.naturality f) } }
100+
#align Mon.has_limits.limit_cone MonCat.HasLimits.limitCone
101+
#align AddMon.has_limits.limit_cone AddMonCat.HasLimits.limitCone
102+
103+
/-- Witness that the limit cone in `MonCat` is a limit cone.
104+
(Internal use only; use the limits API.)
105+
-/
106+
@[to_additive "(Internal use only; use the limits API.)"]
107+
def limitConeIsLimit (F : J ⥤ MonCatMax.{u,v}) : IsLimit (limitCone F) := by
108+
refine IsLimit.ofFaithful (forget MonCatMax) (Types.limitConeIsLimit.{v,u} _)
109+
(fun s => ⟨⟨_, ?_⟩, ?_⟩) (fun s => rfl) <;>
110+
aesop_cat
111+
#align Mon.has_limits.limit_cone_is_limit MonCat.HasLimits.limitConeIsLimit
112+
#align AddMon.has_limits.limit_cone_is_limit AddMonCat.HasLimits.limitConeIsLimit
113+
114+
end HasLimits
115+
116+
open HasLimits
117+
118+
/-- The category of monoids has all limits. -/
119+
@[to_additive "The category of additive monoids has all limits."]
120+
instance hasLimitsOfSize : HasLimitsOfSize.{v} MonCatMax.{u,v} where
121+
has_limits_of_shape _ _ :=
122+
{ has_limit := fun F =>
123+
HasLimit.mk
124+
{ cone := limitCone F
125+
isLimit := limitConeIsLimit F } }
126+
#align Mon.has_limits_of_size MonCat.hasLimitsOfSize
127+
#align AddMon.has_limits_of_size AddMonCat.hasLimitsOfSize
128+
129+
@[to_additive]
130+
instance hasLimits : HasLimits MonCat.{u} :=
131+
MonCat.hasLimitsOfSize.{u, u}
132+
#align Mon.has_limits MonCat.hasLimits
133+
#align AddMon.has_limits AddMonCat.hasLimits
134+
135+
/-- The forgetful functor from monoids to types preserves all limits.
136+
137+
This means the underlying type of a limit can be computed as a limit in the category of types. -/
138+
@[to_additive "The forgetful functor from additive monoids to types preserves all limits.\n\n
139+
This means the underlying type of a limit can be computed as a limit in the category of types."]
140+
instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v} (forget MonCatMax.{u,v}) where
141+
preservesLimitsOfShape {_} _ :=
142+
{ preservesLimit := fun {F} =>
143+
preservesLimitOfPreservesLimitCone (limitConeIsLimit F)
144+
(Types.limitConeIsLimit (F ⋙ forget _)) }
145+
#align Mon.forget_preserves_limits_of_size MonCat.forgetPreservesLimitsOfSize
146+
#align AddMon.forget_preserves_limits_of_size AddMonCat.forgetPreservesLimitsOfSize
147+
148+
@[to_additive]
149+
instance forgetPreservesLimits : PreservesLimits (forget MonCat.{u}) :=
150+
MonCat.forgetPreservesLimitsOfSize.{u, u}
151+
#align Mon.forget_preserves_limits MonCat.forgetPreservesLimits
152+
#align AddMon.forget_preserves_limits AddMonCat.forgetPreservesLimits
153+
154+
end MonCat
155+
156+
open MonCat
157+
158+
-- Porting note: typemax hack
159+
160+
/-- An alias for `CommMonCat.{max u v}`, to deal around unification issues. -/
161+
@[to_additive (attr := nolint checkUnivs) AddCommMonCatMax
162+
"An alias for `AddCommMonCat.{max u v}`, to deal around unification issues."]
163+
abbrev CommMonCatMax.{u1, u2} := CommMonCat.{max u1 u2}
164+
165+
namespace CommMonCat
166+
167+
variable {J : Type v} [SmallCategory J]
168+
169+
@[to_additive]
170+
instance commMonoidObj (F : J ⥤ CommMonCatMax.{u,v}) (j) :
171+
CommMonoid ((F ⋙ forget CommMonCatMax.{u,v}).obj j) := by
172+
change CommMonoid (F.obj j)
173+
infer_instance
174+
#align CommMon.comm_monoid_obj CommMonCat.commMonoidObj
175+
#align AddCommMon.add_comm_monoid_obj AddCommMonCat.addCommMonoidObj
176+
177+
@[to_additive]
178+
instance limitCommMonoid (F : J ⥤ CommMonCatMax.{u,v}) :
179+
CommMonoid (Types.limitCone.{v,u} (F ⋙ forget CommMonCatMax.{u,v})).pt :=
180+
@Submonoid.toCommMonoid (∀ j, F.obj j) _
181+
(MonCat.sectionsSubmonoid (F ⋙ forget₂ CommMonCatMax.{u,v} MonCatMax.{u,v}))
182+
#align CommMon.limit_comm_monoid CommMonCat.limitCommMonoid
183+
#align AddCommMon.limit_add_comm_monoid AddCommMonCat.limitAddCommMonoid
184+
185+
/-- We show that the forgetful functor `CommMonCat ⥤ MonCat` creates limits.
186+
187+
All we need to do is notice that the limit point has a `CommMonoid` instance available,
188+
and then reuse the existing limit. -/
189+
@[to_additive "We show that the forgetful functor `AddCommMonCat ⥤ AddMonCat` creates limits.\n\n
190+
All we need to do is notice that the limit point has an `AddCommMonoid` instance available,\n
191+
and then reuse the existing limit."]
192+
noncomputable instance forget₂CreatesLimit (F : J ⥤ CommMonCatMax.{u,v}) :
193+
CreatesLimit F (forget₂ CommMonCat MonCatMax.{u, v}) :=
194+
createsLimitOfReflectsIso fun c' t =>
195+
{ liftedCone :=
196+
{ pt := CommMonCat.of (Types.limitCone (F ⋙ forget CommMonCat)).pt
197+
π :=
198+
{ app := MonCat.limitπMonoidHom (F ⋙ forget₂ CommMonCatMax.{u,v} MonCatMax.{u,v})
199+
naturality :=
200+
(MonCat.HasLimits.limitCone
201+
(F ⋙ forget₂ CommMonCat MonCat.{max v u})).π.naturality } }
202+
validLift := by apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit _) t
203+
makesLimit :=
204+
IsLimit.ofFaithful (forget₂ CommMonCat MonCat.{max v u})
205+
(MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }
206+
207+
/-- A choice of limit cone for a functor into `CommMonCat`.
208+
(Generally, you'll just want to use `limit F`.)
209+
-/
210+
@[to_additive "A choice of limit cone for a functor into `AddCommMonCat`.
211+
(Generally, you'll just want to use `limit F`.)"]
212+
noncomputable def limitCone (F : J ⥤ CommMonCatMax.{u,v}) : Cone F :=
213+
liftLimit (limit.isLimit (F ⋙ forget₂ CommMonCatMax.{u,v} MonCatMax.{u,v}))
214+
#align CommMon.limit_cone CommMonCat.limitCone
215+
#align AddCommMon.limit_cone AddCommMonCat.limitCone
216+
217+
/-- The chosen cone is a limit cone.
218+
(Generally, you'll just want to use `limit.cone F`.)
219+
-/
220+
@[to_additive
221+
"The chosen cone is a limit cone. (Generally, you'll just want to use\n`limit.cone F`.)"]
222+
noncomputable def limitConeIsLimit (F : J ⥤ CommMonCatMax.{u,v}) : IsLimit (limitCone F) :=
223+
liftedLimitIsLimit _
224+
#align CommMon.limit_cone_is_limit CommMonCat.limitConeIsLimit
225+
#align AddCommMon.limit_cone_is_limit AddCommMonCat.limitConeIsLimit
226+
227+
/-- The category of commutative monoids has all limits. -/
228+
@[to_additive "The category of additive commutative monoids has all limits."]
229+
instance hasLimitsOfSize : HasLimitsOfSize.{v, v} CommMonCatMax.{u,v} where
230+
has_limits_of_shape _ _ :=
231+
{ has_limit := fun F => hasLimit_of_created F (forget₂ CommMonCatMax.{u,v} MonCatMax.{u,v}) }
232+
#align CommMon.has_limits_of_size CommMonCat.hasLimitsOfSize
233+
#align AddCommMon.has_limits_of_size AddCommMonCat.hasLimitsOfSize
234+
235+
@[to_additive]
236+
instance hasLimits : HasLimits CommMonCat.{u} :=
237+
CommMonCat.hasLimitsOfSize.{u, u}
238+
#align CommMon.has_limits CommMonCat.hasLimits
239+
#align AddCommMon.has_limits AddCommMonCat.hasLimits
240+
241+
/-- The forgetful functor from commutative monoids to monoids preserves all limits.
242+
243+
This means the underlying type of a limit can be computed as a limit in the category of monoids. -/
244+
@[to_additive AddCommMonCat.forget₂AddMonPreservesLimits "The forgetful functor from additive\n
245+
commutative monoids to additive monoids preserves all limits.\n\n
246+
This means the underlying type of a limit can be computed as a limit in the category of additive\n
247+
monoids."]
248+
noncomputable instance forget₂MonPreservesLimitsOfSize :
249+
PreservesLimitsOfSize.{v, v} (forget₂ CommMonCatMax.{u,v} MonCatMax.{u,v}) where
250+
preservesLimitsOfShape {J} 𝒥 := { preservesLimit := fun {F} => by infer_instance }
251+
#align CommMon.forget₂_Mon_preserves_limits_of_size CommMonCat.forget₂MonPreservesLimitsOfSize
252+
#align AddCommMon.forget₂_AddMon_preserves_limits AddCommMonCat.forget₂AddMonPreservesLimits
253+
254+
@[to_additive]
255+
noncomputable instance forget₂MonPreservesLimits :
256+
PreservesLimits (forget₂ CommMonCat MonCat.{u}) :=
257+
CommMonCat.forget₂MonPreservesLimitsOfSize.{u, u}
258+
#align CommMon.forget₂_Mon_preserves_limits CommMonCat.forget₂MonPreservesLimits
259+
#align AddCommMon.forget₂_Mon_preserves_limits AddCommMonCat.forget₂MonPreservesLimits
260+
261+
/-- The forgetful functor from commutative monoids to types preserves all limits.
262+
263+
This means the underlying type of a limit can be computed as a limit in the category of types. -/
264+
@[to_additive "The forgetful functor from additive commutative monoids to types preserves all\n
265+
limits.\n\n
266+
This means the underlying type of a limit can be computed as a limit in the category of types."]
267+
noncomputable instance forgetPreservesLimitsOfSize :
268+
PreservesLimitsOfSize.{v, v} (forget CommMonCatMax.{u, v}) where
269+
preservesLimitsOfShape {_} _ :=
270+
{ preservesLimit := fun {F} =>
271+
-- Porting note: we need to specify `F` here explicitly.
272+
@Limits.compPreservesLimit _ _ _ _ _ _ F _ _
273+
(forget₂ CommMonCatMax.{u, v} MonCatMax.{u, v}) (forget MonCat) _ _ }
274+
#align CommMon.forget_preserves_limits_of_size CommMonCat.forgetPreservesLimitsOfSize
275+
#align AddCommMon.forget_preserves_limits_of_size AddCommMonCat.forgetPreservesLimitsOfSize
276+
277+
@[to_additive]
278+
noncomputable instance forgetPreservesLimits : PreservesLimits (forget CommMonCat.{u}) :=
279+
CommMonCat.forgetPreservesLimitsOfSize.{u, u}
280+
#align CommMon.forget_preserves_limits CommMonCat.forgetPreservesLimits
281+
#align AddCommMon.forget_preserves_limits AddCommMonCat.forgetPreservesLimits
282+
283+
end CommMonCat

‎Mathlib/CategoryTheory/ConcreteCategory/Basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ variable {C : Type v} [Category C] [ConcreteCategory.{w} C]
102102

103103
/-- Usually a bundled hom structure already has a coercion to function
104104
that works with different universes. So we don't use this as a global instance. -/
105+
@[reducible]
105106
def ConcreteCategory.hasCoeToFun {X Y : C} : CoeFun (X ⟶ Y) fun _ => X → Y :=
106107
⟨fun f => (forget _).map f⟩
107108
#align category_theory.concrete_category.has_coe_to_fun CategoryTheory.ConcreteCategory.hasCoeToFun

‎Mathlib/Data/TypeMax.lean‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Std.Tactic.Lint
6+
import Mathlib.Tactic.ToAdditive
77

88
/-!
99
# Workaround for changes in universe unification
@@ -15,7 +15,12 @@ categories) in `TypeMax.{u,v}` to expose both universe parameters directly.
1515
1616
See also
1717
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233463.20universe.20constraint.20issues
18+
19+
Note: we mark it as `to_additive` so that `to_additive` doesn't think that types involving this
20+
cannot be additivized. This is just to help with the heuristic `to_additive` uses, and doesn't
21+
indicate that `TypeMax` has any algebraic operations associated to it.
1822
-/
1923

20-
@[nolint checkUnivs]
24+
/-- An alias for `Type max u v`, to deal around unification issues. -/
25+
@[nolint checkUnivs, to_additive existing TypeMax]
2126
abbrev TypeMax.{u, v} := Type max u v

0 commit comments

Comments
 (0)