Commit 2023-08-22 00:30 dd15b866

View on Github →

feat: cochains of morphisms between cochain complexes (#6701) This PR starts the construction of the cochain complex of morphisms from a cochain complex to another.

Estimated changes

Modified Mathlib.lean

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

added theorem CochainComplex.HomComplex.Cochain.add_v

added def CochainComplex.HomComplex.Cochain.comp

added theorem CochainComplex.HomComplex.Cochain.comp_assoc

added theorem CochainComplex.HomComplex.Cochain.comp_v

added theorem CochainComplex.HomComplex.Cochain.comp_zero_cochain_v

added theorem CochainComplex.HomComplex.Cochain.congr_v

added theorem CochainComplex.HomComplex.Cochain.d_comp_ofHom_v

added theorem CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v

added theorem CochainComplex.HomComplex.Cochain.ext

added theorem CochainComplex.HomComplex.Cochain.ext₀

added def CochainComplex.HomComplex.Cochain.mk

added theorem CochainComplex.HomComplex.Cochain.mk_v

added theorem CochainComplex.HomComplex.Cochain.neg_v

added def CochainComplex.HomComplex.Cochain.ofHom

added theorem CochainComplex.HomComplex.Cochain.ofHom_add

added theorem CochainComplex.HomComplex.Cochain.ofHom_neg

added theorem CochainComplex.HomComplex.Cochain.ofHom_sub

added theorem CochainComplex.HomComplex.Cochain.ofHom_v

added theorem CochainComplex.HomComplex.Cochain.ofHom_v_comp_d

added theorem CochainComplex.HomComplex.Cochain.ofHom_zero

added def CochainComplex.HomComplex.Cochain.ofHomotopy

added theorem CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq

added theorem CochainComplex.HomComplex.Cochain.ofHomotopy_refl

added def CochainComplex.HomComplex.Cochain.ofHoms

added theorem CochainComplex.HomComplex.Cochain.ofHoms_v

added theorem CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d

added theorem CochainComplex.HomComplex.Cochain.ofHoms_zero

added theorem CochainComplex.HomComplex.Cochain.sub_v

added def CochainComplex.HomComplex.Cochain.v

added theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom

added theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv

added theorem CochainComplex.HomComplex.Cochain.zero_cochain_comp_v

added theorem CochainComplex.HomComplex.Cochain.zero_v

added theorem CochainComplex.HomComplex.Cochain.zsmul_v

added def CochainComplex.HomComplex.Cochain

added structure CochainComplex.HomComplex.Triplet