Theorems · Theorem · category theory

CategoryTheory.Subobject.Classifier.uniq

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

χ m is the only map X ⟶ Ω which forms the appropriate pullback square for any χ₀'.

Defined in

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Cited by

6 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Mono