Commit 2024-01-09 20:08 487e1983

View on Github →

feat(Algebra/Homology): the mapping cone (#8951) This PR completes the basic API for the mapping cone which shall be used in order to show that the homotopy category of cochain complexes is a triangulated category.

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

added theorem CochainComplex.mappingCone.liftCochain_descCochain

added theorem CochainComplex.mappingCone.liftCochain_fst

added theorem CochainComplex.mappingCone.liftCochain_snd

added theorem CochainComplex.mappingCone.liftCochain_v_descCochain_v

added theorem CochainComplex.mappingCone.liftCochain_v_fst_v

added theorem CochainComplex.mappingCone.liftCochain_v_snd_v

added theorem CochainComplex.mappingCone.lift_desc_f

added theorem CochainComplex.mappingCone.lift_f

added theorem CochainComplex.mappingCone.lift_f_fst_v

added theorem CochainComplex.mappingCone.lift_f_snd_v

added theorem CochainComplex.mappingCone.lift_fst

added theorem CochainComplex.mappingCone.lift_snd

added theorem CochainComplex.mappingCone.ofHom_lift

added theorem CochainComplex.mappingCone.δ_liftCochain

Modified Mathlib/Algebra/Homology/HomotopyCofiber.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

added theorem CategoryTheory.Limits.biprod_isZero_iff