Theorems · Theorem · category theory

CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.EssSurj] [L.Full]
  (W : CategoryTheory.MorphismProperty C),
  W.IsInvertedBy L → (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π) → L.IsLocalization W

Defined in

Mathlib.CategoryTheory.Localization.OfQuotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.EssSurjCategoryTheory.Functor.Full