Theorems · Theorem · category theory

CategoryTheory.Quotient.LiftCommShift.iso_inv_app

∀ {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]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (a : A) (X : C),
  (CategoryTheory.Quotient.LiftCommShift.iso F r hF a).inv.app ((CategoryTheory.Quotient.functor r).obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
      ((CategoryTheory.Quotient.lift r F hF).map
        ((CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.functor r) a).hom.app X))

Defined in

Mathlib.CategoryTheory.Shift.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

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