Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
Given a set and an equivalence relation on , the quotient set of by is the set whose elements are the elements of but where two elements are now considered equal if in 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 as a subset of the power set of .
If there are also no (extensional) power sets in the foundations of mathematics, then there are two alternatives:
The latter is the case if one assumes that 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 is a pretopos: that every internal equivalence relation on a set , defined as a subset of the Cartesian product satisfying reflexivity, transitivity, and symmetry, has a quotient set .
The stronger version of the axiom of quotient sets states that every proposition in the context of the variables and which satisfies reflexivity, transitivity, and symmetry has a quotient set . In some presentations of set theory, this is an axiom schema of quotient sets.
In any case, the element of that comes from the element of may be denoted , or simply if is understood, or simply if there will be no confusion as to which set it is an element of. This is called the equivalence class of with respect to ; the term ‘class’ here is an old word for ‘set’ (in the sense of ‘subset’) and refers to the definition (1) above, where is literally the set .
Let be a set and let be an equivalence relation on . Let us define a quotient set algebra of and to be a set with a function such that for all and , implies .
A quotient set algebra homomorphism of and is a function between two quotient set algebras and such that for all , .
The category of quotient set algebras of and is the category whose objects are quotient set algebras of and and whose morphisms for and are quotient set algebra homomorphisms of and . The quotient set of and , denoted , is defined as the initial object in the category of quotient set algebras of and .
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 and thus power sets of a type , then given a type with an equivalence relation , one could construct the quotient set as a subtype of the power set, as follows: we first define the predicate on the powerset :
since by univalence there is an equivalence between the types and , which for propositions is the same as . Then we define the subtype
Alternatively, if the dependent type theory does not have a type of all propositions, then the quotient set 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 is a higher inductive type inductively generated by the following:
a function
a family of dependent terms
a family of dependent terms
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 indexed by and consists of a type family indexed by , and an element of type
Then the type is the quotient set of with respect to .
Equivalently, one could use functions instead of type families, and say that a choice of unique representatives is a type with a function and an element of type
Then
is the quotient set of with respect to .
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.
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.