Derivability structures deduced from localized equivalences #
Assume that we have a diagram of localizer morphisms, in the
sense that we have an isomorphism T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor.
T
W₁ ---> W₂
| |
L| |R
v v
W₁' ---> W₂'
B
In this file, we obtain the lemma
LocalizerMorphism.isRightDerivabilityStructure_of_isLocalizedEquivalence which shows
that if both L and R are localized equivalences (with R.functor essentially surjective),
then B is a right derivability structure when T is a right derivability structure,
the 2-square above is Guitart exact (and W₂' respects isomorphisms).
In addition, if we require that L.functor is also essentially surjective,
that R.functor is full and that W₂ is induced by W₂', then
B is a right derivability structure iff T is.
The dual results for left derivability structures are also obtained.
This will be particularly useful when L.functor and R.functor are functors
from a category to a quotient category (e.g. functors from categories of homological
complexes to homotopy categories).
theorem
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₂'.RespectsIso]
[L.IsLocalizedEquivalence]
[R.IsLocalizedEquivalence]
[R.functor.EssSurj]
[T.IsLeftDerivabilityStructure]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
[TwoSquare.GuitartExact iso.inv]
:
theorem
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₂'.RespectsIso]
[L.IsLocalizedEquivalence]
[R.IsLocalizedEquivalence]
[R.functor.EssSurj]
[L.functor.EssSurj]
[R.functor.Full]
[R.IsInduced]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
[TwoSquare.GuitartExact iso.inv]
:
theorem
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_isLocalizedEquivalence
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₂'.RespectsIso]
[L.IsLocalizedEquivalence]
[R.IsLocalizedEquivalence]
[R.functor.EssSurj]
[T.IsRightDerivabilityStructure]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
[TwoSquare.GuitartExact iso.hom]
:
theorem
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_isLocalizedEquivalence
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₂'.RespectsIso]
[L.IsLocalizedEquivalence]
[R.IsLocalizedEquivalence]
[R.functor.EssSurj]
[L.functor.EssSurj]
[R.functor.Full]
[R.IsInduced]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
[TwoSquare.GuitartExact iso.hom]
:
theorem
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_equivalences
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₁'.RespectsIso]
[W₂'.RespectsIso]
[L.IsInduced]
[L.functor.IsEquivalence]
[R.IsInduced]
[R.functor.IsEquivalence]
[T.IsLeftDerivabilityStructure]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
:
theorem
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_equivalences
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₁'.RespectsIso]
[W₂'.RespectsIso]
[L.IsInduced]
[L.functor.IsEquivalence]
[R.IsInduced]
[R.functor.IsEquivalence]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
:
theorem
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₁'.RespectsIso]
[W₂'.RespectsIso]
[L.IsInduced]
[L.functor.IsEquivalence]
[R.IsInduced]
[R.functor.IsEquivalence]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
:
theorem
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_equivalences
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_3}
{D₂ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D₁]
[Category.{v_4, u_4} D₂]
{W₁ : MorphismProperty C₁}
{W₁' : MorphismProperty D₁}
{W₂ : MorphismProperty C₂}
{W₂' : MorphismProperty D₂}
{T : LocalizerMorphism W₁ W₂}
{L : LocalizerMorphism W₁ W₁'}
{R : LocalizerMorphism W₂ W₂'}
{B : LocalizerMorphism W₁' W₂'}
[W₁'.RespectsIso]
[W₂'.RespectsIso]
[L.IsInduced]
[L.functor.IsEquivalence]
[R.IsInduced]
[R.functor.IsEquivalence]
[T.IsRightDerivabilityStructure]
(iso : T.functor.comp R.functor ≅ L.functor.comp B.functor)
: