Subset

Let $𝐴, 𝐵$ be sets. A subset $𝐴 \subseteq 𝐵$ is a set whose elements are all elements of $𝐵$ , #m/def/set i.e.

𝐴 \subseteq 𝐵 d e f ⟺ (\forall 𝑥) [𝑥 \in 𝐴 ⟹ 𝑥 \in 𝐵]

A proper subset is is a subset that is not equal to its superset, i.e.

𝐴 ⊊ 𝐵 d e f ⟺ [𝐴 \subseteq 𝐵 \land 𝐴 \neq 𝐵]

Universal property

Adopting a structuralist perspective, let $𝑝 : 𝐵 \to Ω$ denote the membership predicate so that $𝑝 (𝑎) = t t ⟺ 𝑎 \in 𝐴$ . A subset $𝐴$ along with its natural inclusion $𝜄 : 𝐴 ↪ 𝐵$ is characterized up to unique bijection by the following universal property:

$𝑝 𝜄 = t t!$ . If $𝐶$ is a set and $𝑓 : 𝐶 \to 𝐵$ is a function such that $𝑝 𝑓 = t t$ , then there exists a unique function $¯ 𝑓 : 𝐶 \to 𝐴$ such that $𝜄 ¯ 𝑓 = 𝑓$ , i.e.

Proof

Clearly $𝑝 𝜄 = t t!$ by construction. If $𝑝 𝑓 = t t!$ , then $i m 𝑓 \subseteq 𝐴$ so we can take $¯ 𝑓 (𝑐) = 𝑓 (𝑐)$ .

This may be rephrased as a fibre product for a more general Subobject via a Subobject classifier, generalizing this construction to an arbitrary Elementary topos as well as some other categories.

#state/tidy | #lang/en | #SemBr