Commit 2023-11-28 14:52 547a8415

View on Github →

refactor: use the new homology API for right derived functors (#8593) Injective resolutions and right derived functors are redefined using the new homology API.

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

added def CategoryTheory.Functor.mapHomotopyCategoryFactors

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

added theorem CategoryTheory.ShortComplex.Exact.comp_descToInjective

added theorem CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_kernel

added theorem CategoryTheory.ShortComplex.exact_and_epi_g_iff_of_iso

added theorem CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel

added theorem CategoryTheory.ShortComplex.exact_and_mono_f_iff_of_iso

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

added theorem CochainComplex.isIso_liftCycles_iff

Modified Mathlib/Algebra/Homology/SingleHomology.lean

added theorem CochainComplex.exactAt_succ_single_obj

Modified Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean

added theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne

added theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc

added theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero

deleted theorem CategoryTheory.InjectiveResolution.exact_ofCocomplex

added theorem CategoryTheory.InjectiveResolution.exact₀

added def CategoryTheory.InjectiveResolution.iso

added theorem CategoryTheory.InjectiveResolution.iso_hom_naturality

added theorem CategoryTheory.InjectiveResolution.iso_inv_naturality

modified def CategoryTheory.InjectiveResolution.ofCocomplex

added theorem CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1

added theorem CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ

deleted theorem CategoryTheory.InjectiveResolution.ofCocomplex_sq_01_comm

modified theorem CategoryTheory.exact_f_d

deleted def HomologicalComplex.Hom.HomologicalComplex.Hom.fromSingle₀InjectiveResolution

Modified Mathlib/CategoryTheory/Abelian/RightDerived.lean

deleted theorem CategoryTheory.Abelian.Functor.exact_of_map_injectiveResolution

deleted theorem CategoryTheory.Abelian.Functor.preserves_exact_of_preservesFiniteLimits_of_mono

deleted def CategoryTheory.Abelian.Functor.rightDerivedZeroIsoSelf

deleted def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp

deleted def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv

deleted theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv_comp

deleted def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppIso

deleted theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp_comp_inv

deleted theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelf_natural

added theorem CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ

deleted def CategoryTheory.Functor.rightDerived

deleted def CategoryTheory.Functor.rightDerivedObjInjectiveSucc

deleted def CategoryTheory.Functor.rightDerivedObjInjectiveZero

deleted def CategoryTheory.Functor.rightDerivedObjIso

added theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id

added theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app

added theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id

added theorem CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app

modified theorem CategoryTheory.Functor.rightDerived_map_eq

added theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality

added theorem CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality

added theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality

added theorem CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality

added theorem CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq

added theorem CategoryTheory.InjectiveResolution.rightDerived_app_eq

added theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles

added theorem CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality

added theorem CategoryTheory.InjectiveResolution.toRightDerivedZero_eq

deleted def CategoryTheory.NatTrans.rightDerived

added theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp

added theorem CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id

deleted theorem CategoryTheory.NatTrans.rightDerived_eq

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

added theorem CategoryTheory.Functor.map_isZero

Modified Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

added theorem CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ

modified theorem CategoryTheory.InjectiveResolution.complex_d_comp

added theorem CategoryTheory.InjectiveResolution.exact_succ

added def CategoryTheory.InjectiveResolution.isLimitKernelFork

added def CategoryTheory.InjectiveResolution.kernelFork

modified def CategoryTheory.InjectiveResolution.self

modified theorem CategoryTheory.InjectiveResolution.ι_f_succ

modified theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d