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.

Similar definitions are done from left resolutions.

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} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) : Type (max u_1 u_6)

The category of right 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

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

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

• X₁ : C₁

  an object in the source category

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

  a morphism from 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} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (R : Φ.RightResolution X₂) : ∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w), R = { X₁ := X₁, w := w, hw := hw }

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• Φ.HasLeftResolutions = ∀ (X₂ : C₂), Nonempty (Φ.LeftResolution X₂)

structure CategoryTheory.LocalizerMorphism.RightResolution.Hom {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (R R' : Φ.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 : CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w

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

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

@[simp]

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

def CategoryTheory.LocalizerMorphism.RightResolution.Hom.id {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.ContainsIdentities] (R : Φ.RightResolution X₂) : R.Hom 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.id_f {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.ContainsIdentities] (R : Φ.RightResolution X₂) : (id R).f = CategoryStruct.id R.X₁

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

The composition of morphisms in Φ.RightResolution X₂.

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

  a morphism in the source category

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

theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext {C₁ : Type u_1} {C₂ : Type u_2} {inst✝ : Category.{u_5, u_1} C₁} {inst✝¹ : Category.{u_6, u_2} C₂} {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'} (f : x.f = y.f) : x = y

theorem CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} {inst✝ : Category.{u_5, u_1} C₁} {inst✝¹ : Category.{u_6, u_2} C₂} {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} {L L' : Φ.LeftResolution X₂} {x y : L.Hom L'} : x = y ↔ x.f = y.f

@[simp]

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

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

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

Equations

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

@[simp]

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

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

The composition of morphisms in Φ.LeftResolution X₂.

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.LocalizerMorphism.LeftResolution.hom_ext_iff {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} [W₁.IsMultiplicative] {L L' : Φ.LeftResolution X₂} {φ₁ φ₂ : L ⟶ L'} : φ₁ = φ₂ ↔ φ₁.f = φ₂.f

def CategoryTheory.LocalizerMorphism.LeftResolution.op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) : Φ.op.RightResolution (Opposite.op X₂)

The canonical map Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂).

Equations

• L.op = { X₁ := Opposite.op L.X₁, w := L.w.op, hw := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.op_w {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) : L.op.w = L.w.op

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.LeftResolution X₂) : L.op.X₁ = Opposite.op L.X₁

def CategoryTheory.LocalizerMorphism.LeftResolution.unop {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) : Φ.RightResolution (Opposite.unop X₂)

The canonical map Φ.op.LeftResolution X₂ → Φ.RightResolution X₂.

Equations

• L.unop = { X₁ := Opposite.unop L.X₁, w := L.w.unop, hw := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) : L.unop.X₁ = Opposite.unop L.X₁

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.unop_w {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.LeftResolution X₂) : L.unop.w = L.w.unop

def CategoryTheory.LocalizerMorphism.RightResolution.op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) : Φ.op.LeftResolution (Opposite.op X₂)

The canonical map Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂).

Equations

• L.op = { X₁ := Opposite.op L.X₁, w := L.w.op, hw := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.op_w {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) : L.op.w = L.w.op

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.op_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂} (L : Φ.RightResolution X₂) : L.op.X₁ = Opposite.op L.X₁

def CategoryTheory.LocalizerMorphism.RightResolution.unop {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) : Φ.LeftResolution (Opposite.unop X₂)

The canonical map Φ.op.RightResolution X₂ → Φ.LeftResolution X₂.

Equations

• L.unop = { X₁ := Opposite.unop L.X₁, w := L.w.unop, hw := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.unop_w {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) : L.unop.w = L.w.unop

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁ {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {Φ : LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ} (L : Φ.op.RightResolution X₂) : L.unop.X₁ = Opposite.unop L.X₁

theorem CategoryTheory.LocalizerMorphism.nonempty_leftResolution_iff_op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_5, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) : Nonempty (Φ.LeftResolution X₂) ↔ Nonempty (Φ.op.RightResolution (Opposite.op X₂))

theorem CategoryTheory.LocalizerMorphism.nonempty_rightResolution_iff_op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_6, u_1} C₁] [Category.{u_5, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) : Nonempty (Φ.RightResolution X₂) ↔ Nonempty (Φ.op.LeftResolution (Opposite.op X₂))

theorem CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) : Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions

theorem CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) : Φ.HasRightResolutions ↔ Φ.op.HasLeftResolutions

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

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

def CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : Functor (Φ.LeftResolution X₂)ᵒᵖ (Φ.op.RightResolution (Opposite.op X₂))

The functor (Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂).

Equations

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

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_obj {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] (L : (Φ.LeftResolution X₂)ᵒᵖ) : (opFunctor Φ X₂).obj L = (Opposite.unop L).op

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] {X✝ Y✝ : (Φ.LeftResolution X₂)ᵒᵖ} (φ : X✝ ⟶ Y✝) : ((opFunctor Φ X₂).map φ).f = φ.unop.f.op

def CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] : Functor (Φ.op.RightResolution X₂)ᵒᵖ (Φ.LeftResolution (Opposite.unop X₂))

The functor (Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop.

Equations

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

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_f {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] {X✝ Y✝ : (Φ.op.RightResolution X₂)ᵒᵖ} (φ : X✝ ⟶ Y✝) : ((unopFunctor Φ X₂).map φ).f = φ.unop.f.unop

@[simp]

theorem CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_obj {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂ᵒᵖ) [W₁.IsMultiplicative] (R : (Φ.op.RightResolution X₂)ᵒᵖ) : (unopFunctor Φ X₂).obj R = (Opposite.unop R).unop

def CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂)

The equivalence of categories (Φ.LeftResolution X₂)ᵒᵖ ≌ Φ.op.RightResolution (Opposite.op X₂).

Equations

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

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : (opEquivalence Φ X₂).counitIso = Iso.refl ((RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp.comp (opFunctor Φ X₂))

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : (opEquivalence Φ X₂).inverse = (RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : (opEquivalence Φ X₂).functor = opFunctor Φ X₂

@[simp]

theorem CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso {C₁ : Type u_1} {C₂ : Type u_2} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (X₂ : C₂) [W₁.IsMultiplicative] : (opEquivalence Φ X₂).unitIso = Iso.refl (Functor.id (Φ.LeftResolution X₂)ᵒᵖ)

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

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

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

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