Theorems · Definition · category theory

CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (E : Type u_3) →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget W.Q W E

The localized category W.Localization that was constructed satisfies the universal property of the localization.

Defined in

Mathlib.CategoryTheory.Localization.Predicate

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category