The quotient object of a congruence (an internal equivalence relation) on an object in a category is the coequalizer of the induced pair of morphisms .
If is additionally the kernel pair of the map , then is called an effective quotient – and is called an effective congruence, with the map being an effective epimorphism (terminology as for effective group action).
Sometimes the term is used more loosely to mean an arbitrary coequalizer. It may also refer to a co-subobject of (that is, a subobject of in the opposite category ), without reference to any congruence on . Note that in a regular category, any regular epimorphism (i.e. a “regular quotient” in the co-subobject sense) is in fact the quotient (= coequalizer) of its kernel pair (actually, we can prove this under weaker hypotheses; see below).
As we have said, there are various notions of quotient object. Let us consider the most general one, so that of an object denotes the poset of co-subobjects of , in other words the posetal reflection of the preorder of epis which is a full subcategory of the co-slice category . A regular quotient then refers to a regular epi .
On the other hand, let be the poset of relations on , i.e., the poset of subobjects of , or in other words the posetal reflection of the preorder of monos which is a full subcategory of the slice category .
Between and there is a relation where means exactly . If the coequalizer of the parallel pair exists, then by definition we have iff . On the other hand, if the kernel pair of exists, then by definition we have iff .
This indicates in a category which admits coequalizers and kernel pairs, we have
is left adjoint to .
Or, in other words, that and set up a Galois connection between and .
Restricting consideration to kernel pairs only of epis, or coequalizers only of jointly monic pairs, is no real restriction in the presence of epi-mono factorizations:
In a category where every morphism has an epi-mono factorization , we have . Similarly, for a pair , we have where factors as an epi followed by a mono .
We prove just the first statement; the second is proven similarly. It suffices to observe that the same class of jointly monic pairs are coequalized by as by ; the kernel pair is by definition the maximum of this class. If , then by applying to both sides we deduce . If , i.e., if , then by monicity of .
Suppose is a category with coequalizers and kernel pairs and where every morphism has an epi-mono factorization. Then every regular epi is the coequalizer of its kernel pair: . And every kernel pair is the kernel pair of its coequalizer: .
We just prove the first statement; the second is proved similarly. We have of course a counit . On the other hand, if (where we may assume is monic by the lemma), then we have a unit ; applying to each side, we have , as desired.
Constructing quotient objects in an elementary topos , starting from one or another standard definition (e.g., finitely complete category with power objects) that doesn’t already mention colimits, is not trivial.
The standard approach seen in textbooks (see for example Sheaves in Geometry and Logic), apparently first introduced by C.J. Mikkelsen but first published by Paré, is to prove that the contravariant power object functor is monadic. It follows that reflects finite limits in from limits in , but finite limits in are of course finite colimits in .
This elegant approach does involve a fair amount of categorical machinery (a monadicity theorem, Beck-Chevalley conditions, and consideration of up to six applications of the power object functor), making it a challenge to get across intuitively in say an undergraduate course.
Other approaches that are closer to naive or common sense set-theoretic reasoning are possible. In the case of quotient objects, to form the coequalizer of a parallel pair , we outline a possible path to take (see also at quotient type – from univalence):
Construct enough of the internal logic to make available logical operators .
Construct an internal intersection operator via the formula .
Construct the image of a map by taking the internal intersection of all subobjects of through which factors.
To construct the coequalizer of :
Notice that what these steps collectively do is form the object of equivalence classes of the equivalence relation generated by the relation , which is exactly what we would do in ordinary set theory. Full details will appear elsewhere.
These notions have generalizations when is an (∞,1)-category:
an equivalence relation is then a groupoid object in an (∞,1)-category
it has an “effective quotient” if it is deloopable.
For instance an action groupoid is a quotient of a group action in 2-category theory.
In type theory/homotopy type theory the analogous concept is that of quotient types.
Last revised on May 26, 2022 at 14:00:21. See the history of this page for a list of all contributions to it.