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

Commit 024a423

Browse files
javraTwoFX
javra
and
TwoFX
committed
refactor(category_theory): generalise universe levels in preservation statements (#15067)
This big refactoring of universe levels in the category theory library allows to express limit preservation statements like exactness of functors which are between categories that are not necessarily in the same universe level. For this change to make sense for fixed diagrams (like coequalizers or binary products), the corresponding index categories, the universe of which so far was pinned to the category they were used for, is now fixed to `Type`. Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
1 parent 6e8f25e commit 024a423

86 files changed

Lines changed: 1124 additions & 783 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,15 +30,15 @@ open category_theory.limits
3030

3131
namespace FinVect
3232

33-
variables {J : Type v} [small_category J] [fin_category J]
33+
variables {J : Type} [small_category J] [fin_category J]
3434
variables {k : Type v} [field k]
3535

36-
instance {J : Type v} [fintype J] (Z : J → Module.{v} k) [∀ j, finite_dimensional k (Z j)] :
36+
instance {J : Type} [fintype J] (Z : J → Module.{v} k) [∀ j, finite_dimensional k (Z j)] :
3737
finite_dimensional k (∏ λ j, Z j : Module.{v} k) :=
3838
begin
3939
haveI : finite_dimensional k (Module.of k (Π j, Z j)), { dsimp, apply_instance, },
4040
exact finite_dimensional.of_injective
41-
(Module.pi_iso_pi.{v v v} _).hom
41+
(Module.pi_iso_pi _).hom
4242
((Module.mono_iff_injective _).1 (by apply_instance)),
4343
end
4444

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open category_theory.limits
1717

1818
open_locale big_operators
1919

20-
universe u
20+
universes w u
2121

2222
namespace AddCommGroup
2323

@@ -72,9 +72,8 @@ is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk walking_pair.left
7272
(biprod_iso_prod G H).inv ≫ biprod.snd = add_monoid_hom.snd G H :=
7373
is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk walking_pair.right)
7474

75-
variables {J : Type u} (f : J → AddCommGroup.{u})
76-
7775
namespace has_limit
76+
variables {J : Type w} (f : J → AddCommGroup.{max w u})
7877

7978
/--
8079
The map from an arbitrary cone over a indexed family of abelian groups
@@ -109,19 +108,20 @@ end has_limit
109108

110109
open has_limit
111110

111+
variables {J : Type} [fintype J]
112+
112113
/--
113114
We verify that the biproduct we've just defined is isomorphic to the AddCommGroup structure
114115
on the dependent function type
115116
-/
116117
@[simps hom_apply] noncomputable
117-
def biproduct_iso_pi [fintype J] (f : J → AddCommGroup.{u}) :
118+
def biproduct_iso_pi (f : J → AddCommGroup.{u}) :
118119
(⨁ f : AddCommGroup) ≅ AddCommGroup.of (Π j, f j) :=
119120
is_limit.cone_point_unique_up_to_iso
120121
(biproduct.is_limit f)
121122
(product_limit_cone f).is_limit
122123

123-
@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [fintype J]
124-
(f : J → AddCommGroup.{u}) (j : J) :
124+
@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π (f : J → AddCommGroup.{u}) (j : J) :
125125
(biproduct_iso_pi f).inv ≫ biproduct.π f j = pi.eval_add_monoid_hom (λ j, f j) j :=
126126
is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk j)
127127

‎src/algebra/category/Module/biproducts.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open category_theory.limits
1717

1818
open_locale big_operators
1919

20-
universes v u
20+
universes w v u
2121

2222
namespace Module
2323

@@ -76,10 +76,10 @@ is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk walking_pair.left
7676
(biprod_iso_prod M N).inv ≫ biprod.snd = linear_map.snd R M N :=
7777
is_limit.cone_point_unique_up_to_iso_inv_comp _ _ (discrete.mk walking_pair.right)
7878

79-
variables {J : Type v} (f : J → Module.{v} R)
80-
8179
namespace has_limit
8280

81+
variables {J : Type w} (f : J → Module.{max w v} R)
82+
8383
/--
8484
The map from an arbitrary cone over a indexed family of abelian groups
8585
to the cartesian product of those groups.
@@ -113,6 +113,8 @@ end has_limit
113113

114114
open has_limit
115115

116+
variables {J : Type} (f : J → Module.{v} R)
117+
116118
/--
117119
We verify that the biproduct we've just defined is isomorphic to the `Module R` structure
118120
on the dependent function type

‎src/algebra/category/Ring/constructions.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,7 @@ begin
184184
exact ⟨⟨y, this⟩, subtype.eq h₃⟩,
185185
end
186186

187-
instance equalizer_ι_is_local_ring_hom (F : walking_parallel_pair.{u} ⥤ CommRing.{u}) :
187+
instance equalizer_ι_is_local_ring_hom (F : walking_parallel_pair ⥤ CommRing.{u}) :
188188
is_local_ring_hom (limit.π F walking_parallel_pair.zero) :=
189189
begin
190190
have := lim_map_π (diagram_iso_parallel_pair F).hom walking_parallel_pair.zero,
@@ -200,10 +200,10 @@ end
200200
open category_theory.limits.walking_parallel_pair opposite
201201
open category_theory.limits.walking_parallel_pair_hom
202202

203-
instance equalizer_ι_is_local_ring_hom' (F : walking_parallel_pair.{u}ᵒᵖ ⥤ CommRing.{u}) :
203+
instance equalizer_ι_is_local_ring_hom' (F : walking_parallel_pairᵒᵖ ⥤ CommRing.{u}) :
204204
is_local_ring_hom (limit.π F (opposite.op walking_parallel_pair.one)) :=
205205
begin
206-
have : _ = limit.π F (walking_parallel_pair_op_equiv.{u u}.functor.obj _) :=
206+
have : _ = limit.π F (walking_parallel_pair_op_equiv.functor.obj _) :=
207207
(limit.iso_limit_cone_inv_π ⟨_, is_limit.whisker_equivalence (limit.is_limit F)
208208
walking_parallel_pair_op_equiv⟩ walking_parallel_pair.zero : _),
209209
erw ← this,

‎src/algebraic_geometry/Spec.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ Spec, as a contravariant functor from commutative rings to sheafed spaces.
115115
/--
116116
Spec, as a contravariant functor from commutative rings to presheafed spaces.
117117
-/
118-
def Spec.to_PresheafedSpace : CommRingᵒᵖ ⥤ PresheafedSpace CommRing :=
118+
def Spec.to_PresheafedSpace : CommRingᵒᵖ ⥤ PresheafedSpace.{u} CommRing.{u} :=
119119
Spec.to_SheafedSpace ⋙ SheafedSpace.forget_to_PresheafedSpace
120120

121121
@[simp] lemma Spec.to_PresheafedSpace_obj (R : CommRingᵒᵖ) :

‎src/algebraic_geometry/locally_ringed_space/has_colimits.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ def coproduct_cofan_is_colimit : is_colimit (coproduct_cofan F) :=
9494
uniq' := λ s f h, subtype.eq (is_colimit.uniq _ (forget_to_SheafedSpace.map_cocone s) f.1
9595
(λ j, congr_arg subtype.val (h j))) }
9696

97-
instance : has_coproducts LocallyRingedSpace.{u} :=
97+
instance : has_coproducts.{u} LocallyRingedSpace.{u} :=
9898
λ ι, ⟨λ F, ⟨⟨⟨_, coproduct_cofan_is_colimit F⟩⟩⟩⟩
9999

100100
noncomputable
@@ -106,7 +106,7 @@ end has_coproducts
106106

107107
section has_coequalizer
108108

109-
variables {X Y : LocallyRingedSpace.{u}} (f g : X ⟶ Y)
109+
variables {X Y : LocallyRingedSpace.{v}} (f g : X ⟶ Y)
110110

111111
namespace has_coequalizer
112112

@@ -178,7 +178,7 @@ lemma image_basic_open_image_open :
178178
is_open ((coequalizer.π f.1 g.1).base '' (image_basic_open f g U s).1) :=
179179
begin
180180
rw [← (Top.homeo_of_iso (preserves_coequalizer.iso (SheafedSpace.forget _) f.1 g.1))
181-
.is_open_preimage, Top.coequalizer_is_open_iff.{u}, ← set.preimage_comp],
181+
.is_open_preimage, Top.coequalizer_is_open_iff, ← set.preimage_comp],
182182
erw ← coe_comp,
183183
rw [preserves_coequalizer.iso_hom, ι_comp_coequalizer_comparison],
184184
dsimp only [SheafedSpace.forget],
@@ -280,7 +280,7 @@ instance : has_coequalizers LocallyRingedSpace := has_coequalizers_of_has_colimi
280280

281281
noncomputable
282282
instance preserves_coequalizer :
283-
preserves_colimits_of_shape walking_parallel_pair.{v} forget_to_SheafedSpace.{v} :=
283+
preserves_colimits_of_shape walking_parallel_pair forget_to_SheafedSpace.{v} :=
284284
⟨λ F, begin
285285
apply preserves_colimit_of_iso_diagram _ (diagram_iso_parallel_pair F).symm,
286286
apply preserves_colimit_of_preserves_colimit_cocone (coequalizer_cofork_is_colimit _ _),

‎src/algebraic_geometry/open_immersion.lean‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ variables {C : Type u} [category.{v} C]
6868
An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying
6969
spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
7070
-/
71-
class PresheafedSpace.is_open_immersion {X Y : PresheafedSpace C} (f : X ⟶ Y) : Prop :=
71+
class PresheafedSpace.is_open_immersion {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) : Prop :=
7272
(base_open : open_embedding f.base)
7373
(c_iso : ∀ U : opens X, is_iso (f.c.app (op (base_open.is_open_map.functor.obj U))))
7474

@@ -77,7 +77,7 @@ A morphism of SheafedSpaces is an open immersion if it is an open immersion as a
7777
of PresheafedSpaces
7878
-/
7979
abbreviation SheafedSpace.is_open_immersion
80-
[has_products C] {X Y : SheafedSpace C} (f : X ⟶ Y) : Prop :=
80+
[has_products.{v} C] {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) : Prop :=
8181
PresheafedSpace.is_open_immersion f
8282

8383
/--
@@ -104,7 +104,7 @@ attribute [instance] is_open_immersion.c_iso
104104

105105
section
106106

107-
variables {X Y : PresheafedSpace C} {f : X ⟶ Y} (H : is_open_immersion f)
107+
variables {X Y : PresheafedSpace.{v} C} {f : X ⟶ Y} (H : is_open_immersion f)
108108

109109
/-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
110110
abbreviation open_functor := H.base_open.is_open_map.functor
@@ -228,12 +228,12 @@ by { erw ← category.assoc, rw [is_iso.comp_inv_eq, f.c.naturality], congr }
228228
by { erw ← category.assoc, rw [is_iso.comp_inv_eq, f.c.naturality], congr }
229229

230230
/-- An isomorphism is an open immersion. -/
231-
instance of_iso {X Y : PresheafedSpace C} (H : X ≅ Y) : is_open_immersion H.hom :=
231+
instance of_iso {X Y : PresheafedSpace.{v} C} (H : X ≅ Y) : is_open_immersion H.hom :=
232232
{ base_open := (Top.homeo_of_iso ((forget C).map_iso H)).open_embedding,
233233
c_iso := λ _, infer_instance }
234234

235235
@[priority 100]
236-
instance of_is_iso {X Y : PresheafedSpace C} (f : X ⟶ Y) [is_iso f] : is_open_immersion f :=
236+
instance of_is_iso {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) [is_iso f] : is_open_immersion f :=
237237
algebraic_geometry.PresheafedSpace.is_open_immersion.of_iso (as_iso f)
238238

239239
instance of_restrict {X : Top} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier}
@@ -289,7 +289,7 @@ section pullback
289289

290290
noncomputable theory
291291

292-
variables {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : is_open_immersion f] (g : Y ⟶ Z)
292+
variables {X Y Z : PresheafedSpace.{v} C} (f : X ⟶ Z) [hf : is_open_immersion f] (g : Y ⟶ Z)
293293

294294
include hf
295295

@@ -526,7 +526,7 @@ open category_theory.limits.walking_cospan
526526

527527
section to_SheafedSpace
528528

529-
variables [has_products C] {X : PresheafedSpace C} (Y : SheafedSpace C)
529+
variables [has_products.{v} C] {X : PresheafedSpace.{v} C} (Y : SheafedSpace C)
530530
variables (f : X ⟶ Y.to_PresheafedSpace) [H : is_open_immersion f]
531531

532532
include H
@@ -559,14 +559,14 @@ instance to_SheafedSpace_is_open_immersion :
559559

560560
omit H
561561

562-
@[simp] lemma SheafedSpace_to_SheafedSpace {X Y : SheafedSpace C} (f : X ⟶ Y)
562+
@[simp] lemma SheafedSpace_to_SheafedSpace {X Y : SheafedSpace.{v} C} (f : X ⟶ Y)
563563
[is_open_immersion f] : to_SheafedSpace Y f = X := by unfreezingI { cases X, refl }
564564

565565
end to_SheafedSpace
566566

567567
section to_LocallyRingedSpace
568568

569-
variables {X : PresheafedSpace CommRing.{u}} (Y : LocallyRingedSpace.{u})
569+
variables {X : PresheafedSpace.{u} CommRing.{u}} (Y : LocallyRingedSpace.{u})
570570
variables (f : X ⟶ Y.to_PresheafedSpace) [H : is_open_immersion f]
571571

572572
include H
@@ -608,10 +608,10 @@ end PresheafedSpace.is_open_immersion
608608

609609
namespace SheafedSpace.is_open_immersion
610610

611-
variables [has_products C]
611+
variables [has_products.{v} C]
612612

613613
@[priority 100]
614-
instance of_is_iso {X Y : SheafedSpace C} (f : X ⟶ Y) [is_iso f] :
614+
instance of_is_iso {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) [is_iso f] :
615615
SheafedSpace.is_open_immersion f :=
616616
@@PresheafedSpace.is_open_immersion.of_is_iso _ f
617617
(SheafedSpace.forget_to_PresheafedSpace.map_is_iso _)
@@ -1318,7 +1318,7 @@ namespace PresheafedSpace.is_open_immersion
13181318

13191319
section to_Scheme
13201320

1321-
variables {X : PresheafedSpace CommRing.{u}} (Y : Scheme.{u})
1321+
variables {X : PresheafedSpace.{u} CommRing.{u}} (Y : Scheme.{u})
13221322
variables (f : X ⟶ Y.to_PresheafedSpace) [H : PresheafedSpace.is_open_immersion f]
13231323

13241324
include H

0 commit comments

Comments
 (0)