Commit 2025-11-08 15:24 d731ea48

View on Github →

feat(CategoryTheory): existence of right derived functors using derivability structures (#26374) In this PR, we formalize an existence theorem for right derived functors which appeared in the article Structures de dérivabilité by Bruno Kahn and Georges Maltsiniotis, Adv. Math. 218 (2008).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Iso.lean

added theorem CategoryTheory.isIso_comp_left_iff

added theorem CategoryTheory.isIso_comp_right_iff

Modified Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean

deleted theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure'

deleted theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isLeftDerivabilityStructure

deleted theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure'

deleted theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure

Created Mathlib/CategoryTheory/Localization/DerivabilityStructure/PointwiseRightDerived.lean

added theorem CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure

added theorem CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure

added theorem CategoryTheory.LocalizerMorphism.isIso_α_iff_of_isRightDerivabilityStructure

added theorem CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac

added theorem CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app