Commit 2024-01-09 09:25 c64c9a87

View on Github →

feat(Algebra/Homology): morphisms from the mapping cone (#9509) This PR studies morphisms from the mapping cone.

Estimated changes

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

added theorem CochainComplex.HomComplex.Cochain.comp_units_smul

added theorem CochainComplex.HomComplex.Cochain.units_smul_comp

added theorem CochainComplex.HomComplex.δ_units_smul

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

added theorem CochainComplex.mappingCone.d_fst_v'

added theorem CochainComplex.mappingCone.d_fst_v

added theorem CochainComplex.mappingCone.d_snd_v'

added theorem CochainComplex.mappingCone.d_snd_v

added theorem CochainComplex.mappingCone.desc_f

added theorem CochainComplex.mappingCone.ext_cochain_from_iff

added theorem CochainComplex.mappingCone.ext_cochain_to_iff

added theorem CochainComplex.mappingCone.id

added theorem CochainComplex.mappingCone.id_X

added theorem CochainComplex.mappingCone.inl_desc

added theorem CochainComplex.mappingCone.inl_descCochain

added theorem CochainComplex.mappingCone.inl_v_d

added theorem CochainComplex.mappingCone.inl_v_descCochain_v

added theorem CochainComplex.mappingCone.inl_v_desc_f

added theorem CochainComplex.mappingCone.inr_desc

added theorem CochainComplex.mappingCone.inr_descCochain

added theorem CochainComplex.mappingCone.inr_f_d

added theorem CochainComplex.mappingCone.inr_f_descCochain_v

added theorem CochainComplex.mappingCone.inr_f_desc_f

added theorem CochainComplex.mappingCone.ofHom_desc

added theorem CochainComplex.mappingCone.δ_descCochain

added theorem CochainComplex.mappingCone.δ_inl

added theorem CochainComplex.mappingCone.δ_snd