Subobject Classifier

We define what it means for a morphism in a category to be a subobject classifier as CategoryTheory.HasClassifier.

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.Classifier C is the data of a subobject classifier in C.

• CategoryTheory.HasClassifier 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.

References

• [S. MacLane and I. Moerdijk, Sheaves in Geometry and Logic][MLM92]

TODO

• Exhibit the equivalence between having a classifier and the functor B => Subobject B being representable.

• Make API for constructing a subobject classifier without reference to limits (replacing ⊤_ C with an arbitrary Ω₀ : C and including the assumption mono truth)

structure CategoryTheory.Classifier (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] : Type (max u v)

A morphism truth : ⊤_ C ⟶ Ω from the terminal object of a category C is a subobject classifier if, for every monomorphism m : U ⟶ X in C, there is a unique map χ : X ⟶ Ω such that the following square is a pullback square:

      U ---------m----------> X
      |                       |
terminal.from U               χ
      |                       |
      v                       v
    ⊤_ C ------truth--------> Ω

An equivalent formulation replaces the object ⊤_ C with an arbitrary object, and instead includes the assumption that truth is a monomorphism.

• Ω : C

  The target of the truth morphism

• truth : ⊤_ C ⟶ self.Ω

  the truth morphism for a subobject classifier

• χ {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 (Limits.terminal.from U) (self.χ m) self.truth

  χ m forms the appropriate pullback square.

• uniq {U X : C} (m : U ⟶ X) [Mono m] (χ' : X ⟶ self.Ω) (hχ' : IsPullback m (Limits.terminal.from U) χ' self.truth) : χ' = self.χ m

  χ m is the only map X ⟶ Ω which forms the appropriate pullback square.

class CategoryTheory.HasClassifier (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] : Prop

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

• exists_classifier : Nonempty (Classifier C)

  There is some classifier.

@[reducible, inline]

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

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

Equations

• CategoryTheory.HasClassifier.Ω C = ⋯.some.Ω

@[reducible, inline]

abbrev CategoryTheory.HasClassifier.truth (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] : ⊤_ C ⟶ Ω C

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

Equations

• CategoryTheory.HasClassifier.truth C = ⋯.some.truth

def CategoryTheory.HasClassifier.χ {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier 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.HasClassifier.χ m = ⋯.some.χ m

theorem CategoryTheory.HasClassifier.isPullback_χ {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] {U X : C} (m : U ⟶ X) [Mono m] : IsPullback m (Limits.terminal.from U) (χ m) (truth C)

The diagram

      U ---------m----------> X
      |                       |
terminal.from U              χ m
      |                       |
      v                       v
    ⊤_ C -----truth C-------> Ω

is a pullback square.

theorem CategoryTheory.HasClassifier.comm {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] {U X : C} (m : U ⟶ X) [Mono m] : CategoryStruct.comp m (χ m) = CategoryStruct.comp (Limits.terminal.from U) (truth C)

The diagram

      U ---------m----------> X
      |                       |
terminal.from U              χ m
      |                       |
      v                       v
    ⊤_ C -----truth C-------> Ω

commutes.

theorem CategoryTheory.HasClassifier.comm_assoc {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] {U X : C} (m : U ⟶ X) [Mono m] {Z : C} (h : Ω C ⟶ Z) : CategoryStruct.comp m (CategoryStruct.comp (χ m) h) = CategoryStruct.comp (Limits.terminal.from U) (CategoryStruct.comp (truth C) h)

theorem CategoryTheory.HasClassifier.unique {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] {U X : C} (m : U ⟶ X) [Mono m] (χ' : X ⟶ Ω C) (hχ' : IsPullback m (Limits.terminal.from U) χ' (truth C)) : χ' = χ m

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

noncomputable instance CategoryTheory.HasClassifier.truthIsRegularMono {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] : RegularMono (truth C)

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

Equations

• CategoryTheory.HasClassifier.truthIsRegularMono = CategoryTheory.RegularMono.ofIsSplitMono (CategoryTheory.HasClassifier.truth C)

instance CategoryTheory.HasClassifier.isRegularMonoCategory {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier C] : IsRegularMonoCategory C

The following diagram

      U ---------m----------> X
      |                       |
terminal.from U              χ m
      |                       |
      v                       v
    ⊤_ C -----truth C-------> Ω

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.

instance CategoryTheory.HasClassifier.reflectsIsomorphisms {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier 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.

instance CategoryTheory.HasClassifier.reflectsIsomorphismsOp {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [HasClassifier 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.