Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit c43486e

Browse files
kim-emkim-em
committed
feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990)
I'm concerned about the new universe annotations required in places. It was not so impossible to add them when proofs broke, but the proofs might have been hard to construct in the first place .... Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent ad244dd commit c43486e

30 files changed

Lines changed: 654 additions & 413 deletions

File tree

‎src/algebra/category/Algebra/limits.lean‎

Lines changed: 39 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ the underlying types are just the limits in the category of types.
1717
open category_theory
1818
open category_theory.limits
1919

20-
universes v u
20+
universes v w u -- `u` is determined by the ring, so can come last
2121

2222
noncomputable theory
2323

@@ -26,44 +26,46 @@ namespace Algebra
2626
variables {R : Type u} [comm_ring R]
2727
variables {J : Type v} [small_category J]
2828

29-
instance semiring_obj (F : J ⥤ Algebra R) (j) :
29+
instance semiring_obj (F : J ⥤ Algebra.{max v w} R) (j) :
3030
semiring ((F ⋙ forget (Algebra R)).obj j) :=
3131
by { change semiring (F.obj j), apply_instance }
3232

33-
instance algebra_obj (F : J ⥤ Algebra R) (j) :
33+
instance algebra_obj (F : J ⥤ Algebra.{max v w} R) (j) :
3434
algebra R ((F ⋙ forget (Algebra R)).obj j) :=
3535
by { change algebra R (F.obj j), apply_instance }
3636

3737
/--
3838
The flat sections of a functor into `Algebra R` form a submodule of all sections.
3939
-/
40-
def sections_subalgebra (F : J ⥤ Algebra R) :
40+
def sections_subalgebra (F : J ⥤ Algebra.{max v w} R) :
4141
subalgebra R (Π j, F.obj j) :=
4242
{ algebra_map_mem' := λ r j j' f, (F.map f).commutes r,
43-
..SemiRing.sections_subsemiring (F ⋙ forget₂ (Algebra R) Ring ⋙ forget₂ Ring SemiRing) }
43+
..SemiRing.sections_subsemiring
44+
(F ⋙ forget₂ (Algebra R) Ring.{max v w} ⋙ forget₂ Ring SemiRing.{max v w}) }
4445

4546

46-
instance limit_semiring (F : J ⥤ Algebra R) :
47-
ring (types.limit_cone (F ⋙ forget (Algebra.{v} R))).X :=
47+
instance limit_semiring (F : J ⥤ Algebra.{max v w} R) :
48+
ring (types.limit_cone (F ⋙ forget (Algebra.{max v w} R))).X :=
4849
begin
4950
change ring (sections_subalgebra F),
5051
apply_instance,
5152
end
5253

53-
instance limit_algebra (F : J ⥤ Algebra R) :
54-
algebra R (types.limit_cone (F ⋙ forget (Algebra.{v} R))).X :=
54+
instance limit_algebra (F : J ⥤ Algebra.{max v w} R) :
55+
algebra R (types.limit_cone (F ⋙ forget (Algebra.{max v w} R))).X :=
5556
begin
56-
have : algebra R (types.limit_cone (F ⋙ forget (Algebra.{v} R))).X
57+
have : algebra R (types.limit_cone (F ⋙ forget (Algebra.{max v w} R))).X
5758
= algebra R (sections_subalgebra F), by refl,
5859
rw this,
5960
apply_instance,
6061
end
6162

6263
/-- `limit.π (F ⋙ forget (Algebra R)) j` as a `alg_hom`. -/
63-
def limit_π_alg_hom (F : J ⥤ Algebra.{v} R) (j) :
64-
(types.limit_cone (F ⋙ forget (Algebra R))).X →ₐ[R] (F ⋙ forget (Algebra.{v} R)).obj j :=
64+
def limit_π_alg_hom (F : J ⥤ Algebra.{max v w} R) (j) :
65+
(types.limit_cone (F ⋙ forget (Algebra R))).X →ₐ[R] (F ⋙ forget (Algebra.{max v w} R)).obj j :=
6566
{ commutes' := λ r, rfl,
66-
..SemiRing.limit_π_ring_hom (F ⋙ forget₂ (Algebra R) Ring.{v} ⋙ forget₂ Ring SemiRing.{v}) j }
67+
..SemiRing.limit_π_ring_hom
68+
(F ⋙ forget₂ (Algebra R) Ring.{max v w} ⋙ forget₂ Ring SemiRing.{max v w}) j }
6769

6870
namespace has_limits
6971
-- The next two definitions are used in the construction of `has_limits (Algebra R)`.
@@ -74,7 +76,7 @@ namespace has_limits
7476
Construction of a limit cone in `Algebra R`.
7577
(Internal use only; use the limits API.)
7678
-/
77-
def limit_cone (F : J ⥤ Algebra.{v} R) : cone F :=
79+
def limit_cone (F : J ⥤ Algebra.{max v w} R) : cone F :=
7880
{ X := Algebra.of R (types.limit_cone (F ⋙ forget _)).X,
7981
π :=
8082
{ app := limit_π_alg_hom F,
@@ -85,7 +87,7 @@ def limit_cone (F : J ⥤ Algebra.{v} R) : cone F :=
8587
Witness that the limit cone in `Algebra R` is a limit cone.
8688
(Internal use only; use the limits API.)
8789
-/
88-
def limit_cone_is_limit (F : J ⥤ Algebra R) : is_limit (limit_cone F) :=
90+
def limit_cone_is_limit (F : J ⥤ Algebra.{max v w} R) : is_limit (limit_cone F) :=
8991
begin
9092
refine is_limit.of_faithful
9193
(forget (Algebra R)) (types.limit_cone_is_limit _)
@@ -103,36 +105,52 @@ open has_limits
103105

104106
/-- The category of R-algebras has all limits. -/
105107
@[irreducible]
106-
instance has_limits : has_limits (Algebra R) :=
108+
instance has_limits_of_size : has_limits_of_size.{v v} (Algebra.{max v w} R) :=
107109
{ has_limits_of_shape := λ J 𝒥, by exactI
108110
{ has_limit := λ F, has_limit.mk
109111
{ cone := limit_cone F,
110112
is_limit := limit_cone_is_limit F } } }
111113

114+
instance has_limits : has_limits (Algebra.{w} R) := Algebra.has_limits_of_size.{w w u}
115+
112116
/--
113117
The forgetful functor from R-algebras to rings preserves all limits.
114118
-/
115-
instance forget₂_Ring_preserves_limits : preserves_limits (forget₂ (Algebra R) Ring.{v}) :=
119+
instance forget₂_Ring_preserves_limits_of_size :
120+
preserves_limits_of_size.{v v} (forget₂ (Algebra R) Ring.{max v w}) :=
116121
{ preserves_limits_of_shape := λ J 𝒥, by exactI
117122
{ preserves_limit := λ F, preserves_limit_of_preserves_limit_cone
118123
(limit_cone_is_limit F)
119-
(by apply Ring.limit_cone_is_limit (F ⋙ forget₂ (Algebra R) Ring)) } }
124+
(by apply Ring.limit_cone_is_limit (F ⋙ forget₂ (Algebra R) Ring.{max v w})) } }
125+
126+
instance forget₂_Ring_preserves_limits :
127+
preserves_limits (forget₂ (Algebra R) Ring.{w}) :=
128+
Algebra.forget₂_Ring_preserves_limits_of_size.{w w}
120129

121130
/--
122131
The forgetful functor from R-algebras to R-modules preserves all limits.
123132
-/
124-
instance forget₂_Module_preserves_limits : preserves_limits (forget₂ (Algebra R) (Module.{v} R)) :=
133+
instance forget₂_Module_preserves_limits_of_size :
134+
preserves_limits_of_size.{v v} (forget₂ (Algebra R) (Module.{max v w} R)) :=
125135
{ preserves_limits_of_shape := λ J 𝒥, by exactI
126136
{ preserves_limit := λ F, preserves_limit_of_preserves_limit_cone
127137
(limit_cone_is_limit F)
128-
(by apply Module.has_limits.limit_cone_is_limit (F ⋙ forget₂ (Algebra R) (Module R))) } }
138+
(by apply Module.has_limits.limit_cone_is_limit
139+
(F ⋙ forget₂ (Algebra R) (Module.{max v w} R))) } }
140+
141+
instance forget₂_Module_preserves_limits : preserves_limits (forget₂ (Algebra R) (Module.{w} R)) :=
142+
Algebra.forget₂_Module_preserves_limits_of_size.{w w}
129143

130144
/--
131145
The forgetful functor from R-algebras to types preserves all limits.
132146
-/
133-
instance forget_preserves_limits : preserves_limits (forget (Algebra R)) :=
147+
instance forget_preserves_limits_of_size :
148+
preserves_limits_of_size.{v v} (forget (Algebra.{max v w} R)) :=
134149
{ preserves_limits_of_shape := λ J 𝒥, by exactI
135150
{ preserves_limit := λ F, preserves_limit_of_preserves_limit_cone
136151
(limit_cone_is_limit F) (types.limit_cone_is_limit (F ⋙ forget _)) } }
137152

153+
instance forget_preserves_limits : preserves_limits (forget (Algebra.{w} R)) :=
154+
Algebra.forget_preserves_limits_of_size.{w w}
155+
138156
end Algebra

‎src/algebra/category/FinVect/limits.lean‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,11 @@ import category_theory.limits.constructions.limits_of_products_and_equalizers
1515
# `forget₂ (FinVect K) (Module K)` creates all finite limits.
1616
1717
And hence `FinVect K` has all finite limits.
18+
19+
## Future work
20+
After generalising `FinVect` to allow the ring and the module to live in different universes,
21+
generalize this construction so we can take limits over smaller diagrams,
22+
as is done for the other algebraic categories.
1823
-/
1924

2025
noncomputable theory
@@ -33,7 +38,7 @@ instance {J : Type v} [fintype J] (Z : J → Module.{v} k) [∀ j, finite_dimens
3338
begin
3439
haveI : finite_dimensional k (Module.of k (Π j, Z j)), { dsimp, apply_instance, },
3540
exact finite_dimensional.of_injective
36-
(Module.pi_iso_pi _).hom
41+
(Module.pi_iso_pi.{v v v} _).hom
3742
((Module.mono_iff_injective _).1 (by apply_instance)),
3843
end
3944

‎src/algebra/category/Group/filtered_colimits.lean‎

Lines changed: 26 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ particular, this implies that `forget Group` preserves filtered colimits. Simila
2020
2121
-/
2222

23-
universe v
23+
universes v u
2424

2525
noncomputable theory
2626
open_locale classical
@@ -37,15 +37,15 @@ open Mon.filtered_colimits (colimit_one_eq colimit_mul_mk_eq)
3737

3838
-- We use parameters here, mainly so we can have the abbreviations `G` and `G.mk` below, without
3939
-- passing around `F` all the time.
40-
parameters {J : Type v} [small_category J] [is_filtered J] (F : J ⥤ Group.{v})
40+
parameters {J : Type v} [small_category J] [is_filtered J] (F : J ⥤ Group.{max v u})
4141

4242
/--
4343
The colimit of `F ⋙ forget₂ Group Mon` in the category `Mon`.
4444
In the following, we will show that this has the structure of a group.
4545
-/
4646
@[to_additive "The colimit of `F ⋙ forget₂ AddGroup AddMon` in the category `AddMon`.
4747
In the following, we will show that this has the structure of an additive group."]
48-
abbreviation G : Mon := Mon.filtered_colimits.colimit (F ⋙ forget₂ Group Mon)
48+
abbreviation G : Mon := Mon.filtered_colimits.colimit (F ⋙ forget₂ Group Mon.{max v u})
4949

5050
/-- The canonical projection into the colimit, as a quotient type. -/
5151
@[to_additive "The canonical projection into the colimit, as a quotient type."]
@@ -93,8 +93,9 @@ instance colimit_group : group G :=
9393
{ mul_left_inv := λ x, begin
9494
apply quot.induction_on x, clear x, intro x,
9595
cases x with j x,
96-
erw [colimit_inv_mk_eq, colimit_mul_mk_eq (F ⋙ forget₂ Group Mon) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
97-
colimit_one_eq (F ⋙ forget₂ Group Mon) j],
96+
erw [colimit_inv_mk_eq,
97+
colimit_mul_mk_eq (F ⋙ forget₂ Group Mon.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
98+
colimit_one_eq (F ⋙ forget₂ Group Mon.{max v u}) j],
9899
dsimp,
99100
simp only [category_theory.functor.map_id, id_apply, mul_left_inv],
100101
end,
@@ -109,12 +110,12 @@ def colimit : Group := Group.of G
109110
@[to_additive "The cocone over the proposed colimit additive group."]
110111
def colimit_cocone : cocone F :=
111112
{ X := colimit,
112-
ι := { ..(Mon.filtered_colimits.colimit_cocone (F ⋙ forget₂ Group Mon)).ι } }
113+
ι := { ..(Mon.filtered_colimits.colimit_cocone (F ⋙ forget₂ Group Mon.{max v u})).ι } }
113114

114115
/-- The proposed colimit cocone is a colimit in `Group`. -/
115116
@[to_additive "The proposed colimit cocone is a colimit in `AddGroup`."]
116117
def colimit_cocone_is_colimit : is_colimit colimit_cocone :=
117-
{ desc := λ t, Mon.filtered_colimits.colimit_desc (F ⋙ forget₂ Group Mon)
118+
{ desc := λ t, Mon.filtered_colimits.colimit_desc (F ⋙ forget₂ Group Mon.{max v u})
118119
((forget₂ Group Mon).map_cocone t),
119120
fac' := λ t j, monoid_hom.coe_inj $
120121
(types.colimit_cocone_is_colimit (F ⋙ forget Group)).fac ((forget Group).map_cocone t) j,
@@ -124,15 +125,15 @@ def colimit_cocone_is_colimit : is_colimit colimit_cocone :=
124125

125126
@[to_additive forget₂_AddMon_preserves_filtered_colimits]
126127
instance forget₂_Mon_preserves_filtered_colimits :
127-
preserves_filtered_colimits (forget₂ Group Mon.{v}) :=
128+
preserves_filtered_colimits (forget₂ Group Mon.{u}) :=
128129
{ preserves_filtered_colimits := λ J _ _, by exactI
129130
{ preserves_colimit := λ F, preserves_colimit_of_preserves_colimit_cocone
130-
(colimit_cocone_is_colimit F)
131-
(Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ forget₂ Group Mon.{v})) } }
131+
(colimit_cocone_is_colimit.{u u} F)
132+
(Mon.filtered_colimits.colimit_cocone_is_colimit (F ⋙ forget₂ Group Mon.{u})) } }
132133

133134
@[to_additive]
134-
instance forget_preserves_filtered_colimits : preserves_filtered_colimits (forget Group) :=
135-
limits.comp_preserves_filtered_colimits (forget₂ Group Mon) (forget Mon)
135+
instance forget_preserves_filtered_colimits : preserves_filtered_colimits (forget Group.{u}) :=
136+
limits.comp_preserves_filtered_colimits (forget₂ Group Mon) (forget Mon.{u})
136137

137138
end
138139

@@ -145,20 +146,20 @@ section
145146

146147
-- We use parameters here, mainly so we can have the abbreviation `G` below, without
147148
-- passing around `F` all the time.
148-
parameters {J : Type v} [small_category J] [is_filtered J] (F : J ⥤ CommGroup.{v})
149+
parameters {J : Type v} [small_category J] [is_filtered J] (F : J ⥤ CommGroup.{max v u})
149150

150151
/--
151152
The colimit of `F ⋙ forget₂ CommGroup Group` in the category `Group`.
152153
In the following, we will show that this has the structure of a _commutative_ group.
153154
-/
154155
@[to_additive "The colimit of `F ⋙ forget₂ AddCommGroup AddGroup` in the category `AddGroup`.
155156
In the following, we will show that this has the structure of a _commutative_ additive group."]
156-
abbreviation G : Group := Group.filtered_colimits.colimit (F ⋙ forget₂ CommGroup Group.{v})
157+
abbreviation G : Group := Group.filtered_colimits.colimit (F ⋙ forget₂ CommGroup Group.{max v u})
157158

158159
@[to_additive]
159160
instance colimit_comm_group : comm_group G :=
160161
{ ..G.group,
161-
..CommMon.filtered_colimits.colimit_comm_monoid (F ⋙ forget₂ CommGroup CommMon.{v}) }
162+
..CommMon.filtered_colimits.colimit_comm_monoid (F ⋙ forget₂ CommGroup CommMon.{max v u}) }
162163

163164
/-- The bundled commutative group giving the filtered colimit of a diagram. -/
164165
@[to_additive "The bundled additive commutative group giving the filtered colimit of a diagram."]
@@ -168,14 +169,14 @@ def colimit : CommGroup := CommGroup.of G
168169
@[to_additive "The cocone over the proposed colimit additive commutative group."]
169170
def colimit_cocone : cocone F :=
170171
{ X := colimit,
171-
ι := { ..(Group.filtered_colimits.colimit_cocone (F ⋙ forget₂ CommGroup Group)).ι } }
172+
ι := { ..(Group.filtered_colimits.colimit_cocone (F ⋙ forget₂ CommGroup Group.{max v u})).ι } }
172173

173174
/-- The proposed colimit cocone is a colimit in `CommGroup`. -/
174175
@[to_additive "The proposed colimit cocone is a colimit in `AddCommGroup`."]
175176
def colimit_cocone_is_colimit : is_colimit colimit_cocone :=
176177
{ desc := λ t,
177-
(Group.filtered_colimits.colimit_cocone_is_colimit (F ⋙ forget₂ CommGroup Group.{v})).desc
178-
((forget₂ CommGroup Group.{v}).map_cocone t),
178+
(Group.filtered_colimits.colimit_cocone_is_colimit (F ⋙ forget₂ CommGroup Group.{max v u})).desc
179+
((forget₂ CommGroup Group.{max v u}).map_cocone t),
179180
fac' := λ t j, monoid_hom.coe_inj $
180181
(types.colimit_cocone_is_colimit (F ⋙ forget CommGroup)).fac
181182
((forget CommGroup).map_cocone t) j,
@@ -185,15 +186,17 @@ def colimit_cocone_is_colimit : is_colimit colimit_cocone :=
185186

186187
@[to_additive forget₂_AddGroup_preserves_filtered_colimits]
187188
instance forget₂_Group_preserves_filtered_colimits :
188-
preserves_filtered_colimits (forget₂ CommGroup Group.{v}) :=
189+
preserves_filtered_colimits (forget₂ CommGroup Group.{u}) :=
189190
{ preserves_filtered_colimits := λ J _ _, by exactI
190191
{ preserves_colimit := λ F, preserves_colimit_of_preserves_colimit_cocone
191-
(colimit_cocone_is_colimit F)
192-
(Group.filtered_colimits.colimit_cocone_is_colimit (F ⋙ forget₂ CommGroup Group.{v})) } }
192+
(colimit_cocone_is_colimit.{u u} F)
193+
(Group.filtered_colimits.colimit_cocone_is_colimit
194+
(F ⋙ forget₂ CommGroup Group.{u})) } }
193195

194196
@[to_additive]
195-
instance forget_preserves_filtered_colimits : preserves_filtered_colimits (forget CommGroup) :=
196-
limits.comp_preserves_filtered_colimits (forget₂ CommGroup Group) (forget Group)
197+
instance forget_preserves_filtered_colimits :
198+
preserves_filtered_colimits (forget CommGroup.{u}) :=
199+
limits.comp_preserves_filtered_colimits (forget₂ CommGroup Group) (forget Group.{u})
197200

198201
end
199202

0 commit comments

Comments
 (0)