Commit 2026-03-03 01:03 e78b025b

View on Github →

feat(Algebra/Homology): the mapping cocone (#35929) Given a morphism φ : K ⟶ L of cochain complexes, the mapping cone allows to obtain a triangle K ⟶ L ⟶ mappingCone φ ⟶ .... In this PR, we define the mapping cocone, which fits in a rotated triangle: mappingCocone φ ⟶ K ⟶ L ⟶ ....

Estimated changes

Modified Mathlib.lean

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

added theorem CochainComplex.mappingCocone.id_X

added theorem CochainComplex.mappingCocone.inl_comp_descCochain

added theorem CochainComplex.mappingCocone.inl_v_descCochain_v

added theorem CochainComplex.mappingCocone.inl_v_desc_f

added theorem CochainComplex.mappingCocone.inl_v_fst_f

added theorem CochainComplex.mappingCocone.inl_v_snd_v

added theorem CochainComplex.mappingCocone.inr_comp_descCochain

added theorem CochainComplex.mappingCocone.inr_v_descCochain_v

added theorem CochainComplex.mappingCocone.inr_v_desc_f

added theorem CochainComplex.mappingCocone.inr_v_fst_f

added theorem CochainComplex.mappingCocone.inr_v_snd_v

added theorem CochainComplex.mappingCocone.liftCochain_comp_fst

added theorem CochainComplex.mappingCocone.liftCochain_comp_snd

added theorem CochainComplex.mappingCocone.liftCochain_v_fst_f

added theorem CochainComplex.mappingCocone.liftCochain_v_snd_v

added theorem CochainComplex.mappingCocone.lift_f_fst_f

added theorem CochainComplex.mappingCocone.lift_f_snd_v

added theorem CochainComplex.mappingCocone.lift_fst

added theorem CochainComplex.mappingCocone.ofHom_desc

added theorem CochainComplex.mappingCocone.ofHom_lift

added theorem CochainComplex.mappingCocone.δ_descCochain

added theorem CochainComplex.mappingCocone.δ_liftCochain