Commit 2026-05-06 01:11 0f9072dd

View on Github →

feat(Algebra/Homology): quasi-isomorphisms between chain complexes of projective objects are homotopy equivalences (#38958) The dual result for cochain complexes of injective objects (indexed by ℕ) is also obtained. This follows from previously obtained results about K-projective and K-injective objects.

Estimated changes

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

added theorem DerivedCategory.quotientCompQhIso_hom_naturality

added theorem DerivedCategory.quotientCompQhIso_inv_naturality

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

modified theorem CochainComplex.IsKInjective.Qh_map_bijective

added theorem CochainComplex.IsKInjective.quasiIso_iff

added theorem CochainComplex.quasiIso_iff_of_injective

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

added theorem ChainComplex.quasiIso_iff_of_projective

modified theorem CochainComplex.IsKProjective.Qh_map_bijective

added theorem CochainComplex.IsKProjective.quasiIso_iff

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

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

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

added theorem HomologicalComplex.homotopyEquivalences_extendMap_iff

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

added theorem HomotopyCategory.inverseImage_quotient_isomorphisms

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

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