Functorial resolutions give derivability structures

In this file, we provide a constructor for right derivability structures. We assume that Φ : LocalizerMorphism W₁ W₂ is given by a fully faithful functor Φ.functor : C₁ ⥤ C₂ and that we have a resolution functor ρ : C₂ ⥤ C₁ with a natural transformation i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor such that W₂ (i.app X₂) for any X₂ : C₂. If we assume that W₁ is induced by W₂, that W₂ is multiplicative and has the two out of three property, then Φ is a right derivability structure.

theorem CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_functorial_resolutions {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {ρ : Functor C₂ C₁} (i : Functor.id C₂ ⟶ ρ.comp Φ.functor) (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) : Φ.arrow.HasRightResolutions

def CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {ρ : Functor C₂ C₁} {i : Functor.id C₂ ⟶ ρ.comp Φ.functor} (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [W₂.HasTwoOutOfThreeProperty] : LocalizerMorphism W₂ W₁

If Φ : LocalizerMorphism W₁ W₂ corresponds to a class W₁ that is the inverse image of W₂ by the functor Φ.functor and that we have functorial right resolutions, then this is a morphism of localizers in the other direction.

Equations

• CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv hi hW₁ = { functor := ρ, map := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv_functor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {ρ : Functor C₂ C₁} {i : Functor.id C₂ ⟶ ρ.comp Φ.functor} (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [W₂.HasTwoOutOfThreeProperty] : (localizerMorphismInv hi hW₁).functor = ρ

noncomputable def CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {ρ : Functor C₂ C₁} (i : Functor.id C₂ ⟶ ρ.comp Φ.functor) [Φ.functor.Full] [Φ.functor.Faithful] : Functor.id C₁ ⟶ Φ.functor.comp ρ

If Φ : LocalizerMorphism W₁ W₂ corresponds to a class W₁ that is induced by W₂ via the fully faithful functor Φ.functor and we have functorial right resolutions given by a functor ρ : C₂ ⥤ C₁, then this is the natural transformation 𝟭 C₁ ⟶ Φ.functor ⋙ ρ induced by i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor.

Equations

• CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι i = ((CategoryTheory.Functor.whiskeringRight C₁ C₁ C₂).obj Φ.functor).preimage (Φ.functor.whiskerLeft i)

@[simp]

theorem CategoryTheory.LocalizerMorphism.functorialRightResolutions.Φ_functor_map_ι_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_4, u_1} C₁] [Category.{u_3, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {ρ : Functor C₂ C₁} {i : Functor.id C₂ ⟶ ρ.comp Φ.functor} [Φ.functor.Full] [Φ.functor.Faithful] (X₁ : C₁) : Φ.functor.map ((ι i).app X₁) = i.app (Φ.functor.obj X₁)

theorem CategoryTheory.LocalizerMorphism.functorialRightResolutions.W₁_ι_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {ρ : Functor C₂ C₁} {i : Functor.id C₂ ⟶ ρ.comp Φ.functor} (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [Φ.functor.Full] [Φ.functor.Faithful] (X₁ : C₁) : W₁ ((ι i).app X₁)

theorem CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_functorial_right_resolutions {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {ρ : Functor C₂ C₁} (i : Functor.id C₂ ⟶ ρ.comp Φ.functor) (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty] : Φ.IsLocalizedEquivalence

theorem CategoryTheory.LocalizerMorphism.isConnected_rightResolution_of_functorial_resolutions {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {ρ : Functor C₂ C₁} (i : Functor.id C₂ ⟶ ρ.comp Φ.functor) (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty] [W₂.IsMultiplicative] (X₂ : C₂) : IsConnected (Φ.RightResolution X₂)

theorem CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_functorial_resolutions {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_3, u_1} C₁] [Category.{u_4, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) {ρ : Functor C₂ C₁} (i : Functor.id C₂ ⟶ ρ.comp Φ.functor) (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty] [W₂.IsMultiplicative] : Φ.IsRightDerivabilityStructure