Commit 2025-02-24 12:08 f410b48e

View on Github →

feat(CategoryTheory): categories of homological complexes have a separator (#20229) (This also requires the introduction of a typeclass ComplexShape.HasNoLoop, which holds for the most common shapes.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/ComplexShape.lean

modified def ComplexShape.down'

modified theorem ComplexShape.down'_mk

modified def ComplexShape.down

modified theorem ComplexShape.down_mk

modified def ComplexShape.up'

modified def ComplexShape.up

Modified Mathlib/Algebra/Homology/Double.lean

Created Mathlib/Algebra/Homology/HasNoLoop.lean

added theorem ComplexShape.exists_distinct_next_or

added theorem ComplexShape.exists_distinct_prev_or

added theorem ComplexShape.hasNoLoop_down'

added theorem ComplexShape.hasNoLoop_down

added theorem ComplexShape.hasNoLoop_up'

added theorem ComplexShape.hasNoLoop_up

added theorem ComplexShape.not_rel_of_eq

added theorem ComplexShape.not_rel_self

Modified Mathlib/Algebra/Homology/Homotopy.lean

Created Mathlib/CategoryTheory/Generator/HomologicalComplex.lean

added theorem HomologicalComplex.isSeparating_separatingFamily

added theorem HomologicalComplex.isSeparator_coproduct_separatingFamily