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₄} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] [Category.{v₄, u₄} E] {L₁ : Functor C₁ C₂} {L₂ : Functor C₂ C₃} {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E) (h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E) (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁.comp L₂)) (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) :
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₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (L₁ : Functor C₁ C₂) (L₂ : Functor C₂ C₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (W₃ : 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₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (L₁ : Functor C₁ C₂) (L₂ : Functor C₂ C₃) (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₁) [L₁.IsLocalization W₁] [(L₁.comp L₂).IsLocalization W₃] (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ = W₃.map L₁) :
L₂.IsLocalization W₂