Subobject Classifier #

We define a structure containing the data of a subobject classifier in a category C as CategoryTheory.Subobject.Classifier C.

c.f. the following Lean 3 code, where similar work was done: https://github.com/b-mehta/topos/blob/master/src/subobject_classifier.lean

Main definitions #

Let C refer to a category with a terminal object.

CategoryTheory.Subobject.Classifier C is the data of a subobject classifier in C.
CategoryTheory.HasSubobjectClassifier C says that there is at least one subobject classifier. Ω C denotes a choice of subobject classifier.

Main results #

It is a theorem that the truth morphism ⊤_ C ⟶ Ω C is a (split, and therefore regular) monomorphism, simply because its source is the terminal object.
An instance of IsRegularMonoCategory C is exhibited for any category with a subobject classifier.
CategoryTheory.Subobject.Classifier.representableBy: any subobject classifier Ω in C represents the subobjects functor CategoryTheory.Subobject.presheaf C, assuming C has pullbacks.
CategoryTheory.SubobjectRepresentableBy.classifier: any representation Ω of CategoryTheory.Subobject.presheaf C is a subobject classifier in C.
CategoryTheory.hasClassifier_isRepresentable_iff: from the two above mappings, we get that a category C with pullbacks has a subobject classifier if and only if the subobjects presheaf CategoryTheory.Subobject.presheaf C is representable (Proposition 1 in Section I.3 of [MLM92]).

References #

S. MacLane and I. Moerdijk, Sheaves in Geometry and Logic

source

structure CategoryTheory.Subobject.Classifier (C : Type u) [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.

Ω₀ : C
The domain of the truth morphism
Ω : C
The codomain of the truth morphism
truth : self.Ω₀ ⟶ self.Ω
The truth morphism of the subobject classifier
mono_truth : Mono self.truth
The truth morphism is a monomorphism
χ₀ (U : C) : U ⟶ self.Ω₀
The top arrow in the pullback square
χ {U X : C} (m : U ⟶ X) [Mono m] : X ⟶ self.Ω
For any monomorphism U ⟶ X, there is an associated characteristic map X ⟶ Ω.
isPullback {U X : C} (m : U ⟶ X) [Mono m] : IsPullback m (self.χ₀ U) (self.χ m) self.truth
χ₀ U and χ m form the appropriate pullback square.
uniq {U X : C} (m : U ⟶ X) [Mono m] {χ₀' : U ⟶ self.Ω₀} {χ' : X ⟶ self.Ω} (hχ' : IsPullback m χ₀' χ' self.truth) : χ' = self.χ m
χ m is the only map X ⟶ Ω which forms the appropriate pullback square for any χ₀'.

Instances For

source

@[deprecated CategoryTheory.Subobject.Classifier (since := "2026-03-06")]

def CategoryTheory.Classifier (C : Type u) [Category.{v, u} C] :

Type (max u v)

Alias of CategoryTheory.Subobject.Classifier.

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

An equivalent formulation replaces Ω₀ with the terminal object.

Equations

CategoryTheory.Classifier = CategoryTheory.Subobject.Classifier

Instances For

source

def CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) :

Classifier C

More explicit constructor in case Ω₀ is already known to be a terminal object.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) :

(mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω₀ = Ω₀

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) {U✝ X✝ : C} (m : U✝ ⟶ X✝) (x✝ : Mono m) :

(mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ m = χ m

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) :

(mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω = Ω

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_truth {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) :

(mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).truth = truth

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) (Y : C) :

(mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ₀ Y = t.from Y

source

@[deprecated CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ (since := "2026-03-06")]

def CategoryTheory.Classifier.mkOfTerminalΩ₀ {C : Type u} [Category.{v, u} C] (Ω₀ : C) (t : Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m], IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : Mono m] (χ' : X ⟶ Ω), IsPullback m (t.from U) χ' truth → χ' = χ m) :

Subobject.Classifier C

Alias of CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀.

More explicit constructor in case Ω₀ is already known to be a terminal object.

Equations

@CategoryTheory.Classifier.mkOfTerminalΩ₀ = @CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀

Instances For

source

@[implicit_reducible]

instance CategoryTheory.Subobject.Classifier.instUniqueHomΩ₀ {C : Type u} [Category.{v, u} C] {c : Classifier C} (Y : C) :

Unique (Y ⟶ c.Ω₀)

Equations

CategoryTheory.Subobject.Classifier.instUniqueHomΩ₀ Y = { default := c.χ₀ Y, uniq := ⋯ }

source

def CategoryTheory.Subobject.Classifier.isTerminalΩ₀ {C : Type u} [Category.{v, u} C] {c : Classifier C} :

Limits.IsTerminal c.Ω₀

Given c : Classifier C, c.Ω₀ is a terminal object. Prefer c.χ₀ over c.isTerminalΩ₀.from.

Equations

CategoryTheory.Subobject.Classifier.isTerminalΩ₀ = CategoryTheory.Limits.IsTerminal.ofUnique c.Ω₀

Instances For

source

@[deprecated CategoryTheory.Subobject.Classifier.isTerminalΩ₀ (since := "2026-03-06")]

def CategoryTheory.Classifier.isTerminalΩ₀ {C : Type u} [Category.{v, u} C] {c : Subobject.Classifier C} :

Limits.IsTerminal c.Ω₀

Alias of CategoryTheory.Subobject.Classifier.isTerminalΩ₀.

Given c : Classifier C, c.Ω₀ is a terminal object. Prefer c.χ₀ over c.isTerminalΩ₀.from.

Equations

@CategoryTheory.Classifier.isTerminalΩ₀ = @CategoryTheory.Subobject.Classifier.isTerminalΩ₀

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀ {C : Type u} [Category.{v, u} C] (c : Classifier C) :

isTerminalΩ₀.from = c.χ₀

source

@[deprecated CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀ (since := "2026-03-06")]

theorem CategoryTheory.Classifier.isTerminalFrom_eq_χ₀ {C : Type u} [Category.{v, u} C] (c : Subobject.Classifier C) :

Subobject.Classifier.isTerminalΩ₀.from = c.χ₀

Alias of CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀.

source

class CategoryTheory.HasSubobjectClassifier (C : Type u) [Category.{v, u} C] :

Prop

A category C has a subobject classifier if there is at least one subobject classifier.

exists_classifier : Nonempty (Subobject.Classifier C)
There is some classifier.

Instances

source

@[deprecated CategoryTheory.HasSubobjectClassifier (since := "2026-03-06")]

def CategoryTheory.HasClassifier (C : Type u) [Category.{v, u} C] :

Prop

Alias of CategoryTheory.HasSubobjectClassifier.

A category C has a subobject classifier if there is at least one subobject classifier.

Equations

CategoryTheory.HasClassifier = CategoryTheory.HasSubobjectClassifier

Instances For

source

@[reducible, inline]

noncomputable abbrev CategoryTheory.HasSubobjectClassifier.Ω₀ (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

Notation for the Ω₀ in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasSubobjectClassifier.Ω₀ C = ⋯.some.Ω₀

Instances For

source

@[deprecated CategoryTheory.HasSubobjectClassifier.Ω₀ (since := "2026-03-06")]

def CategoryTheory.HasClassifier.Ω₀ (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

Alias of CategoryTheory.HasSubobjectClassifier.Ω₀.

Notation for the Ω₀ in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasClassifier.Ω₀ = CategoryTheory.HasSubobjectClassifier.Ω₀

Instances For

source

@[reducible, inline]

noncomputable abbrev CategoryTheory.HasSubobjectClassifier.Ω (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

Notation for the Ω in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasSubobjectClassifier.Ω C = ⋯.some.Ω

Instances For

source

@[deprecated CategoryTheory.HasSubobjectClassifier.Ω (since := "2026-03-06")]

def CategoryTheory.HasClassifier.Ω (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

Alias of CategoryTheory.HasSubobjectClassifier.Ω.

Notation for the Ω in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasClassifier.Ω = CategoryTheory.HasSubobjectClassifier.Ω

Instances For

source

@[reducible, inline]

noncomputable abbrev CategoryTheory.HasSubobjectClassifier.truth (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

Ω₀ C ⟶ Ω C

Notation for the "truth arrow" in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasSubobjectClassifier.truth C = ⋯.some.truth

Instances For

source

@[deprecated CategoryTheory.HasSubobjectClassifier.truth (since := "2026-03-06")]

def CategoryTheory.HasClassifier.truth (C : Type u) [Category.{v, u} C] [HasSubobjectClassifier C] :

HasSubobjectClassifier.Ω₀ C ⟶ HasSubobjectClassifier.Ω C

Alias of CategoryTheory.HasSubobjectClassifier.truth.

Notation for the "truth arrow" in an arbitrary choice of a subobject classifier

Equations

CategoryTheory.HasClassifier.truth = CategoryTheory.HasSubobjectClassifier.truth

Instances For

source

noncomputable def CategoryTheory.HasSubobjectClassifier.χ {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

X ⟶ Ω C

returns the characteristic morphism of the subobject (m : U ⟶ X) [Mono m]

Equations

CategoryTheory.HasSubobjectClassifier.χ m = ⋯.some.χ m

Instances For

source

@[deprecated CategoryTheory.HasSubobjectClassifier.χ (since := "2026-03-06")]

def CategoryTheory.HasClassifier.χ {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

X ⟶ HasSubobjectClassifier.Ω C

Alias of CategoryTheory.HasSubobjectClassifier.χ.

returns the characteristic morphism of the subobject (m : U ⟶ X) [Mono m]

Equations

@CategoryTheory.HasClassifier.χ = @CategoryTheory.HasSubobjectClassifier.χ

Instances For

source

theorem CategoryTheory.HasSubobjectClassifier.isPullback_χ {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

IsPullback m (⋯.some.χ₀ U) (χ m) (truth C)

The diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

is a pullback square.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.isPullback_χ (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.isPullback_χ {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

IsPullback m (⋯.some.χ₀ U) (HasSubobjectClassifier.χ m) (HasSubobjectClassifier.truth C)

Alias of CategoryTheory.HasSubobjectClassifier.isPullback_χ.

The diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

is a pullback square.

source

theorem CategoryTheory.HasSubobjectClassifier.comm {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

CategoryStruct.comp m (χ m) = CategoryStruct.comp (⋯.some.χ₀ U) (truth C)

The diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

commutes.

source

theorem CategoryTheory.HasSubobjectClassifier.comm_assoc {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] {Z : C} (h : Ω C ⟶ Z) :

CategoryStruct.comp m (CategoryStruct.comp (χ m) h) = CategoryStruct.comp (⋯.some.χ₀ U) (CategoryStruct.comp (truth C) h)

The diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

commutes.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.comm (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.comm {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] :

CategoryStruct.comp m (HasSubobjectClassifier.χ m) = CategoryStruct.comp (⋯.some.χ₀ U) (HasSubobjectClassifier.truth C)

Alias of CategoryTheory.HasSubobjectClassifier.comm.

The diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

commutes.

source

theorem CategoryTheory.HasSubobjectClassifier.unique {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] (χ' : X ⟶ Ω C) (hχ' : IsPullback m (⋯.some.χ₀ U) χ' (truth C)) :

χ' = χ m

χ m is the only map for which the associated square is a pullback square.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.unique (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.unique {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] {U X : C} (m : U ⟶ X) [Mono m] (χ' : X ⟶ HasSubobjectClassifier.Ω C) (hχ' : IsPullback m (⋯.some.χ₀ U) χ' (HasSubobjectClassifier.truth C)) :

χ' = HasSubobjectClassifier.χ m

Alias of CategoryTheory.HasSubobjectClassifier.unique.

χ m is the only map for which the associated square is a pullback square.

source

instance CategoryTheory.HasSubobjectClassifier.truthIsSplitMono {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

IsSplitMono (truth C)

source

@[deprecated CategoryTheory.HasSubobjectClassifier.truthIsSplitMono (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.truthIsSplitMono {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

IsSplitMono (HasSubobjectClassifier.truth C)

Alias of CategoryTheory.HasSubobjectClassifier.truthIsSplitMono.

source

noncomputable def CategoryTheory.HasSubobjectClassifier.truthIsRegularMono {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

RegularMono (truth C)

truth C is a regular monomorphism (because it is split).

Equations

CategoryTheory.HasSubobjectClassifier.truthIsRegularMono = CategoryTheory.RegularMono.ofIsSplitMono (CategoryTheory.HasSubobjectClassifier.truth C)

Instances For

source

@[deprecated CategoryTheory.HasSubobjectClassifier.truthIsRegularMono (since := "2026-03-06")]

def CategoryTheory.HasClassifier.truthIsRegularMono {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

RegularMono (HasSubobjectClassifier.truth C)

Alias of CategoryTheory.HasSubobjectClassifier.truthIsRegularMono.

truth C is a regular monomorphism (because it is split).

Equations

@CategoryTheory.HasClassifier.truthIsRegularMono = @CategoryTheory.HasSubobjectClassifier.truthIsRegularMono

Instances For

source

instance CategoryTheory.HasSubobjectClassifier.instIsRegularMonoTruth {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

IsRegularMono (truth C)

source

instance CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

IsRegularMonoCategory C

The following diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

being a pullback for any monic m means that every monomorphism in C is the pullback of a regular monomorphism; since regularity is stable under base change, every monomorphism is regular. Hence, C is a regular mono category. It also follows that C is a balanced category.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.isRegularMonoCategory {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] :

IsRegularMonoCategory C

Alias of CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory.

The following diagram

      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω

source

instance CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] (D : Type u₀) [Category.{v₀, u₀} D] (F : Functor C D) [F.Faithful] :

F.ReflectsIsomorphisms

If the source of a faithful functor has a subobject classifier, the functor reflects isomorphisms. This holds for any balanced category.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.reflectsIsomorphisms {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] (D : Type u₀) [Category.{v₀, u₀} D] (F : Functor C D) [F.Faithful] :

F.ReflectsIsomorphisms

Alias of CategoryTheory.HasSubobjectClassifier.reflectsIsomorphisms.

If the source of a faithful functor has a subobject classifier, the functor reflects isomorphisms. This holds for any balanced category.

source

instance CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] (D : Type u₀) [Category.{v₀, u₀} D] (F : Functor Cᵒᵖ D) [F.Faithful] :

F.ReflectsIsomorphisms

If the source of a faithful functor is the opposite category of one with a subobject classifier, the same holds -- the functor reflects isomorphisms.

source

@[deprecated CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp (since := "2026-03-06")]

theorem CategoryTheory.HasClassifier.reflectsIsomorphismsOp {C : Type u} [Category.{v, u} C] [HasSubobjectClassifier C] (D : Type u₀) [Category.{v₀, u₀} D] (F : Functor Cᵒᵖ D) [F.Faithful] :

F.ReflectsIsomorphisms

Alias of CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp.

If the source of a faithful functor is the opposite category of one with a subobject classifier, the same holds -- the functor reflects isomorphisms.

The representability theorem of subobject classifiers #

From classifiers to representations #

source

@[reducible, inline]

abbrev CategoryTheory.Subobject.Classifier.truth_as_subobject {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) :

Subobject 𝒞.Ω

The subobject of 𝒞.Ω corresponding to the truth morphism.

Equations

𝒞.truth_as_subobject = CategoryTheory.Subobject.mk 𝒞.truth

Instances For

source

@[deprecated CategoryTheory.Subobject.Classifier.truth_as_subobject (since := "2026-03-06")]

def CategoryTheory.Classifier.truth_as_subobject {C : Type u} [Category.{v, u} C] (𝒞 : Subobject.Classifier C) :

Subobject 𝒞.Ω

Alias of CategoryTheory.Subobject.Classifier.truth_as_subobject.

The subobject of 𝒞.Ω corresponding to the truth morphism.

Equations

@CategoryTheory.Classifier.truth_as_subobject = @CategoryTheory.Subobject.Classifier.truth_as_subobject

Instances For

source

theorem CategoryTheory.Subobject.Classifier.surjective_χ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω) :

∃ (Z : C) (i : Z ⟶ X) (x : Mono i), φ = 𝒞.χ i

source

@[deprecated CategoryTheory.Subobject.Classifier.surjective_χ (since := "2026-03-06")]

theorem CategoryTheory.Classifier.surjective_χ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω) :

∃ (Z : C) (i : Z ⟶ X) (x : Mono i), φ = 𝒞.χ i

Alias of CategoryTheory.Subobject.Classifier.surjective_χ.

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Classifier C) {Z X : C} (i : Z ⟶ X) [Mono i] :

(pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = Subobject.mk i

source

@[deprecated CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth (since := "2026-03-06")]

theorem CategoryTheory.Classifier.pullback_χ_obj_mk_truth {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Subobject.Classifier C) {Z X : C} (i : Z ⟶ X) [Mono i] :

(Subobject.pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = Subobject.mk i

Alias of CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth.

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω) :

𝒞.χ ((pullback φ).obj 𝒞.truth_as_subobject).arrow = φ

source

@[deprecated CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow (since := "2026-03-06")]

theorem CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω) :

𝒞.χ ((Subobject.pullback φ).obj 𝒞.truth_as_subobject).arrow = φ

Alias of CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow.

source

noncomputable def CategoryTheory.Subobject.Classifier.representableBy {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Classifier C) :

(Subobject.presheaf C).RepresentableBy 𝒞.Ω

Any subobject classifier Ω represents the subobjects functor Subobject.presheaf.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[deprecated CategoryTheory.Subobject.Classifier.representableBy (since := "2026-03-06")]

def CategoryTheory.Classifier.representableBy {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (𝒞 : Subobject.Classifier C) :

(Subobject.presheaf C).RepresentableBy 𝒞.Ω

Alias of CategoryTheory.Subobject.Classifier.representableBy.

Any subobject classifier Ω represents the subobjects functor Subobject.presheaf.

Equations

@CategoryTheory.Classifier.representableBy = @CategoryTheory.Subobject.Classifier.representableBy

Instances For

From representations to classifiers #

source

@[reducible, inline]

abbrev CategoryTheory.SubobjectRepresentableBy {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (Ω : C) :

Type (max (max u u v) v)

Abbreviation to enable dot notation on the hypothesis h stating that the subobjects presheaf is representable by some object Ω.

Equations

CategoryTheory.SubobjectRepresentableBy Ω = (Subobject.presheaf C).RepresentableBy Ω

Instances For

source

@[deprecated CategoryTheory.SubobjectRepresentableBy (since := "2026-03-06")]

def CategoryTheory.Classifier.SubobjectRepresentableBy {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (Ω : C) :

Type (max (max u u v) v)

Alias of CategoryTheory.SubobjectRepresentableBy.

Abbreviation to enable dot notation on the hypothesis h stating that the subobjects presheaf is representable by some object Ω.

Equations

@CategoryTheory.Classifier.SubobjectRepresentableBy = @CategoryTheory.SubobjectRepresentableBy

Instances For

source

def CategoryTheory.SubobjectRepresentableBy.Ω₀ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) :

Subobject Ω

h.Ω₀ is the subobject of Ω which corresponds to the identity 𝟙 Ω, given h : SubobjectRepresentableBy Ω.

Equations

h.Ω₀ = h.homEquiv (CategoryTheory.CategoryStruct.id Ω)

Instances For

source

theorem CategoryTheory.SubobjectRepresentableBy.homEquiv_eq {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {X : C} (f : X ⟶ Ω) :

h.homEquiv f = (Subobject.pullback f).obj h.Ω₀

h.homEquiv acts like an "object comprehension" operator: it maps any characteristic map f : X ⟶ Ω to the associated subobject of X, obtained by pulling back h.Ω₀ along f.

source

theorem CategoryTheory.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {X : C} (x : Subobject X) :

(Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x

For any subobject x, the pullback of h.Ω₀ along the characteristic map of x given by h.homEquiv is x itself.

source

def CategoryTheory.SubobjectRepresentableBy.χ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

X ⟶ Ω

h.χ m is the characteristic map of monomorphism m given by the bijection h.homEquiv.

Equations

h.χ m = h.homEquiv.symm (CategoryTheory.Subobject.mk m)

Instances For

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.iso {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

MonoOver.mk m ≅ Subobject.representative.obj ((Subobject.pullback (h.χ m)).obj h.Ω₀)

h.iso m is the isomorphism between m and the pullback of Ω₀ along the characteristic map of m.

Equations

h.iso m = (CategoryTheory.Subobject.representativeIso (CategoryTheory.MonoOver.mk m)).symm ≪≫ CategoryTheory.Subobject.representative.mapIso (CategoryTheory.eqToIso ⋯)

Instances For

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.π {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

U ⟶ Subobject.underlying.obj h.Ω₀

h.π m is the first projection in the following pullback square:

U --h.π m--> (Ω₀ : C)
|                |
m             Ω₀.arrow
|                |
v                v
X -----h.χ m---> Ω

Equations

h.π m = CategoryTheory.CategoryStruct.comp (h.iso m).hom.hom.left (CategoryTheory.Subobject.pullbackπ (h.χ m) h.Ω₀)

Instances For

source

@[simp]

theorem CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

CategoryStruct.comp (h.iso m).inv.hom.left (h.π m) = Subobject.pullbackπ (h.χ m) h.Ω₀

source

@[simp]

theorem CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] {Z : C} (h✝ : Subobject.underlying.obj h.Ω₀ ⟶ Z) :

CategoryStruct.comp (h.iso m).inv.hom.left (CategoryStruct.comp (h.π m) h✝) = CategoryStruct.comp (Subobject.pullbackπ (h.χ m) h.Ω₀) h✝

source

@[simp]

theorem CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

CategoryStruct.comp (h.iso m).inv.hom.left m = ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow

source

@[simp]

theorem CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] {Z : C} (h✝ : X ⟶ Z) :

CategoryStruct.comp (h.iso m).inv.hom.left (CategoryStruct.comp m h✝) = CategoryStruct.comp ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow h✝

source

theorem CategoryTheory.SubobjectRepresentableBy.isPullback {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [Mono m] :

IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow

source

theorem CategoryTheory.SubobjectRepresentableBy.uniq {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) {U X : C} {m : U ⟶ X} [Mono m] {χ' : X ⟶ Ω} {π : U ⟶ Subobject.underlying.obj h.Ω₀} (sq : IsPullback m π χ' h.Ω₀.arrow) :

χ' = h.χ m

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.isTerminalΩ₀ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) :

Limits.IsTerminal (Subobject.underlying.obj h.Ω₀)

The main non-trivial result: h.Ω₀ is actually a terminal object.

Equations

h.isTerminalΩ₀ = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (X : C) => h.π (CategoryTheory.CategoryStruct.id X)) ⋯

Instances For

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.χ₀ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) (U : C) :

U ⟶ Subobject.underlying.obj h.Ω₀

The unique map to the terminal object.

Equations

h.χ₀ U = h.isTerminalΩ₀.from U

Instances For

source

theorem CategoryTheory.SubobjectRepresentableBy.hasTerminal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) :

Limits.HasTerminal C

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.isoΩ₀ {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) [Limits.HasTerminal C] :

Subobject.underlying.obj h.Ω₀ ≅ ⊤_ C

h.isoΩ₀ is the unique isomorphism from h.Ω₀ to the canonical terminal object ⊤_ C.

Equations

h.isoΩ₀ = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso h.isTerminalΩ₀ (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.empty C))

Instances For

source

noncomputable def CategoryTheory.SubobjectRepresentableBy.classifier {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {Ω : C} (h : SubobjectRepresentableBy Ω) [Limits.HasTerminal C] :

Subobject.Classifier C

Any representation Ω of Subobject.presheaf C gives a subobject classifier with truth values object Ω.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CategoryTheory.hasSubobjectClassifier_iff_isRepresentable {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] :

HasSubobjectClassifier C ↔ (Subobject.presheaf C).IsRepresentable

A category has a subobject classifier if and only if the subobjects functor is representable.

source

@[deprecated CategoryTheory.hasSubobjectClassifier_iff_isRepresentable (since := "2026-03-06")]

theorem CategoryTheory.isRepresentable_hasClassifier_iff {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] :

HasSubobjectClassifier C ↔ (Subobject.presheaf C).IsRepresentable

Alias of CategoryTheory.hasSubobjectClassifier_iff_isRepresentable.

A category has a subobject classifier if and only if the subobjects functor is representable.

source

def CategoryTheory.Subobject.Classifier.hom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Classifier C) :

𝒞₁.Ω ⟶ 𝒞₂.Ω

The unique morphism between classifiers mapping each others characteristic maps

Equations

𝒞₁.hom 𝒞₂ = 𝒞₂.χ 𝒞₁.truth

Instances For

source

@[deprecated CategoryTheory.Subobject.Classifier.hom (since := "2026-03-06")]

def CategoryTheory.Classifier.hom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Subobject.Classifier C) :

𝒞₁.Ω ⟶ 𝒞₂.Ω

Alias of CategoryTheory.Subobject.Classifier.hom.

The unique morphism between classifiers mapping each others characteristic maps

Equations

@CategoryTheory.Classifier.hom = @CategoryTheory.Subobject.Classifier.hom

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.hom_comp_hom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : Classifier C) :

CategoryStruct.comp (𝒞₁.hom 𝒞₂) (𝒞₂.hom 𝒞₃) = 𝒞₁.hom 𝒞₃

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.hom_comp_hom_assoc {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : Classifier C) {Z : C} (h : 𝒞₃.Ω ⟶ Z) :

CategoryStruct.comp (𝒞₁.hom 𝒞₂) (CategoryStruct.comp (𝒞₂.hom 𝒞₃) h) = CategoryStruct.comp (𝒞₁.hom 𝒞₃) h

source

@[deprecated CategoryTheory.Subobject.Classifier.hom_comp_hom (since := "2026-03-06")]

theorem CategoryTheory.Classifier.hom_comp_hom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : Subobject.Classifier C) :

CategoryStruct.comp (𝒞₁.hom 𝒞₂) (𝒞₂.hom 𝒞₃) = 𝒞₁.hom 𝒞₃

Alias of CategoryTheory.Subobject.Classifier.hom_comp_hom.

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.hom_refl {C : Type u} [Category.{v, u} C] (𝒞₁ : Classifier C) :

𝒞₁.hom 𝒞₁ = CategoryStruct.id 𝒞₁.Ω

source

@[deprecated CategoryTheory.Subobject.Classifier.hom_refl (since := "2026-03-06")]

theorem CategoryTheory.Classifier.hom_refl {C : Type u} [Category.{v, u} C] (𝒞₁ : Subobject.Classifier C) :

𝒞₁.hom 𝒞₁ = CategoryStruct.id 𝒞₁.Ω

Alias of CategoryTheory.Subobject.Classifier.hom_refl.

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.χ_comp_hom {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Classifier C} {X Y : C} (m : X ⟶ Y) [Mono m] :

CategoryStruct.comp (𝒞₁.χ m) (𝒞₁.hom 𝒞₂) = 𝒞₂.χ m

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.χ_comp_hom_assoc {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Classifier C} {X Y : C} (m : X ⟶ Y) [Mono m] {Z : C} (h : 𝒞₂.Ω ⟶ Z) :

CategoryStruct.comp (𝒞₁.χ m) (CategoryStruct.comp (𝒞₁.hom 𝒞₂) h) = CategoryStruct.comp (𝒞₂.χ m) h

source

@[deprecated CategoryTheory.Subobject.Classifier.χ_comp_hom (since := "2026-03-06")]

theorem CategoryTheory.Classifier.χ_comp_hom {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Subobject.Classifier C} {X Y : C} (m : X ⟶ Y) [Mono m] :

CategoryStruct.comp (𝒞₁.χ m) (𝒞₁.hom 𝒞₂) = 𝒞₂.χ m

Alias of CategoryTheory.Subobject.Classifier.χ_comp_hom.

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.truth_comp_hom {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Classifier C} :

CategoryStruct.comp 𝒞₁.truth (𝒞₁.hom 𝒞₂) = CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) 𝒞₂.truth

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.truth_comp_hom_assoc {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Classifier C} {Z : C} (h : 𝒞₂.Ω ⟶ Z) :

CategoryStruct.comp 𝒞₁.truth (CategoryStruct.comp (𝒞₁.hom 𝒞₂) h) = CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) (CategoryStruct.comp 𝒞₂.truth h)

source

@[deprecated CategoryTheory.Subobject.Classifier.truth_comp_hom (since := "2026-03-06")]

theorem CategoryTheory.Classifier.truth_comp_hom {C : Type u} [Category.{v, u} C] {𝒞₁ 𝒞₂ : Subobject.Classifier C} :

CategoryStruct.comp 𝒞₁.truth (𝒞₁.hom 𝒞₂) = CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) 𝒞₂.truth

Alias of CategoryTheory.Subobject.Classifier.truth_comp_hom.

source

def CategoryTheory.Subobject.Classifier.uniqueUpToIso {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Classifier C) :

𝒞₁.Ω ≅ 𝒞₂.Ω

a concrete equivalence of any two subobject classifiers

Equations

𝒞₁.uniqueUpToIso 𝒞₂ = { hom := 𝒞₁.hom 𝒞₂, inv := 𝒞₂.hom 𝒞₁, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.uniqueUpToIso_inv {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Classifier C) :

(𝒞₁.uniqueUpToIso 𝒞₂).inv = 𝒞₂.hom 𝒞₁

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.uniqueUpToIso_hom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Classifier C) :

(𝒞₁.uniqueUpToIso 𝒞₂).hom = 𝒞₁.hom 𝒞₂

source

@[deprecated CategoryTheory.Subobject.Classifier.uniqueUpToIso (since := "2026-03-06")]

def CategoryTheory.Classifier.uniqueUpToIso {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Subobject.Classifier C) :

𝒞₁.Ω ≅ 𝒞₂.Ω

Alias of CategoryTheory.Subobject.Classifier.uniqueUpToIso.

a concrete equivalence of any two subobject classifiers

Equations

@CategoryTheory.Classifier.uniqueUpToIso = @CategoryTheory.Subobject.Classifier.uniqueUpToIso

Instances For

source

instance CategoryTheory.Subobject.Classifier.instIsIsoHom {C : Type u} [Category.{v, u} C] (𝒞₁ 𝒞₂ : Classifier C) :

IsIso (𝒞₁.hom 𝒞₂)

source

def CategoryTheory.Subobject.Classifier.ofIso {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) :

Classifier C

Being a subobject classifier is preserved under isomorphism.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofIso_χ {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) {F G : C} (m : F ⟶ G) (x✝ : Mono m) :

(𝒞.ofIso eΩ eΩ₀ from' t ht).χ m = CategoryStruct.comp (𝒞.χ m) eΩ.hom

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofIso_Ω₀ {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) :

(𝒞.ofIso eΩ eΩ₀ from' t ht).Ω₀ = Ω₀

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofIso_truth {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) :

(𝒞.ofIso eΩ eΩ₀ from' t ht).truth = t

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofIso_χ₀ {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) (C✝ : C) :

(𝒞.ofIso eΩ eΩ₀ from' t ht).χ₀ C✝ = from' C✝

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofIso_Ω {C : Type u} [Category.{v, u} C] (𝒞 : Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) :

(𝒞.ofIso eΩ eΩ₀ from' t ht).Ω = Ω

source

@[deprecated CategoryTheory.Subobject.Classifier.ofIso (since := "2026-03-06")]

def CategoryTheory.Classifier.ofIso {C : Type u} [Category.{v, u} C] (𝒞 : Subobject.Classifier C) {Ω₀ Ω : C} (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω) (ht : t = CategoryStruct.comp eΩ₀.inv (CategoryStruct.comp 𝒞.truth eΩ.hom) := by cat_disch) :

Subobject.Classifier C

Alias of CategoryTheory.Subobject.Classifier.ofIso.

Being a subobject classifier is preserved under isomorphism.

Equations

@CategoryTheory.Classifier.ofIso = @CategoryTheory.Subobject.Classifier.ofIso

Instances For

source

def CategoryTheory.Subobject.Classifier.ofEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) :

Classifier D

The image of a subobject classifier under an equivalence of categories is a subobject classifier.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofEquivalence_truth {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) :

(𝒞₁.ofEquivalence e).truth = e.functor.map 𝒞₁.truth

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofEquivalence_Ω {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) :

(𝒞₁.ofEquivalence e).Ω = e.functor.obj 𝒞₁.Ω

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofEquivalence_χ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) {U✝ X✝ : D} (m : U✝ ⟶ X✝) [Mono m] :

(𝒞₁.ofEquivalence e).χ m = CategoryStruct.comp (e.counitInv.app X✝) (e.functor.map (𝒞₁.χ (e.inverse.map m)))

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofEquivalence_χ₀ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) (Y : D) :

(𝒞₁.ofEquivalence e).χ₀ Y = CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (𝒞₁.χ₀ (e.inverse.obj Y)))

source

@[simp]

theorem CategoryTheory.Subobject.Classifier.ofEquivalence_Ω₀ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Classifier C) (e : C ≌ D) :

(𝒞₁.ofEquivalence e).Ω₀ = e.functor.obj 𝒞₁.Ω₀

source

@[deprecated CategoryTheory.Subobject.Classifier.ofEquivalence (since := "2026-03-06")]

def CategoryTheory.Classifier.ofEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (𝒞₁ : Subobject.Classifier C) (e : C ≌ D) :

Subobject.Classifier D

Alias of CategoryTheory.Subobject.Classifier.ofEquivalence.

The image of a subobject classifier under an equivalence of categories is a subobject classifier.

Equations

@CategoryTheory.Classifier.ofEquivalence = @CategoryTheory.Subobject.Classifier.ofEquivalence

Instances For

Documentation

Mathlib.CategoryTheory.Subobject.Classifier.Defs

Subobject Classifier #

Main definitions #

Main results #

References #

The representability theorem of subobject classifiers #

From classifiers to representations #

From representations to classifiers #