nLab quotient set

Redirected from "axiom of quotients".
Quotient sets

Quotient sets

Definitions

In set theory

Given a set SS and an equivalence relation \equiv on SS, the quotient set of SS by \equiv is the set S/S/{\equiv} whose elements are the elements of SS but where two elements are now considered equal if in SS they were merely equivalent.

If changing the definition of equality like this is not allowed in the given foundations of mathematics, then one can still define S/S/{\equiv} as a subset of the power set of SS.

  • In material set theory the definition is as follows:
    (1)AS/(x:S),A={y:Sxy} A \in S/{\equiv} \;\Leftrightarrow\; \exists (x: S),\; A = \{y: S \;\mid\; x \equiv y\}
  • In structural set theory the definition is slightly different, because sets are not elements of sets and one cannot in general compare sets for strict equality.

If there are also no (extensional) power sets in the foundations of mathematics, then there are two alternatives:

  • One could use setoids (in which case, perhaps one would do better to change your terminology as described there).
  • One could just include the existence of quotient objects in Set as an axiom (the axiom of quotient sets.

The latter is the case if one assumes that Set\Set is a pretopos or a Grothendieck topos as given by Giraud's axioms). There are actually two possible axiom of quotient sets, depending on what definition of relation one uses.

  • The weaker version of the axiom of quotient sets is the one which states that the coherent category SetSet is a pretopos: that every internal equivalence relation on a set AA, defined as a subset \equiv of the Cartesian product A×AA \times A satisfying reflexivity, transitivity, and symmetry, has a quotient set A/A/\equiv.

  • The stronger version of the axiom of quotient sets states that every proposition xyx \equiv y in the context of the variables xAx \in A and yAy \in A which satisfies reflexivity, transitivity, and symmetry has a quotient set A/A/\equiv. In some presentations of set theory, this is an axiom schema of quotient sets.

In any case, the element of S/S/{\equiv} that comes from the element xx of SS may be denoted [x] [x]_{\equiv}, or simply [x][x] if {\equiv} is understood, or simply xx if there will be no confusion as to which set it is an element of. This [x][x] is called the equivalence class of xx with respect to \equiv; the term ‘class’ here is an old word for ‘set’ (in the sense of ‘subset’) and refers to the definition (1) above, where [x][x] is literally the set AA.

As initial objects in a category

Let SS be a set and let \equiv be an equivalence relation on SS. Let us define a quotient set algebra of SS and \equiv to be a set AA with a function ιSA\iota S \to A such that for all aSa \in S and bSb \in S, (ab)(a \equiv b) implies (ι(a)=ι(b))(\iota(a) = \iota(b)).

A quotient set algebra homomorphism of SS and \equiv is a function f:ABf: A \to B between two quotient set algebras AA and BB such that for all aSa \in S, f(ι A(a))=ι B(a)f(\iota_A(a)) = \iota_B(a).

The category of quotient set algebras of SS and \equiv is the category QSA(S,)QSA(S, \equiv) whose objects Ob(QSA(S,))Ob(QSA(S, \equiv)) are quotient set algebras of SS and \equiv and whose morphisms Mor(A,B)Mor(A, B) for AOb(QSA(S,))A \in Ob(QSA(S, \equiv)) and BOb(QSA(S,))B \in Ob(QSA(S, \equiv)) are quotient set algebra homomorphisms of SS and \equiv. The quotient set of SS and \equiv, denoted S/S/\equiv, is defined as the initial object in the category of quotient set algebras of SS and \equiv.

In dependent type theory

Similar to set theory, there are multiple ways of defining quotient sets in dependent type theory. If the type theory has a univalent type of all propositions (Prop,El)(\mathrm{Prop}, \mathrm{El}) and thus power sets 𝒫TTProp\mathcal{P}T \coloneqq T \to \mathrm{Prop} of a type TT, then given a type TT with an equivalence relation ()():𝒫(T×T)(-)\equiv(-):\mathcal{P}(T \times T), one could construct the quotient set T/T/\equiv as a subtype of the power set, as follows: we first define the predicate on the powerset 𝒫T\mathcal{P}T:

P:𝒫TisEquivalenceClass(P)[ x:T y:TP(x)= Prop(xy)]P:\mathcal{P}T \vdash \mathrm{isEquivalenceClass}(P) \coloneqq \left[\sum_{x:T} \prod_{y:T} P(x) =_\mathrm{Prop} (x \equiv y) \right]

since by univalence there is an equivalence between the types P(x)= Prop(xy)P(x) =_\mathrm{Prop} (x \equiv y) and El(P(x))El(xy)\mathrm{El}(P(x)) \simeq \mathrm{El}(x \equiv y), which for propositions is the same as El(P(x))El(xy)\mathrm{El}(P(x)) \iff \mathrm{El}(x \equiv y). Then we define the subtype

T/ P:𝒫TisEquivalenceClass(P)T/\equiv \coloneqq \sum_{P:\mathcal{P}T} isEquivalenceClass(P)

Alternatively, if the dependent type theory does not have a type of all propositions, then the quotient set T/T/\equiv can still nevertheless be constructed. The analogue of the axiom of quotient sets in dependent type theory is the rules for the quotient set higher inductive type. In particular, the quotient set T/T/\equiv is a higher inductive type inductively generated by the following:

  • a function ι:TT/\iota: T \to T/\equiv

  • a family of dependent terms

    a:T,b:Teq T/(a,b):(ab)(ι(a)= T/ι(b)) a \colon T ,\; b \colon T \;\;\; \vdash \;\;\; eq_{T/\equiv}(a, b) \,\colon\, (a \equiv b) \;\to\; (\iota(a) =_{T/\equiv} \iota(b))
  • a family of dependent terms

    a:T/,b:T/τ(a,b):isProp(a= T/b)a:T/\equiv, b:T/\equiv \vdash \tau(a, b): isProp(a =_{T/\equiv} b)

In general, if one doesn’t have impredicative quotient sets or quotient sets as a higher inductive type, than one could only construct quotient sets of equivalence relations with a choice of unique representatives, which for equivalence relation R(x,y)R(x, y) indexed by x:Ax:A and y:Ay:A consists of a type family C(x)C(x) indexed by x:Ax:A, and an element of type

x:A!y:A.C(x)×R(x,y)\prod_{x:A} \exists!y:A.C(x) \times R(x, y)

Then the type x:AC(x)\sum_{x:A} C(x) is the quotient set of AA with respect to RR.

Equivalently, one could use functions instead of type families, and say that a choice of unique representatives is a type CC with a function f:CAf:C \to A and an element of type

x:A!y:A.( z:Cf(z)= Ax)×R(x,y)\prod_{x:A} \exists!y:A.\left(\sum_{z:C} f(z) =_A x\right) \times R(x, y)

Then

C x:A z:Cf(z)= AxC \simeq \sum_{x:A} \sum_{z:C} f(z) =_A x

is the quotient set of AA with respect to RR.

Generalisations

Quotient sets in Set generalise to quotient objects in other categories. In particular, an exact category is a regular category in which every congruence on every object has an effective quotient object.

See also

Rereferences

For quotient sets in dependent type theory, see:

See the references at quotient type.

Last revised on January 16, 2024 at 18:20:48. See the history of this page for a list of all contributions to it.