Theorems · Theorem · category theory

CategoryTheory.Functor.isTriangulated_of_precomp

∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  [inst_8 : CategoryTheory.Limits.HasZeroObject C] [inst_9 : CategoryTheory.Limits.HasZeroObject D]
  [inst_10 : CategoryTheory.Limits.HasZeroObject E] [inst_11 : CategoryTheory.Preadditive C]
  [inst_12 : CategoryTheory.Preadditive D] [inst_13 : CategoryTheory.Preadditive E]
  [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_15 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_16 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [inst_17 : CategoryTheory.Pretriangulated C]
  [inst_18 : CategoryTheory.Pretriangulated D] [inst_19 : CategoryTheory.Pretriangulated E] [(F.comp G).IsTriangulated]
  [F.IsTriangulated] [F.mapArrow.EssSurj], G.IsTriangulated

Defined in: Mathlib.CategoryTheory.Triangulated.Functor
Cited by: 1 results in Mathlib
Foundations: Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.Category CategoryTheory.HasShift CategoryTheory.HasShift CategoryTheory.HasShift CategoryTheory.Functor.CommShift CategoryTheory.Functor.CommShift CategoryTheory.Limits.HasZeroObject CategoryTheory.Limits.HasZeroObject CategoryTheory.Limits.HasZeroObject CategoryTheory.Preadditive CategoryTheory.Preadditive CategoryTheory.Preadditive CategoryTheory.Functor.Additive CategoryTheory.Functor.Additive CategoryTheory.Functor.Additive CategoryTheory.Pretriangulated CategoryTheory.Pretriangulated CategoryTheory.Pretriangulated CategoryTheory.Functor.IsTriangulated CategoryTheory.Functor.IsTriangulated CategoryTheory.Functor.EssSurj

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functor.objproof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Functor.compstatement and proof · cited by 6,529
CategoryTheory.Isoproof · cited by 3,963
CategoryTheory.Preadditivestatement and proof · cited by 3,309
CategoryTheory.shiftFunctorstatement and proof · cited by 1,553
CategoryTheory.HasShiftstatement and proof · cited by 1,527
CategoryTheory.Limits.HasZeroObjectstatement and proof · cited by 1,298
CategoryTheory.Functor.Additivestatement and proof · cited by 1,179
CategoryTheory.Iso.symmproof · cited by 993
CategoryTheory.Arrowstatement · cited by 713

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Functor.isTriangulated_of_precomp_isoproof · cited by 0