Resolutions for a morphism of localizers

Given a morphism of localizers Φ : LocalizerMorphism W₁ W₂ (i.e. W₁ and W₂ are morphism properties on categories C₁ and C₂, and we have a functor Φ.functor : C₁ ⥤ C₂ which sends morphisms in W₁ to morphisms in W₂), we introduce the notion of right resolutions of objects in C₂: if X₂ : C₂. A right resolution consists of an object X₁ : C₁ and a morphism w : X₂ ⟶ Φ.functor.obj X₁ that is in W₂. Then, the typeclass Φ.HasRightResolutions holds when any X₂ : C₂ has a right resolution.

The type of right resolutions Φ.RightResolution X₂ is endowed with a category structure when the morphism property W₁ is multiplicative.

Future works

• formalize right derivability structures as localizer morphisms admitting right resolutions and forming a Guitart exact square, as it is defined in [the paper by Kahn and Maltsiniotis][KahnMaltsiniotis2008] (TODO @joelriou)
• show that if C is an abelian category with enough injectives, there is a derivability structure associated to the inclusion of the full subcategory of complexes of injective objects into the bounded below homotopy category of C (TODO @joelriou)
• formalize dual results

References

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

structure CategoryTheory.LocalizerMorphism.RightResolution {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂) : Type (max u_1 u_6)

The category of resolutions of an object in the target category of a localizer morphism.

• X₁ : C₁

  an object in the source category

• w : X₂ ⟶ Φ.functor.obj self.X₁

  a morphism to an object of the form Φ.functor.obj X₁

• hw : W₂ self.w

theorem CategoryTheory.LocalizerMorphism.RightResolution.mk_surjective {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) : ∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w), R = CategoryTheory.LocalizerMorphism.RightResolution.mk w hw

@[inline, reducible]

abbrev CategoryTheory.LocalizerMorphism.HasRightResolutions {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) : Prop

A localizer morphism has right resolutions when any object has a right resolution.

Equations

• CategoryTheory.LocalizerMorphism.HasRightResolutions Φ = ∀ (X₂ : C₂), Nonempty (CategoryTheory.LocalizerMorphism.RightResolution Φ X₂)

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (x y : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R'), x = y ↔ x.f = y.f

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext {C₁ : Type u_1} {C₂ : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (x y : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R'), x.f = y.f → x = y

structure CategoryTheory.LocalizerMorphism.RightResolution.Hom {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} (R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) (R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) : Type u_5

The type of morphisms in the category Φ.RightResolution X₂ (when W₁ is multiplicative).

• f : R.X₁ ⟶ R'.X₁

  a morphism in the source category

• hf : W₁ self.f
• comm : CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (self : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R') {Z : C₂} (h : Φ.functor.obj R'.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp R.w (CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) h) = CategoryTheory.CategoryStruct.comp R'.w h

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.id_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.ContainsIdentities W₁] (R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) : (CategoryTheory.LocalizerMorphism.RightResolution.Hom.id R).f = CategoryTheory.CategoryStruct.id R.X₁

def CategoryTheory.LocalizerMorphism.RightResolution.Hom.id {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.ContainsIdentities W₁] (R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R

The identity of a object in Φ.RightResolution X₂.

Equations

• CategoryTheory.LocalizerMorphism.RightResolution.Hom.id R = { f := CategoryTheory.CategoryStruct.id R.X₁, hf := ⋯, comm := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R'' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (φ : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R') (ψ : CategoryTheory.LocalizerMorphism.RightResolution.Hom R' R'') : (CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f

def CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R'' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (φ : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R') (ψ : CategoryTheory.LocalizerMorphism.RightResolution.Hom R' R'') : CategoryTheory.LocalizerMorphism.RightResolution.Hom R R''

The composition of morphisms in Φ.RightResolution X₂.

Equations

• CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp φ ψ = { f := CategoryTheory.CategoryStruct.comp φ.f ψ.f, hf := ⋯, comm := ⋯ }

instance CategoryTheory.LocalizerMorphism.RightResolution.instCategoryRightResolution {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] : CategoryTheory.Category.{u_5, max u_1 u_6} (CategoryTheory.LocalizerMorphism.RightResolution Φ X₂)

Equations

• CategoryTheory.LocalizerMorphism.RightResolution.instCategoryRightResolution = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.id_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] (R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂) : (CategoryTheory.CategoryStruct.id R).f = CategoryTheory.CategoryStruct.id R.X₁

theorem CategoryTheory.LocalizerMorphism.RightResolution.comp_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R'' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (φ : R ⟶ R') (ψ : R' ⟶ R'') {Z : C₁} (h : R''.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ ψ).f h = CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp ψ.f h)

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.comp_f {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R'' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} (φ : R ⟶ R') (ψ : R' ⟶ R'') : (CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f

theorem CategoryTheory.LocalizerMorphism.RightResolution.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [CategoryTheory.MorphismProperty.IsMultiplicative W₁] {R : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {R' : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂} {φ₁ : R ⟶ R'} {φ₂ : R ⟶ R'} (h : φ₁.f = φ₂.f) : φ₁ = φ₂

theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [CategoryTheory.LocalizerMorphism.HasRightResolutions Φ] (L₂ : CategoryTheory.Functor C₂ D₂) [CategoryTheory.Functor.IsLocalization L₂ W₂] : CategoryTheory.Functor.EssSurj (CategoryTheory.Functor.comp Φ.functor L₂)

theorem CategoryTheory.LocalizerMorphism.isIso_iff_of_hasRightResolutions {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_3} {H : Type u_4} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_5, u_3} D₂] [CategoryTheory.Category.{u_6, u_4} H] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [CategoryTheory.LocalizerMorphism.HasRightResolutions Φ] (L₂ : CategoryTheory.Functor C₂ D₂) [CategoryTheory.Functor.IsLocalization L₂ W₂] {F : CategoryTheory.Functor D₂ H} {G : CategoryTheory.Functor D₂ H} (α : F ⟶ G) : CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))