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
Cis 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 ofC(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 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
Instances For
structure
CategoryTheory.LocalizerMorphism.LeftResolution
{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 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
Instances For
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 : Φ.RightResolution X₂)
:
∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w), R = CategoryTheory.LocalizerMorphism.RightResolution.mk w hw
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
(L : Φ.LeftResolution X₂)
:
∃ (X₁ : C₁) (w : Φ.functor.obj X₁ ⟶ X₂) (hw : W₂ w), L = CategoryTheory.LocalizerMorphism.LeftResolution.mk w hw
@[reducible, inline]
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₂)
:
A localizer morphism has right resolutions when any object has a right resolution.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.LocalizerMorphism.HasLeftResolutions
{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₂)
:
A localizer morphism has right resolutions when any object has a right resolution.
Instances For
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 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 : CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w
Instances For
theorem
CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{inst✝ : CategoryTheory.Category.{u_5, u_1} C₁}
{inst✝¹ : CategoryTheory.Category.{u_6, u_2} C₂}
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{Φ : CategoryTheory.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}
[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 R' : Φ.RightResolution X₂}
(self : R.Hom 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
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₂}
[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 := ⋯ }
Instances For
@[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₂}
[W₁.ContainsIdentities]
(R : Φ.RightResolution X₂)
:
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₂}
[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 := ⋯ }
Instances For
@[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₂}
[W₁.IsMultiplicative]
{R R' R'' : Φ.RightResolution X₂}
(φ : R.Hom R')
(ψ : R'.Hom R'')
:
(φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
instance
CategoryTheory.LocalizerMorphism.RightResolution.instCategory
{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₂}
[W₁.IsMultiplicative]
:
CategoryTheory.Category.{u_5, max u_1 u_6} (Φ.RightResolution X₂)
Equations
- CategoryTheory.LocalizerMorphism.RightResolution.instCategory = 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₂}
[W₁.IsMultiplicative]
(R : Φ.RightResolution X₂)
:
@[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₂}
[W₁.IsMultiplicative]
{R R' R'' : Φ.RightResolution X₂}
(φ : R ⟶ R')
(ψ : R' ⟶ R'')
:
(CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
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₂}
[W₁.IsMultiplicative]
{R R' R'' : Φ.RightResolution X₂}
(φ : R ⟶ R')
(ψ : R' ⟶ R'')
{Z : C₁}
(h : R''.X₁ ⟶ Z)
:
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₂}
[W₁.IsMultiplicative]
{R R' : Φ.RightResolution X₂}
{φ₁ φ₂ : R ⟶ R'}
(h : φ₁.f = φ₂.f)
:
φ₁ = φ₂
structure
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
(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 : CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) L'.w = L.w
Instances For
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{inst✝ : CategoryTheory.Category.{u_5, u_1} C₁}
{inst✝¹ : CategoryTheory.Category.{u_6, u_2} C₂}
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
{X₂ : C₂}
{L L' : Φ.LeftResolution X₂}
{x y : L.Hom L'}
(f : x.f = y.f)
:
x = y
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
{L L' : Φ.LeftResolution X₂}
(self : L.Hom L')
{Z : C₂}
(h : X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) (CategoryTheory.CategoryStruct.comp L'.w h) = CategoryTheory.CategoryStruct.comp L.w h
def
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[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 := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.ContainsIdentities]
(L : Φ.LeftResolution X₂)
:
def
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[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 := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.IsMultiplicative]
{L L' L'' : Φ.LeftResolution X₂}
(φ : L.Hom L')
(ψ : L'.Hom L'')
:
(φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
instance
CategoryTheory.LocalizerMorphism.LeftResolution.instCategory
{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₂}
[W₁.IsMultiplicative]
:
CategoryTheory.Category.{u_5, max u_1 u_6} (Φ.LeftResolution X₂)
Equations
- CategoryTheory.LocalizerMorphism.LeftResolution.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.IsMultiplicative]
(L : Φ.LeftResolution X₂)
:
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.IsMultiplicative]
{L L' L'' : Φ.LeftResolution X₂}
(φ : L ⟶ L')
(ψ : L' ⟶ L'')
:
(CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.IsMultiplicative]
{L L' L'' : Φ.LeftResolution X₂}
(φ : L ⟶ L')
(ψ : L' ⟶ L'')
{Z : C₁}
(h : L''.X₁ ⟶ Z)
:
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.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₂}
[W₁.IsMultiplicative]
{L L' : Φ.LeftResolution X₂}
{φ₁ φ₂ : L ⟶ L'}
(h : φ₁.f = φ₂.f)
:
φ₁ = φ₂
def
CategoryTheory.LocalizerMorphism.LeftResolution.op
{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₂}
(L : Φ.LeftResolution X₂)
:
Φ.op.RightResolution (Opposite.op X₂)
The canonical map Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂).
Equations
- L.op = CategoryTheory.LocalizerMorphism.RightResolution.mk L.w.op ⋯
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁
{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₂}
(L : Φ.LeftResolution X₂)
:
L.op.X₁ = Opposite.op L.X₁
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.op_w
{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₂}
(L : Φ.LeftResolution X₂)
:
L.op.w = L.w.op
def
CategoryTheory.LocalizerMorphism.LeftResolution.unop
{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₂ᵒᵖ}
(L : Φ.op.LeftResolution X₂)
:
Φ.RightResolution (Opposite.unop X₂)
The canonical map Φ.op.LeftResolution X₂ → Φ.RightResolution X₂.
Equations
- L.unop = CategoryTheory.LocalizerMorphism.RightResolution.mk L.w.unop ⋯
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.unop_w
{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₂ᵒᵖ}
(L : Φ.op.LeftResolution X₂)
:
L.unop.w = L.w.unop
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁
{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₂ᵒᵖ}
(L : Φ.op.LeftResolution X₂)
:
L.unop.X₁ = Opposite.unop L.X₁
def
CategoryTheory.LocalizerMorphism.RightResolution.op
{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₂}
(L : Φ.RightResolution X₂)
:
Φ.op.LeftResolution (Opposite.op X₂)
The canonical map Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂).
Equations
- L.op = CategoryTheory.LocalizerMorphism.LeftResolution.mk L.w.op ⋯
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.op_w
{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₂}
(L : Φ.RightResolution X₂)
:
L.op.w = L.w.op
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.op_X₁
{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₂}
(L : Φ.RightResolution X₂)
:
L.op.X₁ = Opposite.op L.X₁
def
CategoryTheory.LocalizerMorphism.RightResolution.unop
{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₂ᵒᵖ}
(L : Φ.op.RightResolution X₂)
:
Φ.LeftResolution (Opposite.unop X₂)
The canonical map Φ.op.RightResolution X₂ → Φ.LeftResolution X₂.
Equations
- L.unop = CategoryTheory.LocalizerMorphism.LeftResolution.mk L.w.unop ⋯
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.unop_X₁
{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₂ᵒᵖ}
(L : Φ.op.RightResolution X₂)
:
L.unop.X₁ = Opposite.unop L.X₁
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.unop_w
{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₂ᵒᵖ}
(L : Φ.op.RightResolution X₂)
:
L.unop.w = L.w.unop
theorem
CategoryTheory.LocalizerMorphism.nonempty_leftResolution_iff_op
{C₁ : Type u_1}
{C₂ : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_5, u_2} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.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}
[CategoryTheory.Category.{u_6, u_1} C₁]
[CategoryTheory.Category.{u_5, u_2} C₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.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}
[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₂)
:
Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions
theorem
CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op
{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₂)
:
Φ.HasRightResolutions ↔ Φ.op.HasLeftResolutions
def
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor
{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₂)
[W₁.IsMultiplicative]
:
CategoryTheory.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.
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_obj
{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₂)
[W₁.IsMultiplicative]
(L : (Φ.LeftResolution X₂)ᵒᵖ)
:
(CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).obj L = (Opposite.unop L).op
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_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₂)
[W₁.IsMultiplicative]
{X✝ Y✝ : (Φ.LeftResolution X₂)ᵒᵖ}
(φ : X✝ ⟶ Y✝)
:
((CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).map φ).f = φ.unop.f.op
def
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor
{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₂ᵒᵖ)
[W₁.IsMultiplicative]
:
CategoryTheory.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.
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_obj
{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₂ᵒᵖ)
[W₁.IsMultiplicative]
(R : (Φ.op.RightResolution X₂)ᵒᵖ)
:
(CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).obj R = (Opposite.unop R).unop
@[simp]
theorem
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor_map_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₂ᵒᵖ)
[W₁.IsMultiplicative]
{X✝ Y✝ : (Φ.op.RightResolution X₂)ᵒᵖ}
(φ : X✝ ⟶ Y✝)
:
((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).map φ).f = φ.unop.f.unop
def
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence
{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₂)
[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.
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso
{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₂)
[W₁.IsMultiplicative]
:
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso
{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₂)
[W₁.IsMultiplicative]
:
(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (Φ.LeftResolution X₂)ᵒᵖ)
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse
{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₂)
[W₁.IsMultiplicative]
:
(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).inverse = (CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp
@[simp]
theorem
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor
{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₂)
[W₁.IsMultiplicative]
:
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_6, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.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}
[CategoryTheory.Category.{u_5, u_1} C₁]
[CategoryTheory.Category.{u_6, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D₂]
[CategoryTheory.Category.{u_8, u_4} H]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
[Φ.HasRightResolutions]
{F G : CategoryTheory.Functor D₂ H}
(α : F ⟶ G)
:
CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.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}
[CategoryTheory.Category.{u_5, u_1} C₁]
[CategoryTheory.Category.{u_6, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.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}
[CategoryTheory.Category.{u_5, u_1} C₁]
[CategoryTheory.Category.{u_6, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D₂]
[CategoryTheory.Category.{u_8, u_4} H]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
[Φ.HasLeftResolutions]
{F G : CategoryTheory.Functor D₂ H}
(α : F ⟶ G)
:
CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))