Theorems · Theorem · category theory

CategoryTheory.LocalizerMorphism.isLocalization_of_isLocalizedFullyFaithful

∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedFullyFaithful]
  {L₂ : CategoryTheory.Functor C₂ D₂} [L₂.IsLocalization W₂] {L₁ : CategoryTheory.Functor C₁ D₁}
  {F : CategoryTheory.Functor D₁ D₂} (iso : Φ.functor.comp L₂ ≅ L₁.comp F) [F.Full] [F.Faithful] [L₁.EssSurj],
  L₁.IsLocalization W₁

Assume that a localizer morphism Φ : LocalizerMorphism W₁ W₂ induces a fully faithful functor on the localized categories. If L₂ : C₂ ⥤ D₂ is a localization functor for W₂ and we have a factorization iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F as an essentially surjective functor L₁ : C₁ ⥤ D₁ followed by a fully faithful functor F : D₁ ⥤ D₂, then L₁ is a localization functor for W₁.

Defined in

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithfulCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.FullCategoryTheory.Functor.FaithfulCategoryTheory.Functor.EssSurj