Commit 2023-09-19 07:20 44ec4f1b

View on Github →

feat: the type of cocycles in the complex of morphisms between cochain complexes (#7201)

Estimated changes

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

added theorem CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe

added theorem CochainComplex.HomComplex.Cocycle.coe_add

added theorem CochainComplex.HomComplex.Cocycle.coe_neg

added theorem CochainComplex.HomComplex.Cocycle.coe_sub

added theorem CochainComplex.HomComplex.Cocycle.coe_zero

added theorem CochainComplex.HomComplex.Cocycle.coe_zsmul

added def CochainComplex.HomComplex.Cocycle.diff

added def CochainComplex.HomComplex.Cocycle.equivHom

added theorem CochainComplex.HomComplex.Cocycle.ext

added theorem CochainComplex.HomComplex.Cocycle.ext_iff

added def CochainComplex.HomComplex.Cocycle.homOf

added theorem CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self

added theorem CochainComplex.HomComplex.Cocycle.mem_iff

added def CochainComplex.HomComplex.Cocycle.mk

added def CochainComplex.HomComplex.Cocycle.ofHom

added theorem CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self

added theorem CochainComplex.HomComplex.Cocycle.δ_eq_zero

added def CochainComplex.HomComplex.Cocycle

added def CochainComplex.HomComplex.cocycle