Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.smallShiftedHomMap

{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] →
                      [Φ.functor.CommShift M] →
                        {X₁ Y₁ : C₁} →
                          {X₂ Y₂ : C₂} →
                            [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁] →
                              [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂] →
                                [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂] →
                                  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] →
                                    (Φ.functor.obj X₁ ≅ X₂) →
                                      (Φ.functor.obj Y₁ ≅ Y₂) →
                                        {m : M} →
                                          CategoryTheory.Localization.SmallShiftedHom W₁ X₁ Y₁ m →
                                            CategoryTheory.Localization.SmallShiftedHom W₂ X₂ Y₂ m

The action of a localizer morphism Φ on SmallShiftedHom.

Defined in

Mathlib.CategoryTheory.Localization.SmallShiftedHom

Cited by

5 results in Mathlib

Foundations

Depth 93 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