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.
@[reducible, inline]
abbrev
CategoryTheory.Localization.HasSmallLocalizedShiftedHom
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X Y : C)
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
(X Y : C)
:
HasSmallLocalizedShiftedHom W M X Y ↔ ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
theorem
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X : C)
{Y : C}
[W.IsCompatibleWithShift M]
{Y' : C}
(f : Y ⟶ Y')
(hf : W f)
:
theorem
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_source
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
{X : C}
[W.IsCompatibleWithShift M]
{X' : C}
(f : X ⟶ X')
(hf : W f)
(Y : C)
:
theorem
CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
(M : Type w')
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
:
HasSmallLocalizedHom W X Y
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
HasSmallLocalizedHom W X ((shiftFunctor C m).obj Y)
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_1
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m).obj X) Y
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m m' n : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m').obj ((shiftFunctor C m).obj X)) ((shiftFunctor C n).obj Y)
instance
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_3
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m n n' : M)
:
HasSmallLocalizedHom W ((shiftFunctor C m).obj X) ((shiftFunctor C n').obj ((shiftFunctor C n).obj Y))
noncomputable def
CategoryTheory.Localization.SmallHom.shift
{C : Type u₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y : C}
[HasSmallLocalizedHom W X Y]
(f : SmallHom W X Y)
(a : M)
[HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)]
:
SmallHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)
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.
Equations
- f.shift a = (W.shiftLocalizerMorphism a).smallHomMap f
Instances For
theorem
CategoryTheory.Localization.SmallHom.equiv_shift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
[W.IsCompatibleWithShift M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedHom W X Y]
(f : SmallHom W X Y)
(a : M)
[HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)]
:
(equiv W L) (f.shift a) = CategoryStruct.comp ((Functor.commShiftIso L a).hom.app X)
(CategoryStruct.comp ((shiftFunctor D a).map ((equiv W L) f)) ((Functor.commShiftIso L a).inv.app Y))
def
CategoryTheory.Localization.SmallShiftedHom
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
(X Y : C)
[HasSmallLocalizedShiftedHom W M X Y]
(m : M)
:
Type w
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.
Equations
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.mk
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
{X Y : C}
{m : M}
[HasSmallLocalizedShiftedHom W M X Y]
(f : ShiftedHom X Y m)
:
SmallShiftedHom W X Y m
Constructor for SmallShiftedHom.
Equations
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.shift
{C : Type u₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y : C}
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
SmallHom W ((shiftFunctor C n).obj X) ((shiftFunctor C a').obj Y)
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'.
Equations
- f.shift n a' h = (CategoryTheory.Localization.SmallHom.shift f n).comp (CategoryTheory.Localization.SmallHom.mk W ((CategoryTheory.shiftFunctorAdd' C a n a' h).inv.app Y))
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y Z : C}
{a b c : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M Z Z]
(f : SmallShiftedHom W X Y a)
(g : SmallShiftedHom W Y Z b)
(h : b + a = c)
:
SmallShiftedHom W X Z c
The composition on SmallShiftedHom W.
Equations
- f.comp g h = CategoryTheory.Localization.SmallHom.comp f (g.shift a c h)
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.mk₀
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X ⟶ Y)
:
SmallShiftedHom W X Y m₀
The canonical map (X ⟶ Y) → SmallShiftedHom.{w} W X Y m₀ when m₀ = 0 and
[HasSmallLocalizedShiftedHom.{w} W M X Y] holds.
Equations
Instances For
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
{m : M}
:
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.
Equations
Instances For
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_apply
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
{m : M}
(f : SmallShiftedHom W X Y m)
:
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_shift'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[W.IsCompatibleWithShift M]
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
(SmallHom.equiv W L) (f.shift n a' h) = CategoryStruct.comp ((Functor.commShiftIso L n).hom.app X)
(CategoryStruct.comp ((shiftFunctor D n).map ((SmallHom.equiv W L) f))
(CategoryStruct.comp ((shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y))
(CategoryStruct.comp ((shiftFunctorAdd' D a n a' h).inv.app (L.obj Y))
((Functor.commShiftIso L a').inv.app Y))))
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_shift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[W.IsCompatibleWithShift M]
{a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Y]
(f : SmallShiftedHom W X Y a)
(n a' : M)
(h : a + n = a')
:
(equiv W L) (f.shift n a' h) = CategoryStruct.comp ((Functor.commShiftIso L n).hom.app X)
(CategoryStruct.comp ((shiftFunctor D n).map ((equiv W L) f)) ((shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)))
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y Z : C}
[W.IsCompatibleWithShift M]
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M Z Z]
{a b c : M}
(f : SmallShiftedHom W X Y a)
(g : SmallShiftedHom W Y Z b)
(h : b + a = c)
:
@[simp]
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_mk
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
{m : M}
(f : ShiftedHom X Y m)
:
@[simp]
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
[HasSmallLocalizedShiftedHom W M X Y]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X ⟶ Y)
:
theorem
CategoryTheory.Localization.SmallShiftedHom.comp_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
(W : MorphismProperty C)
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[W.IsCompatibleWithShift M]
{X Y Z T : C}
{a₁ a₂ a₃ a₁₂ a₂₃ a : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Z]
[HasSmallLocalizedShiftedHom W M X T]
[HasSmallLocalizedShiftedHom W M Y Z]
[HasSmallLocalizedShiftedHom W M Y T]
[HasSmallLocalizedShiftedHom W M Z T]
[HasSmallLocalizedShiftedHom W M Z Z]
[HasSmallLocalizedShiftedHom W M T T]
(α : SmallShiftedHom W X Y a₁)
(β : SmallShiftedHom W Y Z a₂)
(γ : SmallShiftedHom W Z T a₃)
(h₁₂ : a₂ + a₁ = a₁₂)
(h₂₃ : a₃ + a₂ = a₂₃)
(h : a₃ + a₂ + a₁ = a)
:
noncomputable def
CategoryTheory.Localization.SmallShiftedHom.chgUniv
{C : Type u₁}
[Category.{v₁, u₁} C]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
{X Y : C}
{m : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Y]
:
Up to an equivalence, the type SmallShiftedHom.{w} W X Y m does
not depend on the universe w.
Equations
Instances For
theorem
CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{W : MorphismProperty C}
{M : Type w'}
[AddMonoid M]
[HasShift C M]
[HasShift D M]
(L : Functor C D)
[L.IsLocalization W]
[L.CommShift M]
{X Y : C}
{m : M}
[HasSmallLocalizedShiftedHom W M X Y]
[HasSmallLocalizedShiftedHom W M X Y]
(e : SmallShiftedHom W X Y m)
:
noncomputable def
CategoryTheory.LocalizerMorphism.smallShiftedHomMap
{C₁ : Type u₁}
[Category.{v₁, u₁} C₁]
{C₂ : Type u₂}
[Category.{v₂, u₂} C₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
{M : Type w'}
[AddMonoid M]
[HasShift C₁ M]
[HasShift C₂ M]
[Φ.functor.CommShift M]
{X₁ Y₁ : C₁}
{X₂ Y₂ : C₂}
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂]
(eX : Φ.functor.obj X₁ ≅ X₂)
(eY : Φ.functor.obj Y₁ ≅ Y₂)
{m : M}
(f : Localization.SmallShiftedHom W₁ X₁ Y₁ m)
:
Localization.SmallShiftedHom W₂ X₂ Y₂ m
The action of a localizer morphism Φ on SmallShiftedHom.
Equations
- Φ.smallShiftedHomMap eX eY f = Φ.smallHomMap' eX ((CategoryTheory.Functor.commShiftIso Φ.functor m).app Y₁ ≪≫ (CategoryTheory.shiftFunctor C₂ m).mapIso eY) f
Instances For
theorem
CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap
{C₁ : Type u₁}
[Category.{v₁, u₁} C₁]
{C₂ : Type u₂}
[Category.{v₂, u₂} C₂]
{D₁ : Type u₁'}
[Category.{v₁', u₁'} D₁]
{D₂ : Type u₂'}
[Category.{v₂', u₂'} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
(L₂ : Functor C₂ D₂)
[L₁.IsLocalization W₁]
[L₂.IsLocalization W₂]
{M : Type w'}
[AddMonoid M]
[HasShift C₁ M]
[HasShift C₂ M]
[HasShift D₁ M]
[HasShift D₂ M]
[L₁.CommShift M]
[L₂.CommShift M]
[Φ.functor.CommShift M]
{X₁ Y₁ : C₁}
{X₂ Y₂ : C₂}
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂]
(eX : Φ.functor.obj X₁ ≅ X₂)
(eY : Φ.functor.obj Y₁ ≅ Y₂)
(G : Functor D₁ D₂)
[G.CommShift M]
(e : Φ.functor.comp L₂ ≅ L₁.comp G)
[NatTrans.CommShift e.hom M]
{m : M}
(f : Localization.SmallShiftedHom W₁ X₁ Y₁ m)
:
(Localization.SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) = (ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (L₂.map eX.inv) (e.hom.app X₁))).comp
((((Localization.SmallShiftedHom.equiv W₁ L₁) f).map G).comp
(ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (e.inv.app Y₁) (L₂.map eY.hom))) ⋯)
⋯
@[simp]
theorem
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk
{C₁ : Type u₁}
[Category.{v₁, u₁} C₁]
{C₂ : Type u₂}
[Category.{v₂, u₂} C₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
{M : Type w'}
[AddMonoid M]
[HasShift C₁ M]
[HasShift C₂ M]
[Φ.functor.CommShift M]
{X₁ Y₁ : C₁}
{X₂ Y₂ : C₂}
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂]
(eX : Φ.functor.obj X₁ ≅ X₂)
(eY : Φ.functor.obj Y₁ ≅ Y₂)
[W₁.IsCompatibleWithShift M]
[W₂.IsCompatibleWithShift M]
{m : M}
(f : ShiftedHom X₁ Y₁ m)
:
Φ.smallShiftedHomMap eX eY (Localization.SmallShiftedHom.mk W₁ f) = Localization.SmallShiftedHom.mk W₂
((ShiftedHom.mk₀ 0 ⋯ eX.inv).comp ((f.map Φ.functor).comp (ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)
theorem
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk₀
{C₁ : Type u₁}
[Category.{v₁, u₁} C₁]
{C₂ : Type u₂}
[Category.{v₂, u₂} C₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
{M : Type w'}
[AddMonoid M]
[HasShift C₁ M]
[HasShift C₂ M]
[Φ.functor.CommShift M]
{X₁ Y₁ : C₁}
{X₂ Y₂ : C₂}
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂]
(eX : Φ.functor.obj X₁ ≅ X₂)
(eY : Φ.functor.obj Y₁ ≅ Y₂)
[W₁.IsCompatibleWithShift M]
[W₂.IsCompatibleWithShift M]
(m₀ : M)
(hm₀ : m₀ = 0)
(f : X₁ ⟶ Y₁)
:
Φ.smallShiftedHomMap eX eY (Localization.SmallShiftedHom.mk₀ W₁ m₀ hm₀ f) = Localization.SmallShiftedHom.mk₀ W₂ m₀ hm₀ (CategoryStruct.comp eX.inv (CategoryStruct.comp (Φ.functor.map f) eY.hom))
theorem
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_comp
{C₁ : Type u₁}
[Category.{v₁, u₁} C₁]
{C₂ : Type u₂}
[Category.{v₂, u₂} C₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
{M : Type w'}
[AddMonoid M]
[HasShift C₁ M]
[HasShift C₂ M]
[Φ.functor.CommShift M]
{X₁ Y₁ Z₁ : C₁}
{X₂ Y₂ Z₂ : C₂}
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂]
(eX : Φ.functor.obj X₁ ≅ X₂)
(eY : Φ.functor.obj Y₁ ≅ Y₂)
(eZ : Φ.functor.obj Z₁ ≅ Z₂)
[W₁.IsCompatibleWithShift M]
[W₂.IsCompatibleWithShift M]
[Localization.HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂]
[Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂]
[Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Z₁]
[Localization.HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁]
[Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Z₂]
{a b c : M}
(f : Localization.SmallShiftedHom W₁ X₁ Y₁ a)
(g : Localization.SmallShiftedHom W₁ Y₁ Z₁ b)
(h : b + a = c)
:
Φ.smallShiftedHomMap eX eZ (f.comp g h) = (Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h