Theorems · Theorem · category theory

CategoryTheory.Functor.IsLocalization.of_comp

∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : 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₃], W₁ ≤ W₃ → W₂ = W₃.map L₁ → L₂.IsLocalization W₂

Defined in

Mathlib.CategoryTheory.Localization.Composition

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalization