Theorems · Definition · category theory

CategoryTheory.Quotient.LiftCommShift.iso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (F : CategoryTheory.Functor C D) →
          (r : HomRel C) →
            {A : Type w} →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] →
                    [inst_5 : r.IsCompatibleWithShift A] →
                      [F.CommShift A] →
                        (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
                          (a : A) →
                            (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) a).comp
                                (CategoryTheory.Quotient.lift r F hF) ≅
                              (CategoryTheory.Quotient.lift r F hF).comp (CategoryTheory.shiftFunctor D a)

Auxiliary definition for Quotient.liftCommShift.

Defined in

Mathlib.CategoryTheory.Shift.Quotient

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftHomRel.IsCompatibleWithShiftCategoryTheory.Functor.CommShift