Commit 2025-12-11 08:08 034d7b7c

View on Github →

feat(Algebra/Homology): more API for the HomComplex from a single cochain complex (#32461)

Estimated changes

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

modified theorem CochainComplex.HomComplex.Cocycle.ext

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

added theorem CochainComplex.HomComplex.mem_coboundaries_iff

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

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_add

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_neg

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_sub

added theorem CochainComplex.HomComplex.Cochain.fromSingleMk_surjective

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_add

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_neg

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_sub

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective

added theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_zero