Theorems · Theorem · category theory

CategoryTheory.Quotient.liftCommShift_commShiftIso

∀ {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),
  CategoryTheory.Functor.commShiftIso (CategoryTheory.Quotient.lift r F hF) a =
    CategoryTheory.Quotient.LiftCommShift.iso F r hF a

Defined in

Mathlib.CategoryTheory.Shift.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

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