Product of derivability structures

In this file, we show that the external product of two left/right derivability structures is also a derivability structure (at least when we assume that the properties of morphisms that are involved contain identities).

The behavior of derivability structures with respect to products of categories was not studied in the paper [KM08]: it was remarked in 2023 by the author of this file (see also §5.3.4 in Formalization of derived categories). This observation was a significant motivation for the formalization of derivability structures (see the files Mathlib/Algebra/Homology/DerivedCategory/DerivabilityStructureInjectives.lean and Mathlib/AlgebraicTopology/ModelCategory/DerivabilityStructureCofibrant.lean for two examples, in homological algebra and in homotopical algebra), because it allows not only to derive functors "in one variable" but also to derive functors in several variables (e.g. the tensor product as a bifunctor).

References

• Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité
• Joël Riou, Formalization of derived categories in {Lean}/mathlib

instance CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureProdProdProd {C₁ : Type u_1} {D₁ : Type u_2} {C₂ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C₁] [Category.{v_2, u_3} C₂] [Category.{v_3, u_2} D₁] [Category.{v_4, u_4} D₂] {W₁ : MorphismProperty C₁} {W₁' : MorphismProperty D₁} {W₂ : MorphismProperty C₂} {W₂' : MorphismProperty D₂} (Φ₁ : LocalizerMorphism W₁ W₁') (Φ₂ : LocalizerMorphism W₂ W₂') [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₁'.ContainsIdentities] [W₂'.ContainsIdentities] [Φ₁.IsRightDerivabilityStructure] [Φ₂.IsRightDerivabilityStructure] : (Φ₁.prod Φ₂).IsRightDerivabilityStructure

instance CategoryTheory.LocalizerMorphism.instIsLeftDerivabilityStructureProdProdProd {C₁ : Type u_1} {D₁ : Type u_2} {C₂ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C₁] [Category.{v_2, u_3} C₂] [Category.{v_3, u_2} D₁] [Category.{v_4, u_4} D₂] {W₁ : MorphismProperty C₁} {W₁' : MorphismProperty D₁} {W₂ : MorphismProperty C₂} {W₂' : MorphismProperty D₂} (Φ₁ : LocalizerMorphism W₁ W₁') (Φ₂ : LocalizerMorphism W₂ W₂') [W₁.ContainsIdentities] [W₂.ContainsIdentities] [W₁'.ContainsIdentities] [W₂'.ContainsIdentities] [Φ₁.IsLeftDerivabilityStructure] [Φ₂.IsLeftDerivabilityStructure] : (Φ₁.prod Φ₂).IsLeftDerivabilityStructure