Commit 2024-02-08 14:48 a2a2298f

View on Github →

feat(Algebra/Homology/HomotopyCategory): definition of the distinguished triangles (#9614) This PR defines the triangles which shall be the distinguished triangles for the (pre)triangulated structure on the homotopy category of cochain complexes in an additive category.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

added theorem CochainComplex.mappingCone.inl_v_triangle_mor₃_f

added theorem CochainComplex.mappingCone.inr_f_triangle_mor₃_f

added theorem CochainComplex.mappingCone.inr_triangleδ

added theorem CochainComplex.mappingCone.map_comp

added theorem CochainComplex.mappingCone.map_eq_mapOfHomotopy

added theorem CochainComplex.mappingCone.map_id

added theorem CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂

added theorem CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃