subobject

Tag. subobject

subobject

Notes (7)

Definition. Proper and maximal sieves proper-maximal-sieve

The representable $𝗒 𝑥$ is itself a sieve on $𝑥$ . A sieve on $𝑥$ is proper when it is not equal to the representable.

Say that a proper sieve is maximal when it contains all other proper sieves as a sub-sieve.

Definition. Sieves sieve

A sieve on an object $𝑥$ of $𝒞︀$ is a subobject of the representable presheaf $𝗒 𝑥$ : a presheaf $𝑆$ with a monic morphism $𝑆 ↣ 𝗒 𝑥$ . Sieves are a generalization from the notion of ideal found in ring theory to category theory.

A morphism $𝑓 : 𝑦 \to 𝑥$ belongs to $𝑆$ , written $𝑆 ∋ 𝑓$ , when $𝑓$ lies in the image of the inclusion at $𝑦$ . Because $𝑆$ is a presheaf and the inclusion is natural, membership is closed under precomposition:

𝑆 ∋ 𝑓 \Rightarrow 𝑆 ∋ 𝑔 ⋆ 𝑓 for every 𝑔 : 𝑧 \to 𝑦 .

A sieve is thus a “downward closed” collection of morphisms into $𝑥$ .

Sieves on $𝑥$ are ordered by refinement: $𝑆 \subseteq 𝑇$ when every morphism belonging to $𝑆$ belongs to $𝑇$ .

Theorem. Maximality of the strict downset among proper sieves strict-downset-maximal

Call a direct structure reflecting when every morphism between objects of equal degree is a split epimorphism. In a reflecting direct category, every non-invertible-in-degree morphism strictly raises degree, and the strict downset is as large as a proper sieve can be:

If the direct structure is reflecting, then every proper sieve $𝑆$ on $𝑥$ refines into the strict downset:

𝑆 \subseteq 𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) .

Suppose $𝑓 \in 𝑆$ with $𝑓 : 𝑦 \to 𝑥$ of equal degree. By reflection $𝑓$ has a section $𝑠$ , and closure under precomposition gives $𝑠 ⋆ 𝑓 = {𝗂𝖽}_{𝑥} \in 𝑆$ , contradicting properness.

So every morphism in $𝑆$ strictly raises degree. That is, every morphism in $𝑆$ is also a member of $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥)$ .

Definition. The strict downset sieve of a direct category strict-downset-sieve

Let $𝒞︀$ carry a direct structure. The strict downset $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥)$ of an object $𝑥$ is the presheaf of morphisms into $𝑥$ from strictly lower objects:

𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) (𝑦) = {𝑓 : 𝑦 \to 𝑥 ∣ 𝑦 ≺ 𝑥},

with restriction by precomposition — well defined since degrees are non-decreasing, so precomposing can only stay strictly below.

The evident inclusion $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥) ↣ よ 𝑥$ makes $𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇 (𝑥)$ a sieve on $𝑥$ . It is moreover a proper sieve, as it exlcudes the identity.

Definition. Subobject subobject

In a category $𝒞︀$ , a subobject of $𝑐$ is an isomorphism class of monomorphisms into $𝑐$ .

Definition. Subobject Classifier subobject-classifier

Subsets $𝐴$ of a set $𝑋$ may classically be identified with a characteristic map $𝜒_{𝐴} : 𝑋 \to 𝖻𝗈𝗈𝗅$ . Intuitively, for every $𝑥 : 𝑋$ , $𝜒_{𝐴}$ gives a truth value to the statement “ $𝑥$ is in the subset $𝐴$ ”. In this manner, the domain of the characteristic map, $𝖻𝗈𝗈𝗅$ , classifies the subsets of $𝑋$ .

Generalizing over this principle, in a category $𝒞︀$ an object $Ω$ is a subobject classifier if maps into it from some object $𝑐$ likewise uniquely identify a subobject of $𝑐$ .

We can understand $Ω$ to behave like an object of truth values that are not necessarily boolean valued. A morphism $𝑝 : 𝑐 \to Ω$ can be thought of like a predicate on $𝑐$ . If $𝑐$ were a set, this would precisely be the characteristic function on it. However, this idea can generalize beyond sets. For instance in the category of graphs, $Ω$ is a cleverly constructed graph such that any graph homomorphism $𝑔 \to Ω$ into it picks out a unique subgraph of $𝑔$ .

There are always two (suggestively named) disjoint “points” of $Ω$ , thought of as morphisms out of the terminal object $𝗍𝗋𝗎𝖾, 𝖿𝖺𝗅𝗌𝖾 : ⊤ \to Ω$ . I think if we’re being careful, $𝗍𝗋𝗎𝖾$ may properly be the “subobject classifier” but I always use the term to refer to $Ω$ itself.

A subobject $𝜙 : 𝑑 ↪ 𝑐$ induces a unique characteristic morphism $𝑝_{𝜙} : 𝑐 \to Ω$ such that

𝑝_{𝜙} \circ 𝜙 = 𝗍𝗋𝗎𝖾 \circ!_{𝑑}

Moreover, the appropriate square must be a pullback.

Subobject Classifier in Dependent Lambek Calculus subobject-classifier-for-grammars

Previously in Agda we had constructed equalizers in Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using sigma types. Further, equalizers form subobjects, which may be comprehended as maps from a type into a subobject classifier.

I believe in our formalization we want to generalize this idea to a broader class of subobjects, maybe even all of them. That is, we could define a subobject classifying grammar $Ω$ . Then we can internally define any predicate on a grammar $𝑔$ via a term $𝑝 : 𝑔 ⊢ Ω$ .

That is, forall $𝑤 : String$ we have $⟦ Ω ⟧ (𝑤) ≔ 𝗁𝖯𝗋𝗈𝗉$ , and

⟦ 𝗌𝗎𝖻𝗀𝗋𝖺𝗆𝗆𝖺𝗋 (𝑔) (𝑝) ⟧ (𝑤) ≔ \sum_{𝑥 : ⟦ 𝑔 ⟧ (𝑤)} ⟦ 𝑝 ⟧ (𝑥)

The code for this is nearly identical to the definition of equalizers as sigma types, and I have even built a translation of the equalizers code that is defined with this as its foundation. I have not yet tested if either implementation is preferable.

It isn’t yet clear how to best expose this sort of construct syntactically. I suppose you could assume some subobject classifying grammar, but then I don’t know if you can then reap the benefits of the propositions internally. That is, how do you reflect the proposition that two terms are equal in the internal language of propositions rather than the external one?

If nothing else, this code gives me a reusable interface to axiomatize smaller, sandboxed ways in which I’d like to internalize certain types of propositions (such as “two terms are equal” or “does not begin with the character $𝑐$ ”).

The hope for this code is that it lets me inductively prove the follow last soundness of Kleene star.