Theorems · Theorem · category theory

CategoryTheory.Localization.Construction.morphismProperty_eq_top

∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
  (P : CategoryTheory.MorphismProperty W.Localization) [P.IsStableUnderComposition],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) →
    (∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (CategoryTheory.Localization.Construction.wInv w hw)) → P = ⊤

A MorphismProperty in W.Localization is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category, the inverses of the morphisms in W and if it is stable under composition

Defined in

Mathlib.CategoryTheory.Localization.Construction

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderComposition