Theorems · Theorem · category theory

CategoryTheory.Localization.SmallHom.equiv_shift

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {W : CategoryTheory.MorphismProperty C} {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] [inst_5 : W.IsCompatibleWithShift M] (L : CategoryTheory.Functor C D)
  [inst_6 : L.IsLocalization W] [inst_7 : L.CommShift M] {X Y : C}
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : CategoryTheory.Localization.SmallHom W X Y)
  (a : M)
  [inst_9 :
    CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X)
      ((CategoryTheory.shiftFunctor C a).obj Y)],
  (CategoryTheory.Localization.SmallHom.equiv W L) (f.shift a) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L a).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Localization.SmallHom.equiv W L) f))
        ((CategoryTheory.Functor.commShiftIso L a).inv.app Y))

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.MorphismProperty.IsCompatibleWithShiftCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.CommShiftCategoryTheory.Localization.HasSmallLocalizedHomCategoryTheory.Localization.HasSmallLocalizedHom