Commit 2025-12-03 19:32 230c619d

View on Github →

feat(Algebra/Homology): morphisms to K-injective complexes in the derived category (#31900) We compute the type of morphisms to K-injective complexes in the derived category. (Some definitions about acyclic complexes are also moved from DerivedCategory.Basic to a new file HomotopyCategory.Acyclic.)

Estimated changes

Modified Mathlib.lean

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

deleted theorem HomotopyCategory.mem_subcategoryAcyclic_iff

deleted theorem HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W

deleted theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt

deleted def HomotopyCategory.subcategoryAcyclic

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

added theorem CochainComplex.IsKInjective.Qh_map_bijective

Created Mathlib/Algebra/Homology/HomotopyCategory/Acyclic.lean

added theorem HomotopyCategory.mem_subcategoryAcyclic_iff

added theorem HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W

added theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic

added theorem HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt

added def HomotopyCategory.subcategoryAcyclic

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

added theorem CochainComplex.IsKInjective.rightOrthogonal

added theorem CochainComplex.isKInjective_iff_of_iso

added theorem CochainComplex.isKInjective_iff_rightOrthogonal

added theorem CochainComplex.isKInjective_of_iso

added theorem CochainComplex.isKInjective_shift_iff

added theorem HomotopyEquiv.isKInjective