Composition of localization functors #
Given two composable functors L₁ : C₁ ⥤ C₂ and L₂ : C₂ ⥤ C₃, it is shown
in this file that under some suitable conditions on W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂ and W₃ : MorphismProperty C₁, then
if L₁ : C₁ ⥤ C₂ is a localization functor for W₁,
then the composition L₁ ⋙ L₂ : C₁ ⥤ C₃ is a localization functor for W₃
if and only if L₂ : C₂ ⥤ C₃ is a localization functor for W₂.
The two implications are the lemmas Functor.IsLocalization.comp and
Functor.IsLocalization.of_comp.
def
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.comp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{E : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₄, u₄} E]
{L₁ : CategoryTheory.Functor C₁ C₂}
{L₂ : CategoryTheory.Functor C₂ C₃}
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(h₁ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L₁ W₁ E)
(h₂ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L₂ W₂ E)
(W₃ : CategoryTheory.MorphismProperty C₁)
(hW₃ : CategoryTheory.MorphismProperty.IsInvertedBy W₃ (CategoryTheory.Functor.comp L₁ L₂))
(hW₁₃ : W₁ ⊆ W₃)
(hW₂₃ : W₂ ⊆ CategoryTheory.MorphismProperty.map W₃ L₁)
:
Under some conditions on the MorphismProperty, functors satisfying the strict
universal property of the localization are stable under composition
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.IsLocalization.comp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
(L₁ : CategoryTheory.Functor C₁ C₂)
(L₂ : CategoryTheory.Functor C₂ C₃)
(W₁ : CategoryTheory.MorphismProperty C₁)
(W₂ : CategoryTheory.MorphismProperty C₂)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
[CategoryTheory.Functor.IsLocalization L₂ W₂]
(W₃ : CategoryTheory.MorphismProperty C₁)
(hW₃ : CategoryTheory.MorphismProperty.IsInvertedBy W₃ (CategoryTheory.Functor.comp L₁ L₂))
(hW₁₃ : W₁ ⊆ W₃)
(hW₂₃ : W₂ ⊆ CategoryTheory.MorphismProperty.map W₃ L₁)
:
theorem
CategoryTheory.Functor.IsLocalization.of_comp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
(L₁ : CategoryTheory.Functor C₁ C₂)
(L₂ : CategoryTheory.Functor C₂ C₃)
(W₁ : CategoryTheory.MorphismProperty C₁)
(W₂ : CategoryTheory.MorphismProperty C₂)
(W₃ : CategoryTheory.MorphismProperty C₁)
[CategoryTheory.Functor.IsLocalization L₁ W₁]
[CategoryTheory.Functor.IsLocalization (CategoryTheory.Functor.comp L₁ L₂) W₃]
(hW₁₃ : W₁ ⊆ W₃)
(hW₂₃ : W₂ = CategoryTheory.MorphismProperty.map W₃ L₁)
: