nLab proper subset

Proper subsets

Proper subsets

Idea

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

Definition

In material set theory

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

  1. AA is not equal (as a subset) to SS;
  2. There exists an element xx of SS such that xAx \notin A;
  3. Given any way of expressing AA as the intersection of a family of subsets of SS, 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 XX, thought of as a subset of the power set of XX.) 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:ASm:A \hookrightarrow S is proper in any of these equivalent ways:

  1. The injection m:ASm:A \hookrightarrow S is not an bijection;
  2. There exists an element xx of SS such that for all elements yAy \in A, m(x)ym(x) \neq y;
  3. Given any way of expressing m:ASm:A \hookrightarrow S as the intersection of a family of injections into SS, 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 CC, subsets become subobjects and are thus represented by the monomorphisms in CC. Then a proper subobject is defined in any of the following ways:

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

See also

Last revised on November 13, 2022 at 03:17:54. See the history of this page for a list of all contributions to it.