Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.smallShiftedHomMap.congr_simp

∀ {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 eX_1 : Φ.functor.obj X₁ ≅ X₂),
  eX = eX_1 →
    ∀ (eY eY_1 : Φ.functor.obj Y₁ ≅ Y₂),
      eY = eY_1 →
        ∀ {m : M} (f f_1 : CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m),
          f = f_1 → Φ.smallShiftedHomMap eX eY f = Φ.smallShiftedHomMap eX_1 eY_1 f_1

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHomCategoryTheory.Localization.HasSmallLocalizedShiftedHom