module Cat.Diagram.Subobject where

Subobject classifiers🔗

In an arbitrary category $\mathcal{C}\text{,}$ a subobject of $X$ is, colloquially speaking, given by a monomorphism $m:A\hookrightarrow X\text{.}$ Formally, though, we must consider the object $A$ to be part of this data, since we can only speak of morphisms if we already know their domain and codomain. The generality in the definition means that the notion of subobject applies to completely arbitrary $\mathcal{C}\text{,}$ but in completely arbitrary situations, the notion might be very badly behaved.

There are several observations we can make about $\mathcal{C}$ that “tame” the behaviour of ${\mathrm{Sub}}_{\mathcal{C}}(X)\text{.}$ For example, if it has pullbacks, then $\mathrm{Sub}(-)$ is a fibration, so that there is a universal way of re-indexing a subobject $x:\mathrm{Sub}(X)$ along a morphism $f:Y\to X\text{,}$ and if it has images, it’s even a bifibration, so that each of these reindexings has a left adjoint, giving an interpretation of existential quantifiers. If $\mathcal{C}$ is a regular category, existential quantifiers and substitution commute, restricting the behaviour of subobjects even further.

However, there is one assumption we can make about $\mathcal{C}$ that rules them all: it has a generic subobject, so that $\mathrm{Sub}(X)$ is equivalent to a given $\mathbf{Hom}\text{-set}$ in $\mathcal{C}\text{.}$ A generic subobject is a morphism $\top :\Omega \ast \to \Omega$ so that, for any a subobject $m:A\hookrightarrow X\text{,}$ there is a unique arrow $┌m┐$ making the square

into a pullback. We can investigate this definition by instantiating it in $\mathbf{Sets}\text{,}$ which does have a generic subobject. Given an embedding $m:A\hookrightarrow X\text{,}$ we have a family of propositions $┌m┐:X\to \Omega$ which maps $x:X$ to $m^{\ast }(x)\text{,}$ the fibre of $m$ over $x\text{.}$ The square above also computes a fibre, this time of $┌m┐\text{,}$ and saying that it is $m$ means that $┌m┐$ assigns $\top$ to precisely those $x:X$ which are in $m\text{.}$

  record is-generic-subobject {Ω} (true : Subobject Ω) : Type (o ⊔ ℓ) where
    field
      name : ∀ {X} (m : Subobject X) → Hom X Ω
      classifies
        : ∀ {X} (m : Subobject X)
        → is-pullback-along C (m .map) (name m) (true .map)
      unique
        : ∀ {X} {m : Subobject X} {nm : Hom X Ω}
        → is-pullback-along C (m .map) nm (true .map)
        → nm ≡ name m

  record Subobject-classifier : Type (o ⊔ ℓ) where
    field
      {Ω}     : Ob
      true    : Subobject Ω
      generic : is-generic-subobject true
    open is-generic-subobject generic public

While the definition of is-generic-subobject can be stated without assuming that $\mathcal{C}$ has any limits at all, we’ll need to assume that $\mathcal{C}$ has pullbacks to get anything of value done. Before we get started, however, we’ll prove a helper theorem that serves as a “smart constructor” for Subobject-classifier, simplifying the verification of the universal property in case $\mathcal{C}$ is univalent and has all finite limits (in particular, a terminal object).

Assuming that we have a terminal object, we no longer need to specify the arrow $\mathtt{true}$ as an arbitrary element of $\mathrm{Sub}(\Omega )$ — we can instead ask for a point $\mathtt{true}:\top \to \Omega$ instead. Since we have pullbacks, we also have the change-of-base operation $f^{\ast }(-):\mathrm{Sub}(B)\to \mathrm{Sub}(A)$ for any $f:A\to B\text{,}$ which allows us to simplify the condition that “$m$ is the pullback of $n$ along $f$”, which requires constructing a pullback square, to the simpler $m\cong f^{\ast }n\text{.}$ The theorem is that it suffices to ask for:

• The point $\mathtt{true}:\top \to \Omega$ corresponding to the generic subobject,
• An operation $┌-┐:\mathrm{Sub}(A)\to \mathbf{Hom}(A,\Omega )$ which maps subobjects to their names,
• A witness that, for any $m:\mathrm{Sub}(A)\text{,}$ we have $m\cong ┌m{┐}^{\ast }\mathtt{true}\text{,}$ and
• A witness that, for any $h:\mathbf{Hom}(A,\Omega )\text{,}$ we have $h=┌h^{\ast }\mathtt{true}┐\text{.}$

These two conditions amount to saying that $┌-┐$ and $(-{)}^{\ast }\top$ form an equivalence between the sets $\mathrm{Sub}(A)$ and $\mathbf{Hom}(A,\Omega )\text{,}$ for all $A\text{.}$ Note that we do not need to assume naturality for $┌-┐$ since it is an inverse equivalence to $(-{)}^{\ast }\mathtt{true}\text{,}$ which is already natural.

  from-classification
    : ∀ {Ω} (true : Hom top Ω)
    → (name : ∀ {A} (m : Subobject A) → Hom A Ω)
    → (∀ {A} (m : Subobject A) → m ≅ₘ name m ^* pt true)
    → (∀ {A} (h : Hom A Ω) → name (h ^* pt true) ≡ h)
    → Subobject-classifier C
  from-classification tru nm invl invr = done where
    done : Subobject-classifier C
    done .Ω = _
    done .true = pt tru
    done .generic .name = nm
    done .generic .classifies m = iso→is-pullback-along {m = m} {n = pt tru} (invl m)

Note that the uniqueness part of the universal property is satisfied by the last constraint on $┌-┐\text{:}$ the is-pullback-along assumption amounts to saying that $m\equiv h^{\prime \ast }\mathtt{true}\text{,}$ by univalence of $\mathrm{Sub}(A)\text{;}$ so we have $$┌m┐=┌h^{\prime \ast }\mathtt{true}┐=h^{\prime }\text{.}$$

    done .generic .unique {m = m} {h'} p =
      let
        rem₁ : m ≡ h' ^* pt tru
        rem₁ = Sub-is-category cat .to-path $
          is-pullback-along→iso {m = m} {n = pt tru} p
      in sym (ap nm rem₁ ∙ invr _)

The prototypical category with a subobject classifier is the category of sets. Since it is finitely complete and univalent, our helper above will let us swiftly dispatch the construction. Our subobject classifier is given by the type of propositions, $\Omega \text{,}$ lifted to the right universe. The name of a subobject $m:\mathrm{Sub}(A)$ is the family of propositions $x\mapsto m^{\ast }(x)\text{.}$ Note that we must squash this fibre down so it fits in $\Omega \text{,}$ but this squashing is benign because $m$ is a monomorphism (hence, an embedding).

  unbox : ∀ {A : Set ℓ} (m : Subobject A) {x} → □ (fibre (m .map) x) → fibre (m .map) x
  unbox m = □-out (monic→is-embedding (hlevel 2) (λ {C} g h p → m .monic {C} g h p) _)

  mk : make-subobject-classifier _ _
  mk .make-subobject-classifier.Ω = el! (Lift _ Ω)
  mk .true _ = lift ⊤Ω
  mk .name m x = lift (elΩ (fibre (m .map) x))

Showing that this name function actually works takes a bit of fiddling, but it’s nothing outrageous.

  mk .named-name m = Sub-antisym
    record
      { map = λ w → m .map w , lift tt , ap lift (to-is-true (inc (w , refl)))
      ; sq  = refl
      }
    record { sq = ext λ x _ p → sym (unbox m (from-is-true p) .snd )}
  mk .name-named h = ext λ a → Ω-ua
    (rec! λ x _ p y=a → from-is-true (ap h (sym y=a) ∙ p))
    (λ ha → inc ((a , lift tt , ap lift (to-is-true ha)) , refl))