Documentation

Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

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:

This statement is essentially Lemme 6.5 in the paper by Kahn and Maltsiniotis.

References #

@[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') :
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.
Instances For
    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.