Constructor for derivability structures

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 statement is essentially Lemme 6.5 in [the paper by Kahn and Maltsiniotis][KahnMaltsiniotis2008].

References

• [Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité][KahnMaltsiniotis2008]

noncomputable def CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [W₁.IsMultiplicative] {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (L : CategoryTheory.Functor C₂ D) [L.IsLocalization W₂] {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) : CategoryTheory.Functor (Φ.RightResolution X₂) ((CategoryTheory.TwoSquare.mk Φ.functor (Φ.functor.comp L) L (CategoryTheory.Functor.id D) (Φ.functor.comp L).rightUnitor.inv).CostructuredArrowDownwards y)

Given Φ : LocalizerMorphism W₁ W₂, L : C₂ ⥤ D a localization functor for W₂ and a morphism y : L.obj X₂ ⟶ X₃, this is the functor which sends R : Φ.RightResolution d to (isoOfHom L W₂ R.w R.hw).inv ≫ y in the category w.CostructuredArrowDownwards y where w is TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [W₁.IsMultiplicative] {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (L : CategoryTheory.Functor C₂ D) [L.IsLocalization W₂] {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) {R : Φ.RightResolution X₂} {R' : Φ.RightResolution X₂} (φ : R ⟶ R') : (CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.f ⋯) ⋯

@[simp]

theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [W₁.IsMultiplicative] {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (L : CategoryTheory.Functor C₂ D) [L.IsLocalization W₂] {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) (R : Φ.RightResolution X₂) : (CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).obj R = CategoryTheory.CostructuredArrow.mk (CategoryTheory.StructuredArrow.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W₂ R.w ⋯).inv y) ⋯)

theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [W₁.IsMultiplicative] [∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)] [Φ.arrow.HasRightResolutions] [W₂.ContainsIdentities] {D : Type u_3} [CategoryTheory.Category.{u_6, u_3} D] (L : CategoryTheory.Functor C₂ D) [L.IsLocalization W₂] {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) : CategoryTheory.IsConnected ((CategoryTheory.TwoSquare.mk Φ.functor (Φ.functor.comp L) L (CategoryTheory.Functor.id D) (Φ.functor.comp L).rightUnitor.inv).CostructuredArrowDownwards y)

theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk' {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_3, u_1} C₁] [CategoryTheory.Category.{u_4, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [W₁.IsMultiplicative] [∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)] [Φ.arrow.HasRightResolutions] [W₂.ContainsIdentities] [Φ.IsLocalizedEquivalence] : Φ.IsRightDerivabilityStructure

If a localizer morphism Φ is a localized equivalence, then it is a right derivability structure if the categories of right resolutions are connected and the categories of right resolutions of arrows are nonempty.