# 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₄} [] [] [] [] {L₁ : } {L₂ : } {W₁ : } {W₂ : } (W₃ : ) (hW₃ : W₃.IsInvertedBy (L₁.comp L₂)) (hW₁₃ : W₁ W₃) (hW₂₃ : W₂ W₃.map L₁) :

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 : ) (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₃} [] [] [] (L₁ : ) (L₂ : ) (W₁ : ) (W₂ : ) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (W₃ : ) (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₃} [] [] [] (L₁ : ) (L₂ : ) (W₁ : ) (W₂ : ) (W₃ : ) [L₁.IsLocalization W₁] [(L₁.comp L₂).IsLocalization W₃] (hW₁₃ : W₁ W₃) (hW₂₃ : W₂ = W₃.map L₁) :
L₂.IsLocalization W₂