Commit 2024-07-26 08:26 c387e3e1

View on Github →

feat(Algebra/Homology): the canonical truncation truncGE (#14734) We construct the canonical truncation truncGE of homological complexes relative to an embedding e of complex shapes which satisfies e.IsTruncGE.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Embedding/Boundary.lean

deleted theorem ComplexShape.Embedding.BoundaryGE.false

added theorem ComplexShape.Embedding.BoundaryGE.false_of_isTruncLE

deleted theorem ComplexShape.Embedding.BoundaryLE.false

added theorem ComplexShape.Embedding.BoundaryLE.false_of_isTruncGE

Created Mathlib/Algebra/Homology/Embedding/TruncGE.lean

added theorem HomologicalComplex.truncGE'.d_comp_d

added theorem HomologicalComplex.truncGE'_d_eq

added theorem HomologicalComplex.truncGE'_d_eq_fromOpcycles