Commit 2024-06-25 06:39 c9d0d58e

feat(CategoryTheory): constructor for right derivability structures (#12676) In this file, we provide a constructor for right derivability structures. Assume that W₁ and W₂ are classes of morphisms in categories C₁ and C₂, and that we have a localizer morphism Φ : LocalizerMorphism W₁ W₂ that is a localized equivalence, i.e. Φ.functor induces an equivalence of categories between the localized categories. Assume moreover that W₁ is multiplicative and W₂ contains identities. Then, Φ is a right derivability structure (LocalizerMorphism.IsRightDerivabilityStructure.mk') if it satisfies the two following conditions:

• for any X₂ : C₂, the category Φ.RightResolution X₂ of resolutions of X₂ is connected
• any arrow in C₂ admits a resolution (i.e. Φ.arrow.HasRightResolutions holds, where Φ.arrow is the induced localizer morphism on categories of arrows in C₁ and C₂) This is essentially Lemme 6.5 in Structures de dérivabilité, Adv. Math. 218 (4), pp. 1286-1318 (2008) by Bruno Kahn and Georges Maltsiniotis. The "injective", "projective" and "flat" derivability structures on categories of cochain complexes shall be obtained using this constructor.