Commit 2024-06-08 04:33 68203c8e

View on Github →

feat(CategoryTheory): right derivability structures (#12633) In this PR, we define the notion of right derivability structures introduced by Bruno Kahn and Georges Maltsiniotis (Structures de dérivabilité, Adv. Math. 218 (4), pp. 1286-1318 (2008)). It shall be used in order to construct and study derived functors.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/CatCommSq.lean

added def CategoryTheory.CatCommSq.vInv

added def CategoryTheory.CatCommSq.vInvEquiv

added theorem CategoryTheory.CatCommSq.vInv_vInv

Modified Mathlib/CategoryTheory/GuitartExact/Basic.lean

Modified Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean

added theorem CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences

added theorem CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences

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

added theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure'

added theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure

added theorem CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff