Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.commShift

{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              (M : Type u_3) →
                [inst_2 : AddMonoid M] →
                  [inst_3 : CategoryTheory.HasShift C₁ M] →
                    [inst_4 : CategoryTheory.HasShift C₂ M] →
                      [Φ.functor.CommShift M] →
                        {D₁ : Type u_4} →
                          {D₂ : Type u_5} →
                            [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁] →
                              [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] →
                                (L₁ : CategoryTheory.Functor C₁ D₁) →
                                  [L₁.IsLocalization W₁] →
                                    (L₂ : CategoryTheory.Functor C₂ D₂) →
                                      [inst_9 : CategoryTheory.HasShift D₁ M] →
                                        [inst_10 : CategoryTheory.HasShift D₂ M] →
                                          [L₁.CommShift M] →
                                            [L₂.CommShift M] →
                                              (G : CategoryTheory.Functor D₁ D₂) →
                                                (Φ.functor.comp L₂ ≅ L₁.comp G) → G.CommShift M

This is the commutation of a functor G to shifts by an additive monoid M when e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G is an isomorphism, Φ is a localizer morphism and L₁ is a localization functor. We assume that all categories involved are equipped with shifts and that L₁, L₂ and Φ.functor commute to them.

Defined in

Mathlib.CategoryTheory.Shift.Localization

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShiftCategoryTheory.Functor.CommShift