Theorems · Definition · category theory

CategoryTheory.Abelian.Preradical.shortComplexObj

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian.Preradical C → C → CategoryTheory.ShortComplex C

For X : C, the short complex Φ.r.obj X ⟶ X ⟶ Φ.quotient.obj X obtained by evaluating Φ.shortComplex at X.

Defined in

Mathlib.CategoryTheory.Abelian.Preradical.Colon

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian