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
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 resolutions of an object in the target category of a localizer morphism.
- X₁ : C₁
an object in the source category
- w : X₂ ⟶ Φ.functor.toPrefunctor.obj self.X₁
a morphism to 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 : CategoryTheory.LocalizerMorphism.RightResolution Φ X₂)
:
∃ (X₁ : C₁) (w : X₂ ⟶ Φ.functor.toPrefunctor.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₂)
:
A localizer morphism has right resolutions when any object has a right resolution.
Equations
Instances For
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.toPrefunctor.map self.f) = R'.w
Instances For
@[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.toPrefunctor.obj R'.X₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp R.w (CategoryTheory.CategoryStruct.comp (Φ.functor.toPrefunctor.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₂)
:
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₂)
:
The identity of a object in Φ.RightResolution X₂.
Equations
- One or more equations did not get rendered due to their size.
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₂}
[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'')
:
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'')
:
The composition of morphisms in Φ.RightResolution X₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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₁]
:
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₂)
:
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)
:
@[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.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₂.toPrefunctor.obj (Φ.functor.toPrefunctor.obj X₁)))