Theorems · Theorem · category theory

CategoryTheory.HasClassifier.unique

Deprecated since 2026-03-06Use CategoryTheory.HasSubobjectClassifier.unique instead.

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] (χ' : X ⟶ CategoryTheory.HasSubobjectClassifier.Ω C),
  CategoryTheory.IsPullback m (⋯.some.χ₀ U) χ' (CategoryTheory.HasSubobjectClassifier.truth C) →
    χ' = CategoryTheory.HasSubobjectClassifier.χ m

Alias of CategoryTheory.HasSubobjectClassifier.unique. χ m is the only map for which the associated square is a pullback square.

Defined in

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.HasSubobjectClassifierCategoryTheory.Mono