Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk

∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type w'}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_9 : CategoryTheory.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 : CategoryTheory.ShiftedHom X₁ Y₁ m),
  Φ.smallShiftedHomMap eX eY (CategoryTheory.Localization.SmallShiftedHom.mk W₁ f) =
    CategoryTheory.Localization.SmallShiftedHom.mk W₂
      ((CategoryTheory.ShiftedHom.mk₀ 0 ⋯ eX.inv).comp
        ((f.map Φ.functor).comp (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.MorphismProperty.IsCompatibleWithShiftCategoryTheory.MorphismProperty.IsCompatibleWithShift