Commit 2025-12-19 13:08 47a30a93

View on Github →

feat(Algebra/Homology): equivOfIsKInjective (#32814) We construct a bijection CohomologyClass K L n ≃ SmallShiftedHom.{w} (HomologicalComplex.quasiIso C (.up ℤ)) K L n when K and L are cochain complexes, and L is K-injective, or K is K-projective.

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean

added theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective

modified theorem CochainComplex.IsKInjective.Qh_map_bijective

Modified Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean

added theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective

modified theorem CochainComplex.IsKProjective.Qh_map_bijective

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

added theorem HomologicalComplex.isSupported_iff_of_quasiIso

Modified Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

Modified Mathlib/CategoryTheory/Abelian/Projective/Extend.lean