Closed avekens closed 4 years ago
In that case, could you not define RngCat and RingCat as the category restriction (|'cat
) of the Set category to the (non-unital) Rings?
It seems ~df-resc
does exactly that.
df-rngc $a |- RngCat = ( u e. _V |-> ( ( SetCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) )
df-ringc $a |- RingCat = ( u e. _V |-> ( ( SetCat ` u ) |`cat ( RingHomo |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) )
That restriction operation does not change the compositions, but only the morphisms and the base set.
In that case, could you not define RngCat and RingCat as the category restriction (
|'cat
) of the Set category to the (non-unital) Rings? It seems~df-resc
does exactly that.df-rngc $a |- RngCat = ( u e. _V |-> ( ( SetCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) df-ringc $a |- RingCat = ( u e. _V |-> ( ( SetCat ` u ) |`cat ( RingHomo |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) )
That restriction operation does not change the compositions, but only the morphisms and the base set.
@tirix : In principle I planned exactly this, but your approach is more elegant. And it will safe some overhead/auxiliary theorems because general theorems about category restrictions can be used. I'll follow your suggestion.
I haven't checked the codings, but if, in metamath parlance, one can say that the category of rings is a subcategory / restriction of the category of sets, then, somewhere, something went horribly wrong.
As I repeated too often, I am not fond of extensible structures, and I think that this provides yet another reason. Apparently, one could consider RingCat a subcategory of SetCat because rings (resp. ring morphisms) are particular cases of sets (resp. functions), because they rings are extensible structures, that is, functions from a subset of \N such that [...], hence particular sets ? Is that correct, @digama0 ? It looks very artificial. Does it really work for morphism composition ??
By the way, the treatment of subcategories by @avekens would be simpler if the base set of a category were its set of morphisms (see https://groups.google.com/d/topic/metamath/BVfiiSv-1R0/discussion).
I believe @benjub is correct - you cannot use |`cat
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
.
According to @tirix , my proposed definition from yesterday is equivalent to his definition (I think I can show this formally very soon), because "That restriction operation does not change the compositions, but only the morphisms and the base set": All involved categories are unordered triples of ordered pairs (slots), where the third slot "comp" is identical, but the others ("Base", "Hom") are not. As @benjub correctly observed ("rings (resp. ring morphisms) are particular cases of sets (resp. functions)", the composition of SetCat also works for the Ring/Rng homomorphisms. Of course the homs are different, but they are replaced entirly by the |`cat operation. The only requirement on the homs is that they must be a subset of functions, which is apparently the case. Furthermore, the objects (base set) and the homs are identical with the objects and homs of the current definition df-rngc/df-ringc in set.mm (my mathbox), only the composition will be changed (according to the statement about the category of groups in the book I referenced above). Therefore, the discussion should be concentrated on the decision which composition is appropriate.
I would propose that I provide the alternate definitions and some related theorems and put them into my mathbox. Then these results can be compared and may make a decision easier.
The restriction operation changes the homs and the base, yes, but only by restriction, as the name implies. It cannot create homs that were not originally in the category. Because rings are sets (extensible structures), the objects are in the category, but the hom set for them in Set is functions R --> S
which is nonsense because R
and S
are extensible structures. In particular, the subset of this set which are also ring homs from R
to S
are functions that are both R --> S
and (Base`R) --> (Base`S)
, which is usually the empty set. So you won't get a category, and the typing has plainly gone off the rails.
Alternatively, 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 is the definition of |'cat
:
$( Define the restriction of a category to a given set of arrows.
(Contributed by Mario Carneiro, 4-Jan-2017.) $)
df-resc $a |- |`cat = ( c e. _V , h e. _V |->
( ( c |`s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) ) $.
The Hom
field is overwritten, not restricted.
The Base
field is restricted to dom dom h
. In the case of the proposal, h
is ( RingHomo |' ( ( u i^i Ring ) X. ( u i^i Ring ) ) )
, so dom dom h
is ( u i^i Ring )
, which I believe is the intended "base".
Of course this only works because we are using ZFC and everything is sets, including (ring) structures...
I'm afraid that Benoît and Mario are right: all my attempts to prove that the constructs proposed by Thierry and me end up in statements of the form "R = (Base ` R)" to be proven, as Mario expected. Therefore, it seems that the composition defined for SetCat is not compatible with the homs of RngCat/RingCat. The proposal of Mario, however, to provide an alternative version of the Set category consisting of extensible structures seems to be promising. I'll try this approach...
@avekens What do you dislike about your current definition df-rngc ? Indeed, one can define sets as extensible structures, and on the one hand, this will put them on the same footing as other structured sets like rings etc., but on the other hand, it may be awkward to have both a category of sets and a category of sets-as-extensible-structures.
I actually think that sets as extensible structures is not a bad category to have. It's not really the same as the category of sets, because different structures with the same base set are isomorphic. So it would seem to capture an important element of extensible structure reasoning in category theory terminology, and the fact that this "is" the category of sets is demonstrable through the category equivalence to Set.
You may be right. I'm not fond of extensible structures, but if they are the device of choice, then the category of sets-as-extensible-structures allows a more transparent interplay (forgetful/free adjunctions, etc.).
@digama0 Before I start to prove theorems I want to ask you if the following definition is appropriate for your suggested alternative:
df-estrc $a |- ExtStrCat = ( u e. _V |->
{ <. ( Base ` ndx ) , u >. ,
<. ( Hom ` ndx ) ,
( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. ,
<. ( comp ` ndx ) , ( v e. ( u X. u ) , z e. u
|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) ,
f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) )
|-> ( g o. f ) ) ) >. } ) $.
This is the category whose objects are all sets in a universe u
regarded as extensible structures and whose morphisms are the functions between their base sets. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set.
Or should the objects be restricted to sets which have at least a base set, like
df-estrc $a |- ExtStrCat == ( u e. _V
|-> [_ { s e. u | E. c <. ( Base ` ndx ) , c >. e. s } / b ]_ { <. ( Base ` ndx ) , b >. , ...
@benjub My goal is to have definitions which allows for proving that RingCat is a subcategory of RngCat ( ( ( RngCat
U ) |cat ( RingHom |
( R X. R ) ) ) = ( RingCat U ) ) `), see the start of this discussion. For this, I need a more general definition of the composistion as currently used for RngCat and RingCat. The most general definition of a composition, if extensible structutres are involved, is the one given in ExtStrCat. By this, I think the following "inclusion chain" can be proved (although the morphisms of the shown categories are different):
RingCat -> RngCat -> GrpCat -> MndCat -> MgmCat -> ExtStrCat ( "->" means "is subcategory of")
@avekens The first definition is correct. Most definitions based on extensible structures do not make any constraints on the object itself (besides it being a set), except "extensionally" by asking what the results of ( Base ` X )
, ( +g ` X )
, and so on, are. The only exception to this is df-struct, which is mostly a utility for quickly proving the extraction lemmas for a concretely given structure in O(n log n) of the number of slots rather than O(n^2) for an unstructured set of ordered pairs.
@avekens sorry I made you waste your time checking my proposal, and thanks to the others for pointing out my mistake.
I'll have my go at the definition of the "Structure" category, but please check it first! ;-)
df-strc $a |- StructCat = ( u e. _V |->
[_ ( ( `' Base " _V ) i^i u ) / b ]_
{ <. ( Base ` ndx ) , b >. ,
<. ( Hom ` ndx ) ,
( x e. b , y e. b |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. ,
<. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b
|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) ,
f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) )
|-> ( g o. f ) ) ) >. } ) $.
( `' Base " _V )
is just _V
. Every set is in the preimage of Base
because ( Base ` { <. 1 , X >. } ) = X
. So you can just use u
in place of b
.
Oh wait, I got the direction mixed up. Above is an argument that ( Base " _V ) = _V
; ( `' F " _V ) = _V
is in fact true for every class function on _V
.
@tirix I have made the same mistake, so I have to blame myself ;-). Of corse I'll commit the definition to Github onyl after I have proved some theorems which confirm its soundness.
@digama0 I actually could (formally) prove that ( `' Base " _V ) = _V
(I'll provide that proof with my next PR). Therefore, ( ( `' Base " _V ) i^i u )
is actually just u
(see ~inv1), so that we need no substitution.
@benjub My goal is to have definitions which allows for proving that RingCat is a subcategory of RngCat, ( ( RngCat ` U ) |`cat ( RingHom |` ( R X. R ) ) ) = ( RingCat ` U ) ), see the start of this discussion. For this, I need a more general definition of the composistion as currently used for RngCat and RingCat.
This looks true with the current df-rngc and df-ringc, which have a very similar form?
By this, I think the following "inclusion chain" can be proved (although the morphisms of the shown categories are different): RingCat -> RngCat -> GrpCat -> MndCat -> MgmCat -> ExtStrCat ( "->" means "is subcategory of")
RingCat can indeed be seen as a subcategory of RngCat (even though the unit could be considered part of the structure and not simply a property), and similarly for GrpCat and MndCat, but the other "inclusions" are not true/meaningful mathematically. You may devise a metamath-coding which allows to prove them, but it would not mean much. It's a bit like wanting to prove that 2 is a subset of 3: you might use an encoding which makes it true (e.g. the von Neumann encoding of natural numbers), but it does not mean much.
By this, I think the following "inclusion chain" can be proved (although the morphisms of the shown categories are different): RingCat -> RngCat -> GrpCat -> MndCat -> MgmCat -> ExtStrCat ( "->" means "is subcategory of")
RingCat can indeed be seen as a subcategory of RngCat (even though the unit could be considered part of the structure and not simply a property), and similarly for GrpCat and MndCat, but the other "inclusions" are not true/meaningful mathematically. You may devise a metamath-coding which allows to prove them, but it would not mean much.
I'm not sure what you mean by this. If I understand correctly, all of the categories in the inclusion chain are totally reasonable and should be in a subcategory chain. If we generalize from subcategories to embeddings, then we can even fit Set into the chain, equivalent to ExtStrCat at the end.
Perhaps you are saying that it is abusive to have a ring "be" a group in the literal sense. We will have to disagree on this, but even if it was not (or if we were dealing with another functor which is not the inclusion map), we could still use embeddings to make the chain. For example RingCat embeds into MndCat via the forgetful functor mulGrp
.
The functor "multiplicative group" from Ring to Mnd is not an embedding (not injective on objects). Similarly, the forgetful functor "underlying (additive) group" from Ring to Grp is not an embedding (not injective on objects). Therefore, proving some kinds of inclusions through non-natural functors which depend on the specific metamath-encoding is dangerous.
I think that the problem comes from the fact that extensible structures are defined "as rich as possible", and that this does not play well with categorical thinking. For instance, consider the three extensible strutures:
They "are" groups in the metamath encoding. Are they three different groups ? This would be problematic in categorical thinking.
Edit: If, indeed, these are considered three different groups, then the functors of the first paragraphs are embeddings (since one "duplicates" the images to make the functor injective on objects), but it feels strange, doesn't it ?
I think that "injective on objects" is not a "categorical" notion, nor is being a subset of objects as in a subcategory. According to https://en.wikipedia.org/wiki/Subcategory, there seems to be some dispute on whether an embedding is a full and faithful functor or whether it is also injective on objects, and in particular points out that the Yoneda embedding is only an embedding by the former definition.
In the extensible structures world, equality of objects is not a meaningful notion. Only isomorphism, or the intermediate "equality up to slots" matter. Luckily this is exactly the mentality that is brought by category theory, so it would seem to be a good fit.
In your example, those are three instances of "the same" group. They are equal up to base and +g, which implies that they are isomorphic objects in ExtStrCat, MgmCat, GrpCat but not RngCat and RingCat.
I think you should just get the idea of injectivity of objects out of your mind. It doesn't matter. In a category there is already a suitable replacement for injectivity of objects, and that is isomorphism in the target implies isomorphism in the source, and this is already implied by a full and faithful functor. (That said, most of these forgetful functors are only faithful, not full, because the hom sets grow as you go down the chain.)
I think that "injective on objects" is not a "categorical" notion, nor is being a subset of objects as in a subcategory.
You're right, since equality is an "evil" notion, in categorical lingo, and should be upgraded to isomorphism, for functors the important notion is faithfulness. That's basically what I advocated above: simply define the natural forgetful functor, prove its faithfulness, and call it a day without proving the subcategory thing.
I maintain that viewing Ring as a subcategory of Group is pretty weird. Even though as you say, it is consistent with the set.mm encoding.
In a category there is already a suitable replacement for injectivity of
objects, and that is isomorphism in the target implies isomorphism in the source, and this is already implied by a full and faithful functor. (That said, most of these forgetful functors are only faithful, not full, because the hom sets grow as you go down the chain.
Yes, a fully faihful functor obviously reflects isomorphisms, but in the present case, reflection of isomorphisms follows from faithfulness alone since functors are between algebraic constructs (or monadic is enough, don't remember). This is just fancy vocabulary and can be proved by hand for Ring and friends.
@benjub
I maintain that viewing Ring as a subcategory of Group is pretty weird. Even though as you say, it is consistent with the set.mm encoding.
While this probably won't change your mind, here's how Herstein defines rings:
From I. N. Herstein, Abstract algebra, 3rd ed., 1995, p. 126
Definition. A nonempty set R is said to be a ring if in R there are two operations + and . such that: (a) a,b e. R implies that a + b e. R. (b) a + b = b + a for a,b e. R. (c) (a + b) + c = a + (b + c) for a,b,c e. R. (d) There exists an element 0 e. R such that a + 0 = a for every a e. R. (e) Given a e. R, there exists a b e. R such that a + b = O. (We shall write b as -a.) Note that so far all we have said is that R is an abelian group under +. We now spell out the rules for the multiplication in R... ...
Here he calls R a "an abelian group under +" even though R has an extraneous . operation. He didn't say, "R with the . operation removed is an abelian group under +."
I suppose that "under" could be interpreted as "removing everything else," but I think it could also be interpreted as "ignoring everything else" which is essentially what extensible structures do. He doesn't seem to define "under" anywhere that I could find, but his other uses suggest he means focusing on + while ignoring the rest.
Thanks @nmegill for this example, and indeed this does not change my mind ;)
Of course, it is only my opinion, and @avekens or other people who do the work should feel free to use whatever encoding system they prefer.
I can fully understand @benjub `s concerns about rings being (abelian) groups, because 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) C_ Ob(B) and MorA(X,Y) C Mor_B(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) C_ 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.
I looked up more books about algebra, and all definitions are vague about rings being groups:
All definitions say "A ring A is a (...) group", which would mean A e. Ring -> A e. Grp, but always with an amendment restricting this statement to the addition. But this "restriction" is never defined formally.
To conclude, as long as we define Rings, Groups, etc. in a way that A e. Ring -> A e. Grp is valid (see ~rnggrp) 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
g e. Grp -> g Struct <. ( Base ` ndx ) , ( +g ` ndx ) >.
r e. Ring -> r Struct <. ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) >.
I will continue, however, to work with the current definitions...
The forgetful functor from Ring to Group is injective neither on objects nor on isomorphism classes of objects. Therefore, I think it should not be called an embedding and Ring should not be called a subcategory of Group. @digama0 says that it is a pseudomonic functor (faithful and full on isomorphisms), therefore it reflects isomorphisms (i.e. it is conservative), and therefore it deserves the name of "embedding" and Ring deserves to be a "subcategory" of Group.
This is a matter of taste, although, set.mm being set-theoretical, as opposed to category-theoretical, I think it makes more sense to define an embedding as a faithful and injective-on-objects functor.
Of course, injectivity on objects is a 0-categorical, i.e. set-theoretical, notion, and faithfulness is 1-categorical (because it is injectivity on homsets), so you can climb the ladder to 2-categorical, etc. This does not always disqualifies the lower rungs. Since set.mm itself is set-theoretical, I think injectivity on objects is relevant.
@digama0 : by the way, the Yoneda embedding is injective on objects, unless you mess up the definition of a category and make the homsets non-disjoint.
With PR #1539 and #1542, I provided the definition of the category of extensible structures, and the definitions of the categories of non-unital and unital rings as restrictions of the category of extensible structures, i.e. as subcategories of the category of extensible structures. All previous theorems could be reproven, they are still available marked with OLD (I will delete these, however, in the near future).
With ~rngcresringcat I could prove that the restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. This was the starting point of this issue, so that I will close this issue.
In the section header comments I summarized the results of our discussion, and maybe I will provide some more theorems based on it.
With PR #1506 I proved that the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings (see ~rhmsubc) and that the restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category (see ~rhmsubccat):
I also wanted to show
but this is not possible because the compositions are different. Therefore, I think my definions of the Categories of Rngs and Rings are not adequate, i.e. too restrictive, e.g.:
I plan to replace the comp slot by the composition used for the category of sets (see ~df-setc). Before that, I want to provide a definition for such a composition:
With this definition, I plan to change the definition of categories of Rngs (and Rings):
By this, I think
( C |`cat H ) = ( RingCat ` U )
can be proved. Analogously, categories of Rngs (and Rings) can be shown to be restrictions/subcategories of the category of sets.Unfortunately, I found no hints in the literature how to precisely define the composition within the category of rings. In http://katmat.math.uni-bremen.de/acc/acc.pdf, however, I found for "Grp", the category of groups:
This gives me the assurance that my new definition is appropriate.
@benjub, @digama0 what do you think?