Commit 2025-01-16 22:07 e6c7f463

View on Github →

feat(Algebra/Homology/Embedding): the morphism from a complex to its truncGE truncation (#19544) Given an embedding e of complex shapes which satisfies e.IsTruncGE, we define the canonical (natural) epimorphism K.πTruncGE e : K ⟶ K.truncGE e from a complex to its canonical truncation.

Estimated changes

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

added theorem ComplexShape.Embedding.homRestrict_comp_extendMap

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

added theorem HomologicalComplex.isIso_restrictionToTruncGE'

added theorem HomologicalComplex.restrictionToTruncGE'.comm

added theorem HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv

added theorem HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv

added theorem HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv

added theorem HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv

added theorem HomologicalComplex.restrictionToTruncGE'_hasLift

added theorem HomologicalComplex.restrictionToTruncGE'_naturality

added theorem HomologicalComplex.πTruncGE_naturality

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

added theorem CategoryTheory.Limits.IsZero.epi

added theorem CategoryTheory.Limits.IsZero.mono