Metamath Proof Explorer


Table of Contents - 8.3.3. The category of extensible structures

The "category of extensible structures" is the category of all sets in a universe regarded as extensible structures and the functions between their base sets, see df-estrc.

Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are all sets in a universe , which can be an arbitrary set, see estrcbas. Generally, we will take to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv we do not need to restrict the universe to sets which "have a base". The morphisms (or arrows) between two objects, i.e. sets from the universe, are the mappings between their base sets, see estrchomfval, whereas the composition is the ordinary composition of functions, see estrccofval and estrcco.

It is shown that the category of extensible structures is actually a category, see estrccat with the identity function as identity arrow, see estrcid.

In the following, some background information about the category of extensible structures is given, taken from the discussion in Github issue #1507 (see https://github.com/metamath/set.mm/issues/1507):

At the beginning, the categories of non-unital rings and unital rings were defined separately (as unordered triples of ordereds pairs, see dfrngc2 and dfringc2, but with special compositions). With this definitions, however, theorem rngcresringcat could not be proven, because the compositions were not compatible. Unfortunately, no precise definition of the composition within the category of rings could be found in the literature. In section 3.3 EXAMPLES, paragraph (2) of [Adamek] p. 22, however, a definition is given for "Grp", the category of groups: "The following constructs; i.e., categories of structured sets and structure-preserving functions between them (o will always be the composition of functions and idA will always be the identity function on A): ... (b) Grp with objects all groups and morphisms all homomorphisms between them." Therefore, the compositions should have been harmonized by using the composition of the category of sets , see df-setc, which is the ordinary composition of functions. Analogously, categories of Rngs (and Rings) could have been shown to be restrictions resp. subcategories of the category of sets.

BJ and MC observed, however, that "... [cannot be used] to restrict the category Set to Ring, because the homs are different. Although Ring is a concrete category, a hom between rings R and S is a function (Base`R) --> (Base`S) with certain properties, unlike in Set where it is a function R --> S.". Therefore, MC suggested that "we could have an alternative version of the Set category consisting of extensible structures (in U) together with (A Hom B) := (Base`A) --> (Base`B). This category is not isomorphic to Set because different extensible structures can have the same base set, but it is equivalent to Set; the relevant functors are (U`A) = (Base`A), the forgetful functor, and (F`A) = { <. (Base`ndx), A >. }". This led to the current definition of , see df-estrc. The claimed equivalence is proven by equivestrcsetc. Having a definition of a category of extensible structures, the categories of non-unital and unital rings can be defined as appropriate restrictions of the category of extensible structures, see df-rngc and df-ringc.

In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat, although the morphisms of the shown categories are different ( "->" means "is subcategory of"):

-> -> GrpCat -> MndCat -> MgmCat ->

According to MC, "If we generalize from subcategories to embeddings, then we can even fit into the chain, equivalent to at the end." As mentioned before, the equivalence of and is proven by equivestrcsetc. Furthermore, it can be shown that is embedded into , see embedsetcestrc.

Remark: equivestrcsetc as well as embedsetcestrc require that the index of the base set extractor is contained within the considered universe. This is ensured by assuming that the natural numbers are contained within the considered universe: (see wunndx), but it would be currently sufficient to assume that , because the index value of the base set extractor is hard-coded as , see basendx.

Some people, however, feel uncomfortable to say that a ring "is a" group (without mentioning the restriction to the addition, which is usually found in the literature, e.g. the definition of a ring in [Herstein] p. 126: "... Note that so far all we have said is that R is an abelian group under +.". The main argument against a ring being a group is the number of components/slots: usually, a group consists of (exactly!) two components (a base set and an operation), whereas a ring consists of (exactly!) three components (a base set and two operations). According to this "definition", a ring cannot be a group.

This is also an (unfortunately informal) argument for the category of rings not being a subcategory of the category of abelian groups in "Categories and Functors", Bodo Pareigis, Academic Press, New York, London, 1970: "A category A is called a subcategory of a category B if Ob(A) Ob(B) and MorA(X,Y) MorB(X,Y) for all X,Y e. Ob(A), if the composition of morphisms in A coincides with the composition of the same morphisms in B and if the identity of an object in A is also the identity of the same object viewed as an object in B. Then there is a forgetful functor from A to B. We note that Ri [the category of rings] is not a subcategory of Ab [the category of abelian groups]. In fact, Ob(Ri) Ob(Ab) is not true, although every ring can also be regarded as an abelian group. The corresponding abelian groups of two rings may coincide even if the rings do not coincide. The multiplication may be defined differently.".

As long as we define Rings, Groups, etc. in a way that is valid (see ringgrp) the corresponding categories are in a subcategory relation. If we do not want Rings to be Groups (then the category of rings would not be a subcategory of the category of groups, as observed by Pareigis), we would have to change the definitions of Magmas, Monoids, Groups, Rings etc. to restrict them to have exactly the required number of slots, so that the following holds

  1. fncnvimaeqv
  2. bascnvimaeqv
  3. cestrc
  4. df-estrc
  5. estrcval
  6. estrcbas
  7. estrchomfval
  8. estrchom
  9. elestrchom
  10. estrccofval
  11. estrcco
  12. estrcbasbas
  13. estrccatid
  14. estrccat
  15. estrcid
  16. estrchomfn
  17. estrchomfeqhom
  18. estrreslem1
  19. estrreslem2
  20. estrres
  21. funcestrcsetclem1
  22. funcestrcsetclem2
  23. funcestrcsetclem3
  24. funcestrcsetclem4
  25. funcestrcsetclem5
  26. funcestrcsetclem6
  27. funcestrcsetclem7
  28. funcestrcsetclem8
  29. funcestrcsetclem9
  30. funcestrcsetc
  31. fthestrcsetc
  32. fullestrcsetc
  33. equivestrcsetc
  34. setc1strwun
  35. funcsetcestrclem1
  36. funcsetcestrclem2
  37. funcsetcestrclem3
  38. embedsetcestrclem
  39. funcsetcestrclem4
  40. funcsetcestrclem5
  41. funcsetcestrclem6
  42. funcsetcestrclem7
  43. funcsetcestrclem8
  44. funcsetcestrclem9
  45. funcsetcestrc
  46. fthsetcestrc
  47. fullsetcestrc
  48. embedsetcestrc