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.

• CategoryTheory.Classifier.representableBy: any subobject classifier Ω in C represents the subobjects functor CategoryTheory.Subobject.presheaf C.

• CategoryTheory.Classifier.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 has a subobject classifier if and only if the subobjects presheaf CategoryTheory.Subobject.presheaf C is representable (Proposition 1 in Section I.3 of [MM92]).

References

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

structure CategoryTheory.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 χ₀'.

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) : Classifier C

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

@[simp]

theorem CategoryTheory.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

@[simp]

theorem 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) : (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω = Ω

@[simp]

theorem 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) (Y : C) : (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ₀ Y = t.from Y

@[simp]

theorem 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) : (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω₀ = Ω₀

@[simp]

theorem 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) {U✝ X✝ : C} (m : U✝ ⟶ X✝) (x✝ : Mono m) : (mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ m = χ m

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

def CategoryTheory.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.

@[simp]

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

class CategoryTheory.HasClassifier (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 (Classifier C)

  There is some classifier.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

theorem CategoryTheory.HasClassifier.isPullback_χ {C : Type u} [Category.{v, u} C] [HasClassifier 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.

theorem CategoryTheory.HasClassifier.comm {C : Type u} [Category.{v, u} C] [HasClassifier 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.

theorem CategoryTheory.HasClassifier.comm_assoc {C : Type u} [Category.{v, u} 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 (⋯.some.χ₀ U) (CategoryStruct.comp (truth C) h)

theorem CategoryTheory.HasClassifier.unique {C : Type u} [Category.{v, u} C] [HasClassifier 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.

instance CategoryTheory.HasClassifier.truthIsSplitMono {C : Type u} [Category.{v, u} C] [HasClassifier C] : IsSplitMono (truth C)

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

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

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

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

The representability theorem of subobject classifiers

From classifiers to representations

@[reducible, inline]

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

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

theorem CategoryTheory.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

@[simp]

theorem CategoryTheory.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] : (Subobject.pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = Subobject.mk i

@[simp]

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

noncomputable def CategoryTheory.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.

From representations to classifiers

@[reducible, inline]

abbrev CategoryTheory.Classifier.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 Ω.

def CategoryTheory.Classifier.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 Ω.

theorem CategoryTheory.Classifier.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.

theorem CategoryTheory.Classifier.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.

def CategoryTheory.Classifier.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.

noncomputable def CategoryTheory.Classifier.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.

noncomputable def CategoryTheory.Classifier.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---> Ω

@[simp]

theorem CategoryTheory.Classifier.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.left (h.π m) = Subobject.pullbackπ (h.χ m) h.Ω₀

@[simp]

theorem CategoryTheory.Classifier.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.left (CategoryStruct.comp (h.π m) h✝) = CategoryStruct.comp (Subobject.pullbackπ (h.χ m) h.Ω₀) h✝

@[simp]

theorem CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_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.left m = ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow

@[simp]

theorem CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_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.left (CategoryStruct.comp m h✝) = CategoryStruct.comp ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow h✝

theorem CategoryTheory.Classifier.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

theorem CategoryTheory.Classifier.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

noncomputable def CategoryTheory.Classifier.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.

noncomputable def CategoryTheory.Classifier.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.

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

noncomputable def CategoryTheory.Classifier.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.

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

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

theorem CategoryTheory.isRepresentable_hasClassifier_iff {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] : HasClassifier C ↔ (Subobject.presheaf C).IsRepresentable

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