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 [MLM92]).

References

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

TODO

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

The representability theorem of subobject classifiers

From classifiers to representations

theorem CategoryTheory.Classifier.surjective_χ {C : Type u} [Category.{v, u} C] [Limits.HasTerminal 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.HasTerminal C] [Limits.HasPullbacks C] (𝒞 : Classifier C) {Z X : C} (i : Z ⟶ X) [Mono i] : (Subobject.pullback (𝒞.χ i)).obj (Subobject.mk 𝒞.truth) = Subobject.mk i

@[simp]

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

noncomputable def CategoryTheory.Classifier.representableBy {C : Type u} [Category.{v, u} C] [Limits.HasTerminal 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.

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 Ω.

Equations

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

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 Ω.

Equations

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

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.

Equations

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

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.

Equations

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

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---> Ω

Equations

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

@[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.

Equations

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

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.

Equations

• h.isoΩ₀ = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso h.isTerminalΩ₀ (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.empty 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 Ω.

Equations

• h.classifier = { Ω := Ω, truth := CategoryTheory.CategoryStruct.comp h.isoΩ₀.inv h.Ω₀.arrow, χ := fun {U X : C} (m : U ⟶ X) (x : CategoryTheory.Mono m) => h.χ m, isPullback := ⋯, uniq := ⋯ }

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.