Commit 2021-03-10 11:57 eaa02185View on Github →
feat(category_theory/triangulated/basic): add definitions of additive category and triangle (#6539) This PR adds the definition of an additive category and the definition of a triangle in an additive category with an additive shift.
added structure category_theory.triangulated.triangle
added theorem category_theory.triangulated.triangle_morphism.comp_id
added theorem category_theory.triangulated.triangle_morphism.id_comp
added structure category_theory.triangulated.triangle_morphism