Theorems · Inductive type · category theory

CategoryTheory.Pretriangulated.Triangle

(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasShift C ℤ] → Type (max u v)

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C.

Defined in

Mathlib.CategoryTheory.Triangulated.Basic

Cited by

645 results in Mathlib

Foundations

Depth 31 from the axioms, rests on 248 definitions · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift