-
Notifications
You must be signed in to change notification settings - Fork 261
/
SmallShiftedHom.lean
218 lines (174 loc) · 9.28 KB
/
SmallShiftedHom.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
/-
Copyright (c) 2024 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.CategoryTheory.Localization.SmallHom
import Mathlib.CategoryTheory.Shift.ShiftedHom
import Mathlib.CategoryTheory.Shift.Localization
/-!
# Shrinking morphisms in localized categories equipped with shifts
If `C` is a category equipped with a shift by an additive monoid `M`,
and `W : MorphismProperty C` is compatible with the shift,
we define a type-class `HasSmallLocalizedShiftedHom.{w} W X Y` which
says that all the types of morphisms from `X⟦a⟧` to `Y⟦b⟧` in the
localized category are `w`-small for a certain universe. Then,
we define types `SmallShiftedHom.{w} W X Y m : Type w` for all `m : M`,
and endow these with a composition which transports the composition
on the types `ShiftedHom (L.obj X) (L.obj Y) m` when `L : C ⥤ D` is
any localization functor for `W`.
-/
universe w w' v₁ v₂ u₁ u₂
namespace CategoryTheory
open Category
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
(W : MorphismProperty C) {M : Type w'} [AddMonoid M] [HasShift C M] [HasShift D M]
[W.IsCompatibleWithShift M]
namespace Localization
section
variable (X Y : C)
variable (M) in
/-- Given objects `X` and `Y` in a category `C`, this is the property that
all the types of morphisms from `X⟦a⟧` to `Y⟦b⟧` are `w`-small
in the localized category with respect to a class of morphisms `W`. -/
abbrev HasSmallLocalizedShiftedHom : Prop :=
∀ (a b : M), HasSmallLocalizedHom.{w} W (X⟦a⟧) (Y⟦b⟧)
variable (M) in
lemma hasSmallLocalizedShiftedHom_iff
(L : C ⥤ D) [L.IsLocalization W] [L.CommShift M] (X Y : C) :
HasSmallLocalizedShiftedHom.{w} W M X Y ↔
∀ (a b : M), Small.{w} ((L.obj X)⟦a⟧ ⟶ (L.obj Y)⟦b⟧) := by
dsimp [HasSmallLocalizedShiftedHom]
have eq := fun (a b : M) ↦ small_congr.{w}
(Iso.homCongr ((L.commShiftIso a).app X) ((L.commShiftIso b).app Y))
dsimp at eq
simp only [hasSmallLocalizedHom_iff _ L, eq]
variable [HasSmallLocalizedShiftedHom.{w} W M X Y]
variable (M) in
lemma hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ :
HasSmallLocalizedHom.{w} W X Y :=
(hasSmallLocalizedHom_iff_of_isos W
((shiftFunctorZero C M).app X) ((shiftFunctorZero C M).app Y)).1 inferInstance
instance (m : M) : HasSmallLocalizedHom.{w} W X (Y⟦m⟧) :=
(hasSmallLocalizedHom_iff_of_isos W
((shiftFunctorZero C M).app X) (Iso.refl (Y⟦m⟧))).1 inferInstance
instance (m : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧) Y :=
(hasSmallLocalizedHom_iff_of_isos W
(Iso.refl (X⟦m⟧)) ((shiftFunctorZero C M).app Y)).1 inferInstance
instance (m m' n : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧⟦m'⟧) (Y⟦n⟧) :=
(hasSmallLocalizedHom_iff_of_isos W
((shiftFunctorAdd C m m').app X) (Iso.refl (Y⟦n⟧))).1 inferInstance
instance (m n n' : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧) (Y⟦n⟧⟦n'⟧) :=
(hasSmallLocalizedHom_iff_of_isos W
(Iso.refl (X⟦m⟧)) ((shiftFunctorAdd C n n').app Y)).1 inferInstance
end
namespace SmallHom
variable {W}
variable (L : C ⥤ D) [L.IsLocalization W] [L.CommShift M]
{X Y : C} [HasSmallLocalizedHom.{w} W X Y]
(f : SmallHom.{w} W X Y) (a : M) [HasSmallLocalizedHom.{w} W (X⟦a⟧) (Y⟦a⟧)]
/-- Given `f : SmallHom W X Y` and `a : M`, this is the element
in `SmallHom W (X⟦a⟧) (Y⟦a⟧)` obtained by shifting by `a`. -/
noncomputable def shift : SmallHom.{w} W (X⟦a⟧) (Y⟦a⟧) :=
(W.shiftLocalizerMorphism a).smallHomMap f
lemma equiv_shift : equiv W L (f.shift a) =
(L.commShiftIso a).hom.app X ≫ (equiv W L f)⟦a⟧' ≫ (L.commShiftIso a).inv.app Y :=
(W.shiftLocalizerMorphism a).equiv_smallHomMap _ _ _ (L.commShiftIso a) f
end SmallHom
/-- The type of morphisms from `X` to `Y⟦m⟧` in the localized category
with respect to `W : MorphismProperty C` that is shrunk to `Type w`
when `HasSmallLocalizedShiftedHom.{w} W X Y` holds. -/
def SmallShiftedHom (X Y : C) [HasSmallLocalizedShiftedHom.{w} W M X Y] (m : M) : Type w :=
SmallHom W X (Y⟦m⟧)
namespace SmallShiftedHom
section
variable {W}
variable {X Y Z : C}
/-- Given `f : SmallShiftedHom.{w} W X Y a`, this is the element in
`SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧)` that is obtained by shifting by `n`
when `a + n = a'`. -/
noncomputable def shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧) :=
(SmallHom.shift f n).comp (SmallHom.mk W ((shiftFunctorAdd' C a n a' h).inv.app Y))
/-- The composition on `SmallShiftedHom W`. -/
noncomputable def comp {a b c : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M X Z]
[HasSmallLocalizedShiftedHom.{w} W M Z Z]
(f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
SmallShiftedHom.{w} W X Z c :=
SmallHom.comp f (g.shift a c h)
variable (W) in
/-- The canonical map `(X ⟶ Y) → SmallShiftedHom.{w} W X Y m₀` when `m₀ = 0` and
`[HasSmallLocalizedShiftedHom.{w} W M X Y]` holds. -/
noncomputable def mk₀ [HasSmallLocalizedShiftedHom.{w} W M X Y]
(m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
SmallShiftedHom.{w} W X Y m₀ :=
SmallHom.mk W (f ≫ (shiftFunctorZero' C m₀ hm₀).inv.app Y)
end
section
variable (L : C ⥤ D) [L.IsLocalization W] [HasShift D M] [L.CommShift M]
{X Y Z T : C}
/-- The bijection `SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m`
for all `m : M`, and `X` and `Y` in `C` when `L : C ⥤ D` is a localization functor for
`W : MorphismProperty C` such that the category `D` is equipped with a shift by `M`
and `L` commutes with the shifts. -/
noncomputable def equiv [HasSmallLocalizedShiftedHom.{w} W M X Y] {m : M} :
SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m :=
(SmallHom.equiv W L).trans ((L.commShiftIso m).app Y).homToEquiv
lemma equiv_shift' {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
SmallHom.equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫
(SmallHom.equiv W L f)⟦n⟧' ≫ ((L.commShiftIso a).hom.app Y)⟦n⟧' ≫
(shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y := by
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc,
L.commShiftIso_add' h, Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc,
← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]
lemma equiv_shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫ (equiv W L f)⟦n⟧' ≫
(shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) := by
dsimp [equiv]
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, equiv_shift']
simp only [Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
rfl
lemma equiv_comp [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M X Z]
[HasSmallLocalizedShiftedHom.{w} W M Z Z] {a b c : M}
(f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
equiv W L (f.comp g h) = (equiv W L f).comp (equiv W L g) h := by
dsimp [comp, equiv, ShiftedHom.comp]
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply, SmallHom.equiv_comp]
simp only [equiv_shift', Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app,
comp_id, Functor.map_comp]
rfl
@[simp]
lemma equiv_mk₀ [HasSmallLocalizedShiftedHom.{w} W M X Y]
(m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
equiv W L (SmallShiftedHom.mk₀ W m₀ hm₀ f) =
ShiftedHom.mk₀ m₀ hm₀ (L.map f) := by
subst hm₀
dsimp [equiv, mk₀]
erw [SmallHom.equiv_mk, Iso.homToEquiv_apply, Functor.map_comp]
dsimp [equiv, mk₀, ShiftedHom.mk₀, shiftFunctorZero']
simp only [comp_id, L.commShiftIso_zero, Functor.CommShift.isoZero_hom_app, assoc,
← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id, id_comp]
end
lemma comp_assoc {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M}
[HasSmallLocalizedShiftedHom.{w} W M X Y] [HasSmallLocalizedShiftedHom.{w} W M X Z]
[HasSmallLocalizedShiftedHom.{w} W M X T] [HasSmallLocalizedShiftedHom.{w} W M Y Z]
[HasSmallLocalizedShiftedHom.{w} W M Y T] [HasSmallLocalizedShiftedHom.{w} W M Z T]
[HasSmallLocalizedShiftedHom.{w} W M Z Z] [HasSmallLocalizedShiftedHom.{w} W M T T]
(α : SmallShiftedHom.{w} W X Y a₁) (β : SmallShiftedHom.{w} W Y Z a₂)
(γ : SmallShiftedHom.{w} W Z T a₃)
(h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
(α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) =
α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h]) := by
apply (equiv W W.Q).injective
simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]
end SmallShiftedHom
end Localization
end CategoryTheory