Theorems · Inductive type · category theory

CategoryTheory.Subobject.Classifier

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)

A monomorphism truth : Ω₀ ⟶ Ω is a subobject classifier if, for every monomorphism m : U ⟶ X in C, there is a unique map χ : X ⟶ Ω such that for some (necessarily unique) χ₀ : U ⟶ Ω₀ the following square is a pullback square: `` U m -> X | | χ₀ U χ m | | v v Ω₀ truth --> Ω ` An equivalent formulation replaces Ω₀` with the terminal object.

Defined in

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Cited by

46 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category