Proper subsets

# Proper subsets

## Idea

A subset $A$ of a set $S$ is proper if it is not the improper subset of $S$ ($S$ as a subset of itself). We may also say (in the context of concrete sets) that $S$ is a proper superset of $A$ or that $S$ properly contains? $A$.

## Definition

### In material set theory

In material set theory, we may state that $A$ is proper in any of these equivalent ways:

1. $A$ is not equal (as a subset) to $S$;
2. There exists an element $x$ of $S$ such that $x \notin A$;
3. Given any way of expressing $A$ as the intersection of a family of subsets of $S$, this family is inhabited.

Actually, these three definitions are equivalent only if we accept the principle of excluded middle; in constructive mathematics, we usually prefer (3). (For example, consider the notion of proper filter on a set $X$, thought of as a subset of the power set of $X$.) However, (3) is not predicative; see positive element for discussion of this in the dual context. Also, (2) may be strengthened using an inequality relation other than the denial inequality.

### In structural set theory

In structural set theory, subsets are represented by injections, and so we may state that the injection $m:A \hookrightarrow S$ is proper in any of these equivalent ways:

1. The injection $m:A \hookrightarrow S$ is not an bijection;
2. There exists an element $x$ of $S$ such that for all elements $y \in A$, $m(x) \neq y$;
3. Given any way of expressing $m:A \hookrightarrow S$ as the intersection of a family of injections into $S$, this family is inhabited.

Similarly as the case in material set theory, these three definitions are equivalent only if we accept the principle of excluded middle.

### More generally

In any category $C$, subsets become subobjects and are thus represented by the monomorphisms in $C$. Then a proper subobject is defined in any of the following ways:

1. The monomorphism $m:A \hookrightarrow S$ is not an isomorphism;
2. If $C$ is a well-pointed category with terminal object $1$, then there exists a global element $x:1 \to S$ such that for all global elements $y:1 \to A$, $m \circ x \neq y$;
3. If the subobject preorder of every object in $C$ is a pre-inflattice, then given any way of expressing $m:A \hookrightarrow S$ as the intersection of a family of monomorphisms into $S$, this family is inhabited.