Skip to content

Commit bd38094

Browse files
joelriouriccardobrasca
joelriou
and
riccardobrasca
committed
feat: small types of shifted hom in the localized category (#13926)
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`. This shall be used in the redefinition of `Ext`-groups in abelian categories. Co-authored-by: Riccardo Brasca <[email protected]> Co-authored-by: Joël Riou <[email protected]>
1 parent cc796ed commit bd38094

File tree

4 files changed

+221
-3
lines changed

4 files changed

+221
-3
lines changed

‎Mathlib.lean

+1
Original file line numberDiff line numberDiff line change
@@ -1561,6 +1561,7 @@ import Mathlib.CategoryTheory.Localization.Predicate
15611561
import Mathlib.CategoryTheory.Localization.Prod
15621562
import Mathlib.CategoryTheory.Localization.Resolution
15631563
import Mathlib.CategoryTheory.Localization.SmallHom
1564+
import Mathlib.CategoryTheory.Localization.SmallShiftedHom
15641565
import Mathlib.CategoryTheory.Localization.Triangulated
15651566
import Mathlib.CategoryTheory.Monad.Adjunction
15661567
import Mathlib.CategoryTheory.Monad.Algebra

‎Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean

+187
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
import Mathlib.CategoryTheory.Localization.SmallHom
7+
import Mathlib.CategoryTheory.Shift.ShiftedHom
8+
import Mathlib.CategoryTheory.Shift.Localization
9+
10+
/-!
11+
# Shrinking morphisms in localized categories equipped with shifts
12+
13+
If `C` is a category equipped with a shift by an additive monoid `M`,
14+
and `W : MorphismProperty C` is compatible with the shift,
15+
we define a type-class `HasSmallLocalizedShiftedHom.{w} W X Y` which
16+
says that all the types of morphisms from `X⟦a⟧` to `Y⟦b⟧` in the
17+
localized category are `w`-small for a certain universe. Then,
18+
we define types `SmallShiftedHom.{w} W X Y m : Type w` for all `m : M`,
19+
and endow these with a composition which transports the composition
20+
on the types `ShiftedHom (L.obj X) (L.obj Y) m` when `L : C ⥤ D` is
21+
any localization functor for `W`.
22+
23+
-/
24+
25+
universe w w' v₁ v₂ u₁ u₂
26+
27+
namespace CategoryTheory
28+
29+
open Category
30+
31+
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
32+
(W : MorphismProperty C) {M : Type w'} [AddMonoid M] [HasShift C M] [HasShift D M]
33+
[W.IsCompatibleWithShift M]
34+
35+
namespace Localization
36+
37+
section
38+
39+
variable (X Y : C)
40+
41+
variable (M) in
42+
/-- Given objects `X` and `Y` in a category `C`, this is the property that
43+
all the types of morphisms from `X⟦a⟧` to `Y⟦b⟧` are `w`-small
44+
in the localized category with respect to a class of morphisms `W`. -/
45+
abbrev HasSmallLocalizedShiftedHom : Prop :=
46+
∀ (a b : M), HasSmallLocalizedHom.{w} W (X⟦a⟧) (Y⟦b⟧)
47+
48+
variable [HasSmallLocalizedShiftedHom.{w} W M X Y]
49+
50+
variable (M) in
51+
lemma hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ :
52+
HasSmallLocalizedHom.{w} W X Y :=
53+
(hasSmallLocalizedHom_iff_of_isos W
54+
((shiftFunctorZero C M).app X) ((shiftFunctorZero C M).app Y)).1 inferInstance
55+
56+
instance (m : M) : HasSmallLocalizedHom.{w} W X (Y⟦m⟧) :=
57+
(hasSmallLocalizedHom_iff_of_isos W
58+
((shiftFunctorZero C M).app X) (Iso.refl (Y⟦m⟧))).1 inferInstance
59+
60+
instance (m : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧) Y :=
61+
(hasSmallLocalizedHom_iff_of_isos W
62+
(Iso.refl (X⟦m⟧)) ((shiftFunctorZero C M).app Y)).1 inferInstance
63+
64+
instance (m m' n : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧⟦m'⟧) (Y⟦n⟧) :=
65+
(hasSmallLocalizedHom_iff_of_isos W
66+
((shiftFunctorAdd C m m').app X) (Iso.refl (Y⟦n⟧))).1 inferInstance
67+
68+
instance (m n n' : M) : HasSmallLocalizedHom.{w} W (X⟦m⟧) (Y⟦n⟧⟦n'⟧) :=
69+
(hasSmallLocalizedHom_iff_of_isos W
70+
(Iso.refl (X⟦m⟧)) ((shiftFunctorAdd C n n').app Y)).1 inferInstance
71+
72+
end
73+
74+
namespace SmallHom
75+
76+
variable {W}
77+
variable (L : C ⥤ D) [L.IsLocalization W] [L.CommShift M]
78+
{X Y : C} [HasSmallLocalizedHom.{w} W X Y]
79+
(f : SmallHom.{w} W X Y) (a : M) [HasSmallLocalizedHom.{w} W (X⟦a⟧) (Y⟦a⟧)]
80+
81+
/-- Given `f : SmallHom W X Y` and `a : M`, this is the element
82+
in `SmallHom W (X⟦a⟧) (Y⟦a⟧)` obtained by shifting by `a`. -/
83+
noncomputable def shift : SmallHom.{w} W (X⟦a⟧) (Y⟦a⟧) :=
84+
(W.shiftLocalizerMorphism a).smallHomMap f
85+
86+
lemma equiv_shift : equiv W L (f.shift a) =
87+
(L.commShiftIso a).hom.app X ≫ (equiv W L f)⟦a⟧' ≫ (L.commShiftIso a).inv.app Y :=
88+
(W.shiftLocalizerMorphism a).equiv_smallHomMap _ _ _ (L.commShiftIso a) f
89+
90+
end SmallHom
91+
92+
/-- The type of morphisms from `X` to `Y⟦m⟧` in the localized category
93+
with respect to `W : MorphismProperty C` that is shrunk to `Type w`
94+
when `HasSmallLocalizedShiftedHom.{w} W X Y` holds. -/
95+
def SmallShiftedHom (X Y : C) [HasSmallLocalizedShiftedHom.{w} W M X Y] (m : M) : Type w :=
96+
SmallHom W X (Y⟦m⟧)
97+
98+
namespace SmallShiftedHom
99+
100+
section
101+
102+
variable {W}
103+
variable {X Y Z : C}
104+
105+
/-- Given `f : SmallShiftedHom.{w} W X Y a`, this is the element in
106+
`SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧)` that is obtained by shifting by `n`
107+
when `a + n = a'`. -/
108+
noncomputable def shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
109+
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
110+
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
111+
SmallHom.{w} W (X⟦n⟧) (Y⟦a'⟧) :=
112+
(SmallHom.shift f n).comp (SmallHom.mk W ((shiftFunctorAdd' C a n a' h).inv.app Y))
113+
114+
/-- The composition on `SmallShiftedHom W`. -/
115+
noncomputable def comp {a b c : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
116+
[HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M X Z]
117+
[HasSmallLocalizedShiftedHom.{w} W M Z Z]
118+
(f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
119+
SmallShiftedHom.{w} W X Z c :=
120+
SmallHom.comp f (g.shift a c h)
121+
122+
end
123+
124+
section
125+
126+
variable (L : C ⥤ D) [L.IsLocalization W] [HasShift D M] [L.CommShift M]
127+
{X Y Z T : C}
128+
129+
/-- The bijection `SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m`
130+
for all `m : M`, and `X` and `Y` in `C` when `L : C ⥤ D` is a localization functor for
131+
`W : MorphismProperty C` such that the category `D` is equipped with a shift by `M`
132+
and `L` commutes with the shifts. -/
133+
noncomputable def equiv [HasSmallLocalizedShiftedHom.{w} W M X Y] {m : M} :
134+
SmallShiftedHom.{w} W X Y m ≃ ShiftedHom (L.obj X) (L.obj Y) m :=
135+
(SmallHom.equiv W L).trans ((L.commShiftIso m).app Y).homToEquiv
136+
137+
lemma equiv_shift' {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
138+
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
139+
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
140+
SmallHom.equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫
141+
(SmallHom.equiv W L f)⟦n⟧' ≫ ((L.commShiftIso a).hom.app Y)⟦n⟧' ≫
142+
(shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y := by
143+
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc,
144+
L.commShiftIso_add' h, Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc,
145+
← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]
146+
147+
lemma equiv_shift {a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
148+
[HasSmallLocalizedShiftedHom.{w} W M Y Y]
149+
(f : SmallShiftedHom.{w} W X Y a) (n a' : M) (h : a + n = a') :
150+
equiv W L (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫ (equiv W L f)⟦n⟧' ≫
151+
(shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) := by
152+
dsimp [equiv]
153+
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, equiv_shift']
154+
simp only [Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
155+
rfl
156+
157+
lemma equiv_comp [HasSmallLocalizedShiftedHom.{w} W M X Y]
158+
[HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M X Z]
159+
[HasSmallLocalizedShiftedHom.{w} W M Z Z] {a b c : M}
160+
(f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
161+
equiv W L (f.comp g h) = (equiv W L f).comp (equiv W L g) h := by
162+
dsimp [comp, equiv, ShiftedHom.comp]
163+
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply, SmallHom.equiv_comp]
164+
simp only [equiv_shift', Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app,
165+
comp_id, Functor.map_comp]
166+
rfl
167+
168+
end
169+
170+
lemma comp_assoc {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M}
171+
[HasSmallLocalizedShiftedHom.{w} W M X Y] [HasSmallLocalizedShiftedHom.{w} W M X Z]
172+
[HasSmallLocalizedShiftedHom.{w} W M X T] [HasSmallLocalizedShiftedHom.{w} W M Y Z]
173+
[HasSmallLocalizedShiftedHom.{w} W M Y T] [HasSmallLocalizedShiftedHom.{w} W M Z T]
174+
[HasSmallLocalizedShiftedHom.{w} W M Z Z] [HasSmallLocalizedShiftedHom.{w} W M T T]
175+
(α : SmallShiftedHom.{w} W X Y a₁) (β : SmallShiftedHom.{w} W Y Z a₂)
176+
(γ : SmallShiftedHom.{w} W Z T a₃)
177+
(h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
178+
(α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) =
179+
α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h]) := by
180+
apply (equiv W W.Q).injective
181+
simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]
182+
183+
end SmallShiftedHom
184+
185+
end Localization
186+
187+
end CategoryTheory

‎Mathlib/CategoryTheory/Shift/Localization.lean

+8
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Joël Riou
55
-/
66
import Mathlib.CategoryTheory.Shift.Induced
77
import Mathlib.CategoryTheory.Localization.HasLocalization
8+
import Mathlib.CategoryTheory.Localization.LocalizerMorphism
89

910
/-!
1011
# The shift induced on a localized category
@@ -51,6 +52,13 @@ lemma shiftFunctor_comp_inverts (a : A) :
5152

5253
end IsCompatibleWithShift
5354

55+
variable {A} in
56+
/-- The morphism of localizer from `W` to `W` given by the functor `shiftFunctor C a`
57+
when `a : A` and `W` is compatible with the shift by `A`. -/
58+
abbrev shiftLocalizerMorphism (a : A) : LocalizerMorphism W W where
59+
functor := shiftFunctor C a
60+
map := by rw [MorphismProperty.IsCompatibleWithShift.condition]
61+
5462
end MorphismProperty
5563

5664
variable [W.IsCompatibleWithShift A]

‎Mathlib/CategoryTheory/Shift/ShiftedHom.lean

+25-3
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joël Riou
55
-/
6-
import Mathlib.CategoryTheory.Shift.Basic
6+
import Mathlib.CategoryTheory.Shift.CommShift
77
import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
88

99
/-! Shifted morphisms
@@ -24,8 +24,8 @@ namespace CategoryTheory
2424

2525
open Category
2626

27-
variable {C : Type*} [Category C]
28-
{M : Type*} [AddMonoid M] [HasShift C M]
27+
variable {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*} [Category E]
28+
{M : Type*} [AddMonoid M] [HasShift C M] [HasShift D M] [HasShift E M]
2929

3030
/-- In a category `C` equipped with a shift by an additive monoid,
3131
this is the type of morphisms `X ⟶ (Y⟦n⟧)` for `m : M`. -/
@@ -121,6 +121,28 @@ lemma zero_comp (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) :
121121

122122
end Preadditive
123123

124+
/-- The action on `ShiftedHom` of a functor which commutes with the shift. -/
125+
def map {a : M} (f : ShiftedHom X Y a) (F : C ⥤ D) [F.CommShift M] :
126+
ShiftedHom (F.obj X) (F.obj Y) a :=
127+
F.map f ≫ (F.commShiftIso a).hom.app Y
128+
129+
@[simp]
130+
lemma id_map {a : M} (f : ShiftedHom X Y a) : f.map (𝟭 C) = f := by
131+
simp [map, Functor.commShiftIso, Functor.CommShift.iso]
132+
133+
lemma comp_map {a : M} (f : ShiftedHom X Y a) (F : C ⥤ D) [F.CommShift M]
134+
(G : D ⥤ E) [G.CommShift M] : f.map (F ⋙ G) = (f.map F).map G := by
135+
simp [map, Functor.commShiftIso_comp_hom_app]
136+
137+
lemma map_comp {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b)
138+
(h : b + a = c) (F : C ⥤ D) [F.CommShift M] :
139+
(f.comp g h).map F = (f.map F).comp (g.map F) h := by
140+
dsimp [comp, map]
141+
simp only [Functor.map_comp, assoc]
142+
erw [← NatTrans.naturality_assoc]
143+
simp only [Functor.comp_map, F.commShiftIso_add' h, Functor.CommShift.isoAdd'_hom_app,
144+
← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.comp_obj, comp_id, assoc]
145+
124146
end ShiftedHom
125147

126148
end CategoryTheory

0 commit comments

Comments
 (0)