Commit 2025-01-23 05:40 ce9c3fe6

View on Github →

feat(Algebra/Homology/Embedding): canonical truncations on CochainComplex (#19578) We apply the basic Algebra.Homology.Embedding definitions to the particular case of cochain complexes indexed by the integers.

Estimated changes

Modified Mathlib.lean

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

added theorem ComplexShape.not_mem_range_embeddingUpIntGE_iff

added theorem ComplexShape.not_mem_range_embeddingUpIntLE_iff

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

added theorem CochainComplex.exactAt_of_isGE

added theorem CochainComplex.exactAt_of_isLE

added theorem CochainComplex.exists_iso_single

added theorem CochainComplex.isGE_iff

added theorem CochainComplex.isGE_of_ge

added theorem CochainComplex.isGE_of_iso

added theorem CochainComplex.isLE_iff

added theorem CochainComplex.isLE_of_iso

added theorem CochainComplex.isLE_of_le

added theorem CochainComplex.isStrictlyGE_iff

added theorem CochainComplex.isStrictlyGE_of_ge

added theorem CochainComplex.isStrictlyGE_of_iso

added theorem CochainComplex.isStrictlyLE_iff

added theorem CochainComplex.isStrictlyLE_of_iso

added theorem CochainComplex.isStrictlyLE_of_le

added theorem CochainComplex.isZero_of_isGE

added theorem CochainComplex.isZero_of_isLE

added theorem CochainComplex.isZero_of_isStrictlyGE

added theorem CochainComplex.isZero_of_isStrictlyLE

added theorem CochainComplex.ιTruncLE_naturality

added theorem CochainComplex.πTruncGE_naturality

Modified Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

added theorem HomologicalComplex.ExactAt.isZero_homology