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.

Under some conditions on the MorphismProperty, functors satisfying the strict universal property of the localization are stable under composition

Instances For