Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap

∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {D₁ : Type u₁'} [inst_2 : CategoryTheory.Category.{v₁', u₁'} D₁]
  {D₂ : Type u₂'} [inst_3 : CategoryTheory.Category.{v₂', u₂'} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {M : Type w'} [inst_6 : AddMonoid M] [inst_7 : CategoryTheory.HasShift C₁ M]
  [inst_8 : CategoryTheory.HasShift C₂ M] [inst_9 : CategoryTheory.HasShift D₁ M]
  [inst_10 : CategoryTheory.HasShift D₂ M] [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M]
  [inst_13 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_14 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_15 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_16 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_17 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂)
  (eY : Φ.functor.obj Y₁ ≅ Y₂) (G : CategoryTheory.Functor D₁ D₂) [inst_18 : G.CommShift M]
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) [CategoryTheory.NatTrans.CommShift e.hom M] {m : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W₂ L₂) (Φ.smallShiftedHomMap eX eY f) =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (CategoryTheory.CategoryStruct.comp (L₂.map eX.inv) (e.hom.app X₁))).comp
      ((((CategoryTheory.Localization.SmallShiftedHom.equiv W₁ L₁) f).map G).comp
        (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (CategoryTheory.CategoryStruct.comp (e.inv.app Y₁) (L₂.map eY.hom))) ⋯)
      ⋯

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShiftCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Functor.CommShiftCategoryTheory.NatTrans.CommShift