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₃ : W₃.IsInvertedBy (L₁.comp L₂))
(hW₁₃ : W₁ ≤ W₃)
(hW₂₃ : W₂ ≤ W₃.map L₁)
:
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (L₁.comp L₂) W₃ E
Under some conditions on the MorphismProperty, functors satisfying the strict
universal property of the localization are stable under composition
Equations
- h₁.comp h₂ W₃ hW₃ hW₁₃ hW₂₃ = { inverts := hW₃, lift := fun (F : CategoryTheory.Functor C₁ E) (hF : W₃.IsInvertedBy F) => h₂.lift (h₁.lift F ⋯) ⋯, fac := ⋯, uniq := ⋯ }
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₂)
[L₁.IsLocalization W₁]
[L₂.IsLocalization W₂]
(W₃ : CategoryTheory.MorphismProperty C₁)
(hW₃ : W₃.IsInvertedBy (L₁.comp L₂))
(hW₁₃ : W₁ ≤ W₃)
(hW₂₃ : W₂ ≤ W₃.map L₁)
:
(L₁.comp L₂).IsLocalization W₃
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₁)
[L₁.IsLocalization W₁]
[(L₁.comp L₂).IsLocalization W₃]
(hW₁₃ : W₁ ≤ W₃)
(hW₂₃ : W₂ = W₃.map L₁)
:
L₂.IsLocalization W₂