On the definition of RR^n and things concerning probability theory work
193 views
Skip to first unread message
savask
Oct 16, 2017, 11:16:44 AM10/16/17
to Metamath
The long-awaited (at least for me :-) ) update on probability theory and general measure theory was recently delivered by Thierry Arnoux and that got me into thinking.
At some point, the direct product of RR with itself is considered and studied from the standpoint of topology, then, as I understand, some steps are taken into proving facts about dyadic squares on RR^2. When finished that will provide a Borel sigma algebra on RR^2 and then finally area can be defined.
While RR^2 as a set of pairs must fit well into the already developed framework (for example, the product of two sigma-algebras seems to be defined), it looks like not constraining yourself to products of two sigma-algebras only seems like a good idea. Proving the results about dyadic cubes in the case of RR^N should be doable and will yield a smoother development process in case if we ever go as far as developing calculus on RR^N.
So with that in mind, I suggest to try fixing a more or less coordinated definition of RR^N. I know that this question has been risen before a few times without any definite results, but when so much work is being put into the probability branch, not having an "official" version of RR^N seems to be a sad omission which may make us pay later, when some parts depending on a specific construction of RR^2 will have to be rewritten into a more general framework.
I suggest the following definition:
df-rrtn $a |- RRn = ( n e. NN |-> ( ( CCfld |`s RR ) freeLMod ( 1 ... n ) ) ) $.
The function freeLMod here is from Stefan O'Rear's mathbox and it has the structure product underneath, so in this definition RRn will inherit a few properties of
( CCfld |`s RR ). That is, it's trivial to prove that RRn will be a vector space, and though I didn't check it, it must also be a topological product and have a corresponding metric. I think it should also be mentioned that freeLMod has quite a few theorems proved about it and ties in nicely with the linear algebra framework developed by Stefan. If I'm not mistaken, square matrices, for example, are a freeLMod, so one could build a map from RR^(n x n) onto the matrix algebra and perhaps prove some results by continuity (or consider manifolds arising from certain matrix groups).
Virtually the only quality this definition of RR^N lacks is the Hilbert space structure. df-prds doesn't seem to define the inner product for a structure product (btw, it would be great if a comment for df-prds listed structures it can work with and the ways it generalizes operations), but probably it can be changed. Another option is artificially augmenting RRn with an inner product, but that makes treating RRn as a free left module a bit harder.
Another variation of this definition is dropping the ( 1 ... n ) part and using an arbitrary set there. Maybe it makes it more general, but I feel that writing ( 1 ... n ) in every usage of RR^N will get a bit tedious.
I hope to hear some opinions on whether or not this definition looks good enough and/or some other suggestions and enhancements. It would be especially interesting to know if it's indeed a good idea to use a general RR^N definition in the Borel sigma-algebra work.
At some point, the direct product of RR with itself is considered and studied from the standpoint of topology, then, as I understand, some steps are taken into proving facts about dyadic squares on RR^2. When finished that will provide a Borel sigma algebra on RR^2 and then finally area can be defined.
While RR^2 as a set of pairs must fit well into the already developed framework (for example, the product of two sigma-algebras seems to be defined), it looks like not constraining yourself to products of two sigma-algebras only seems like a good idea. Proving the results about dyadic cubes in the case of RR^N should be doable and will yield a smoother development process in case if we ever go as far as developing calculus on RR^N.
So with that in mind, I suggest to try fixing a more or less coordinated definition of RR^N. I know that this question has been risen before a few times without any definite results, but when so much work is being put into the probability branch, not having an "official" version of RR^N seems to be a sad omission which may make us pay later, when some parts depending on a specific construction of RR^2 will have to be rewritten into a more general framework.
I suggest the following definition:
df-rrtn $a |- RRn = ( n e. NN |-> ( ( CCfld |`s RR ) freeLMod ( 1 ... n ) ) ) $.
The function freeLMod here is from Stefan O'Rear's mathbox and it has the structure product underneath, so in this definition RRn will inherit a few properties of
( CCfld |`s RR ). That is, it's trivial to prove that RRn will be a vector space, and though I didn't check it, it must also be a topological product and have a corresponding metric. I think it should also be mentioned that freeLMod has quite a few theorems proved about it and ties in nicely with the linear algebra framework developed by Stefan. If I'm not mistaken, square matrices, for example, are a freeLMod, so one could build a map from RR^(n x n) onto the matrix algebra and perhaps prove some results by continuity (or consider manifolds arising from certain matrix groups).
Virtually the only quality this definition of RR^N lacks is the Hilbert space structure. df-prds doesn't seem to define the inner product for a structure product (btw, it would be great if a comment for df-prds listed structures it can work with and the ways it generalizes operations), but probably it can be changed. Another option is artificially augmenting RRn with an inner product, but that makes treating RRn as a free left module a bit harder.
Another variation of this definition is dropping the ( 1 ... n ) part and using an arbitrary set there. Maybe it makes it more general, but I feel that writing ( 1 ... n ) in every usage of RR^N will get a bit tedious.
I hope to hear some opinions on whether or not this definition looks good enough and/or some other suggestions and enhancements. It would be especially interesting to know if it's indeed a good idea to use a general RR^N definition in the Borel sigma-algebra work.
fl
Oct 16, 2017, 2:40:19 PM10/16/17
to Metamath
To have an official definition of RR ^ N would be a very good thing. It is not a structure since the base set is not abstract so you don't need to use the structure builder to define it.
On contrary you can define each part (the base set, the norms, the distances, the operations ...) in isolation and then group them together to show that in the
case so or so one structure or another can be applied to RR ^ N .
Moreover it would allow several people to work smoothly together on several aspects of RR ^ N .
--
FL
Thierry Arnoux
Oct 16, 2017, 9:33:00 PM10/16/17
to meta...@googlegroups.com, savask
Hi,
(resending on the mailing list!)
Nice to see my developments draw interest! :-)
Yes, following the same method, the same results could be proven on
RR^n, which could then provide a path to the Borel measure on RR^n.
I've chosen to work in RR^2 for simplicity and indeed also because of
the lack of a commonly agreed definition for RR^n, but the literature I
saw always treated the RR case, then RR^n.
With an official structure and basic theorems, it would not be too hard
to move the proofs to RR^n.
> Seeing new areas of math being formalized in Metamath is always
> thrilling, so my interest is very logical
>
> I was afraid that maybe you were using RR x RR because of its
> structure as a set of pairs, which roughly corresponds to the same
> situation with product topology. RR^N as a structure power will have a
> set of functions underneath, so some notions will have to be redefined
> appropriately (such as sigma algebra product, for example). I guess,
> right now the RR x RR work didn't go very far so moving proofs won't
> be very painful, though the more time we wait, the harder it gets.
Right : I think I would probably keep the product sigma-algebra as
defined now, and add the n-dimensional product. Anyway my direction now
for probabilities is to define the measure integral. That may keep me
busy for the next... months.
BR,
_
Thierry
(resending on the mailing list!)
Nice to see my developments draw interest! :-)
Yes, following the same method, the same results could be proven on
RR^n, which could then provide a path to the Borel measure on RR^n.
I've chosen to work in RR^2 for simplicity and indeed also because of
the lack of a commonly agreed definition for RR^n, but the literature I
saw always treated the RR case, then RR^n.
With an official structure and basic theorems, it would not be too hard
to move the proofs to RR^n.
> Seeing new areas of math being formalized in Metamath is always
> thrilling, so my interest is very logical
>
> I was afraid that maybe you were using RR x RR because of its
> structure as a set of pairs, which roughly corresponds to the same
> situation with product topology. RR^N as a structure power will have a
> set of functions underneath, so some notions will have to be redefined
> appropriately (such as sigma algebra product, for example). I guess,
> right now the RR x RR work didn't go very far so moving proofs won't
> be very painful, though the more time we wait, the harder it gets.
Right : I think I would probably keep the product sigma-algebra as
defined now, and add the n-dimensional product. Anyway my direction now
for probabilities is to define the measure integral. That may keep me
busy for the next... months.
BR,
_
Thierry
savask
Oct 17, 2017, 2:28:58 AM10/17/17
to Metamath
It is not a structure since the base set is not abstract so you don't need to use the structure builder to define it.
set.mm seems to have other examples of objects which are not "abstract" but still use structures for them, for example the symmetric group is a structure while it has a very concrete base set (bijections). Or Z/nZ is defined as a quotient ring while again, it could have been defined as a set 0 ... n-1 with corresponding operations. I'm not well acquainted with set.mm unfortunately, but it seems that the only exception to this rule is the set of complex numbers and that's probably because it is used that often, that using it as a structure would get cumbersome.
In case of RR^n though, one probably won't need to do a lot of direct computations on it. If we were to develop RR^n in the CC fashion, we would have to introduce a whole new bunch of symbols for vector addition, subtraction, inner product, norm, product on a scalar and so on. Then we could show that RR^n is a Hilbert space (similar to how Cfld shows that CC is a field), but then if we wanted to use some known theorems on Hilbert spaces, we would have to transfer them into our "direct" RR^n language. So essentially we will be redoing a lot of work which has been done in the theorems about, say, freeLMod or Cfld.
In case of RR^n though, one probably won't need to do a lot of direct computations on it. If we were to develop RR^n in the CC fashion, we would have to introduce a whole new bunch of symbols for vector addition, subtraction, inner product, norm, product on a scalar and so on. Then we could show that RR^n is a Hilbert space (similar to how Cfld shows that CC is a field), but then if we wanted to use some known theorems on Hilbert spaces, we would have to transfer them into our "direct" RR^n language. So essentially we will be redoing a lot of work which has been done in the theorems about, say, freeLMod or Cfld.
Anyway my direction now for probabilities is to define the measure integral.
By the way, as FL suggested earlier, picking a book (or several) as a guidance is a good idea. Most of theorems about sigma-algebras and probabilities don't seem to have references to any sources, so the question is, do you have a set of books you're using as a base? Maybe if someone wanted to develop sigma-algebras work in parallel to you, having a common source for definitions would come in handy.
Mario Carneiro
Oct 17, 2017, 3:02:14 AM10/17/17
to metamath
On Mon, Oct 16, 2017 at 11:16 AM, savask <sav...@yandex.ru> wrote:
The long-awaited (at least for me :-) ) update on probability theory and general measure theory was recently delivered by Thierry Arnoux and that got me into thinking.
At some point, the direct product of RR with itself is considered and studied from the standpoint of topology, then, as I understand, some steps are taken into proving facts about dyadic squares on RR^2. When finished that will provide a Borel sigma algebra on RR^2 and then finally area can be defined.
While RR^2 as a set of pairs must fit well into the already developed framework (for example, the product of two sigma-algebras seems to be defined), it looks like not constraining yourself to products of two sigma-algebras only seems like a good idea. Proving the results about dyadic cubes in the case of RR^N should be doable and will yield a smoother development process in case if we ever go as far as developing calculus on RR^N.
So with that in mind, I suggest to try fixing a more or less coordinated definition of RR^N. I know that this question has been risen before a few times without any definite results, but when so much work is being put into the probability branch, not having an "official" version of RR^N seems to be a sad omission which may make us pay later, when some parts depending on a specific construction of RR^2 will have to be rewritten into a more general framework.
I suggest the following definition:
df-rrtn $a |- RRn = ( n e. NN |-> ( ( CCfld |`s RR ) freeLMod ( 1 ... n ) ) ) $.
A minor quibble with this definition is that the freeLMod construction does a structure restriction to the finitely supported functions, which is superfluous in this case because the domain is finite. In other words, the following produces a provably identical term:
df-rrtn $a |- RRn = ( n e. NN |-> ( ( CCfld |`s RR ) ^s ( 1 ... n ) ) ) $.
One other thing that I'd rather not commit to is a particular finite set as the base. I may yet be convinced that it is untenable to just work with R^I where I is a finite set, but most of the theorems I know about R^n are exactly the same even if the index set is unordered. I can imagine that the choice to use 1...n specifically will bite us later, say if we want to work with Words (which use 0..^n instead) or vector products of R^n or something which, like finite sums, may need to be over other finite sets like subsets and cartesian products of finite sets.
Virtually the only quality this definition of RR^N lacks is the Hilbert space structure. df-prds doesn't seem to define the inner product for a structure product (btw, it would be great if a comment for df-prds listed structures it can work with and the ways it generalizes operations), but probably it can be changed. Another option is artificially augmenting RRn with an inner product, but that makes treating RRn as a free left module a bit harder.
Most of the theorems about free left modules should not be dependent on the structure literally having the form ( A freeLMod B ), because of this exact reason. Most structure theorems instead carefully delineate the "relevant" parts of the structure for the definition or theorem to make sense, so that these kind of augmentations can be papered over once you have the theorems that say that all of the original components are preserved.
df-prds doesn't define an inner product because I wasn't aware of a good way to generalize the inner product, but now that I come to think of it, it seems that <a,b> = sum_ i e. I <a(i), b(i)> will do just fine. We would also need to augment ringLMod (df-rgmod) to put the ring multiplication as the inner product so that RR gets the right inner product over itself before taking the product.
Another variation of this definition is dropping the ( 1 ... n ) part and using an arbitrary set there. Maybe it makes it more general, but I feel that writing ( 1 ... n ) in every usage of RR^N will get a bit tedious.
Actually, I would suggest not putting (1...n) in all the time, as that defeats the purpose of the generality. Instead all the theorems would be stated for arbitrary finite sets, so there is no additional tedium, just more generality (and possibly harder proofs, but I would bet that the generality helps more than hinders, since it is a lot easier to put finite sets together and still have the algebraic laws on the cardinalities).
Mario
fl
Oct 17, 2017, 5:56:35 AM10/17/17
to Metamath
It would have been me, RR ^N would have been defined a long time ago over 1 .. N with all the distances and operations in isolation.
And we would have theorems about it.
--
FL
David A. Wheeler
Oct 17, 2017, 7:36:46 AM10/17/17
to Mario Carneiro, metamath
On October 17, 2017 3:02:12 AM EDT, Mario Carneiro <di....@gmail.com> wrote:
>A minor quibble with this definition is that the freeLMod construction
>does
>a structure restriction to the finitely supported functions, which is
>superfluous in this case because the domain is finite...
>A minor quibble with this definition is that the freeLMod construction
>does
>a structure restriction to the finitely supported functions, which is
>One other thing that I'd rather not commit to is a particular finite
>set as
>Actually, I would suggest not putting (1...n) in all the time, as that
>defeats the purpose of the generality. Instead all the theorems would
>be
>stated for arbitrary finite sets, so there is no additional tedium,
>just
>more generality (and possibly harder proofs, but I would bet that the
>generality helps more than hinders, since it is a lot easier to put
>finite
>sets together and still have the algebraic laws on the cardinalities)...
>defeats the purpose of the generality. Instead all the theorems would
>be
>stated for arbitrary finite sets, so there is no additional tedium,
>just
>more generality (and possibly harder proofs, but I would bet that the
>generality helps more than hinders, since it is a lot easier to put
>finite
What definition would you like to see instead?
--- David A.Wheeler
Mario Carneiro
Oct 17, 2017, 7:44:48 AM10/17/17
to David A. Wheeler, metamath
Combining all the recommendations in the previous email would look something like:
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.
df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
Mario
fl
Oct 17, 2017, 8:07:41 AM10/17/17
to Metamath
Combining all the recommendations in the previous email would look something like:
You mean your own recommendations in your previous email.
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
So clear. It will be appreciate.
--
FL
fl
Oct 17, 2017, 8:16:42 AM10/17/17
to Metamath
You mean your own recommendations in your previous email.
Be courageous. Say "I".
--
FL
savask
Oct 17, 2017, 10:33:57 AM10/17/17
to Metamath
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.
df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
I guess I agree with what is being said about using an arbitrary set as indices, it is similar to the approach in Jeff Madsen's mathbox and if I recall correctly, real matrices in Stefan O'Rear's mathbox will be RR^ ( n X. n ) elements straight away.
Is this more or less settled up then? df-prds change is pretty global though, so it would be great to hear some suggestions/objections/etc concerning it, before diving into changing all dependent results.
Is this more or less settled up then? df-prds change is pretty global though, so it would be great to hear some suggestions/objections/etc concerning it, before diving into changing all dependent results.
Thierry Arnoux
Oct 17, 2017, 1:20:17 PM10/17/17
to meta...@googlegroups.com, savask
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
How could I add them to the Bibliography?
David A. Wheeler
Oct 17, 2017, 1:20:36 PM10/17/17
to Mario Carneiro, metamath
On October 17, 2017 7:44:46 AM EDT, Mario Carneiro <di....@gmail.com> wrote:
>Combining all the recommendations in the previous email would look
>something like:
Cool! Can you show an example of how those definitions would be used together? (No need to write a proof, I just want to see them used together.)
>Combining all the recommendations in the previous email would look
>something like:
Everyone else: Would these proposed definitions work? I'm sure there are many ways to do this, but are there *serious* technical problems with the ones outlined by Mario (if so, what are the problems and what is the better alternative)? Or tweaks that would improve it? I'd just like to eventually move to a rough consensus.
--- David A.Wheeler
savask
Oct 17, 2017, 1:34:44 PM10/17/17
to Metamath
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
Thanks for the list. As I understand the book Mario was orienting on when defining vol is Fremlin, Measure theory, so I guess it can be used as well. On a quick glance it seems pretty comprehensive and what's nice, it often offers full proofs of the results which could be considered "obvious" (for example the theorem on bounding the measure of a box by sum of measures of its box cover).
Everyone else: Would these proposed definitions work? I'm sure there are many ways to do this, but are there *serious* technical problems with the ones outlined by Mario (if so, what are the problems and what is the better alternative)? Or tweaks that would improve it? I'd just like to eventually move to a rough consensus.
I don't have any objections - as noticed by Mario earlier, the freeLMod definition is equivalent to the structure product one, and before writing this topic I've tried proving theorems like |- ( RRn ` N ) e. LVec so there shouldn't be any serious technical issues (at very least the object we are talking about is a vector space, heh). And concerning tweaks to the structure product to make it work on Hilbert spaces, I think these changes can be even postponed for some time, since they shouldn't affect theorems about RR^ not using the Hilbert space structure.
Norman Megill
Oct 17, 2017, 3:23:28 PM10/17/17
to Metamath
On Tuesday, October 17, 2017 at 1:20:17 PM UTC-4, Thierry Arnoux wrote:
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
How could I add them to the Bibliography?
The file mmset.html is in the develop branch on github, so you can edit it directly and do a pull request. Follow the formatting by example; in particular, the <A NAME="Author"> tag must be an exact match to the [Author] reference in set.mm.
The "[QAnnn...]" number at the end of many references is optional but nice to have for finding the book in a library (for US universities at least); I use the number obtained by looking up the book at http://libraries.mit.edu/barton .
The set.mm formatting should follow the specification given by 'help write bib' in metamath.exe.
Norm
Benoit
Oct 17, 2017, 7:12:52 PM10/17/17
to Metamath
Just a few uninformed remarks from an "end-user" who does not know well the internal machinery of set.mm:
- The idea of defining \R^I for any set I seems better than restricting to \R^n (and similarly for \C^I).
- The field of real numbers seems central enough in mathematics to deserve its own definition: RRfld = CCfld |`s RR.
- For Hilbert spaces, it is not the product, but the direct sum, which is important (of course, it is the same for finite sums/products, but it looks like you wanted to treat the general case; actually, I even doubt that the product exists in general). (And just to clear a possible confusion from the original post: a free module is a direct sum, that is, a coproduct, not a product.)
- The idea of defining \R^I for any set I seems better than restricting to \R^n (and similarly for \C^I).
- The field of real numbers seems central enough in mathematics to deserve its own definition: RRfld = CCfld |`s RR.
- For Hilbert spaces, it is not the product, but the direct sum, which is important (of course, it is the same for finite sums/products, but it looks like you wanted to treat the general case; actually, I even doubt that the product exists in general). (And just to clear a possible confusion from the original post: a free module is a direct sum, that is, a coproduct, not a product.)
> df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
David A. Wheeler
Oct 17, 2017, 8:18:46 PM10/17/17
to Benoit, Metamath
On October 17, 2017 7:12:51 PM EDT, Benoit <benoit...@gmail.com> wrote: ...
--- David A.Wheeler
>- The field of real numbers seems central enough in mathematics to
>deserve
>its own definition: RRfld = CCfld |`s RR.
I agree. Others?
>deserve
>its own definition: RRfld = CCfld |`s RR.
--- David A.Wheeler
Mario Carneiro
Oct 17, 2017, 9:27:58 PM10/17/17
to metamath
Okay, so it looks like there are a few issues with MY previous proposal in MY previous email.
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.
This one is almost correct, and actually got me thinking in the same direction as Benoit (why not just define RRfld and skip RR^?), but it doesn't actually use the .i component coming from ringLMod, because it needs to be upgraded into a vector space first. So it should look like this instead:
df-rrx $a |- RR^ = ( i e. _V |-> ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) $.
and that's just a bit too cumbersome to not have a dedicated definition.
---
df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
This one is okay as far as it goes, but the distance component is wrong for R^n - it gives the supremum metric instead of the sum-of-squares metric. Luckily this was also foreseen, and the toCHil function works for exactly this purpose. Whence:
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
At this point it clearly can't be written in the form ( R ^s I ) for some appropriate definition of R, so having the RR^ definition is important.
- For Hilbert spaces, it is not the product, but the direct sum, which is important (of course, it is the same for finite sums/products, but it looks like you wanted to treat the general case; actually, I even doubt that the product exists in general). (And just to clear a possible confusion from the original post: a free module is a direct sum, that is, a coproduct, not a product.)
It should be mentioned that not all components make sense in all contexts. These are definitions that work in SOME cases, and in particular work whenever we care about them. The extensible structure framework allows us to have utter garbage in irrelevant components without affecting any theorems, so that the single definition df-prds can be a group when its pieces are groups, and a topological space when its pieces are topological spaces, despite these having no common slots except Base.
A few of the slots in df-prds don't make sense if the base set is infinite, or only make sense under restricted conditions:
* dist makes sense as an extended metric, but is only a metric on a subspace in which every two functions are uniformly bounded apart. (The direct sum satisfies this.)
* .i as I've written above makes sense only when the two functions are finitely supported (i.e. exactly on the direct sum). There are expansions of this domain of interest, for example taking an infinite sum instead of a finite sum when it exists, but to write this as a function using tsums would need me to assume that the structure is equipped with a Hausdorff topological structure, which would get in the way if dealing with purely algebraic structures with no topology. In this case it would be better to have a "pimp my metric" structure function like toCHil that just overrides the .i component with one generated from the existing topology on the structure.
This simply means that the full product space will not have any nice theorems like "the product of infinitely many Hilbert spaces is a Hilbert space", but does not mess up any theorems. In particular, you can take a structure restriction and then it *will* be a good inner product, so that df-prdm will actually satisfy such a theorem by inheriting the sometimes-defined, sometimes-garbage definition from df-prds and screening out the garbage parts.
---
> df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
I don't understand anything to this line (I haven't looked it up in set.mm), but to anyone new to metamath (or at least, new to set.mm), "sSet" means "simplicial set" (which it probably doesn't, here), so maybe a more meaningful name could be found ?
Although this is fine as a definition, it is questionable if it should actually go in subringAlg instead of ringLMod. For context, what these definitions are doing is:
* subringAlg takes a ring and produces a module (or takes a field and produces a vector space) whose scalar ring is a specified subring. For example, we might want to view RR as a QQ vector space, which can be written as ( ( subringAlg ` ( CCfld |`s RR ) ) ` QQ ).
* ringLMod is just specializing to viewing a field as a one-dimensional vector space over itself.
The reason these are needed in defining RR^n is because the general construction of taking a product of vector spaces takes as input an F-vector space and outputs another F-vector space - there is no producting happening in the F. So RR^n, as an RR vector space, is the n-fold product of RR, as an RR vector space. But (CCfld |`s RR) itself is not an RR vector space, it is a field, and we need to upgrade it to a vector space first using ringLMod.
Now on to the issue. If R is a ring and A is a subring, then an inner product for ((subringAlg ` R) `A), if it exists, should have the type R X. R -> A (roughly). But the ring product essentially never satisfies this when A =/= R, because r * 1 = r e. R. So it seems silly to augment subringAlg with an inner product that never works, and instead the augmentation should happen in ringLMod:
df-rgmod $a |- ringLMod = ( w e. _V |->
( ( ( subringAlg ` w ) ` ( Base ` w ) ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) $.
( ( ( subringAlg ` w ) ` ( Base ` w ) ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) $.
Re simplicial sets: No, of course sSet doesn't mean that here. It's a good point that the notation is already taken, though, and we should probably change the name. This is the "structure set/assign" function, which takes a structure S and a component <. N , X >. and produces a new structure ( S sSet <. N , X >. ) in which every slot is the same except N, which has the value X instead of whatever S had. Do you have any suggestions for a better name?
On Tue, Oct 17, 2017 at 7:12 PM, Benoit <benoit...@gmail.com> wrote:
- The field of real numbers seems central enough in mathematics to deserve its own definition: RRfld = CCfld |`s RR.
I'd rather hold off on this until it is central enough in *metamath* to give it a definition. (CCfld |`s RR) is used 5 times in set.mm, CCfld is used 286 times. Also keep in mind that a structure definition of any complexity at all (anything more than a single constant) should probably be given a temporary definition, i.e. put $e |- R = ( CCfld |`s RR ), or R = ( RR^ ` I ) in the case of R^n, in your assumptions to any theorems. Given this convention, a little complexity in the structure statement is tolerable because it only shows up once at the top of the theorem. Plus, if all the theorems have such abbreviations for RRfld then if it eventually becomes used enough to warrant a definition the retrofit will be easy.
On Tue, Oct 17, 2017 at 1:20 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
Cool! Can you show an example of how those definitions would be used together? (No need to write a proof, I just want to see them used together.)
I guess ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s ( 1 ... N ) ) ) is an example? This little incantation takes the field of complex numbers, restricts it to RR to get RR as a field, then applies ringLMod to get RR as a 1-dimensional RR vector space (with an inner product that makes it a Hilbert space), then builds the space of functions from 1...N to RR (which is an n-dimensional RR vector space which is still a Hilbert space), then finally uses the inner product to give it a norm that is compatible with the inner product, turning it into a CHil (a complex Hilbert space where "complex" actually means the scalar field is a subset of the complexes, i.e. RR). I'm pretty sure the result has all the slots and compatibilities of RR^n we are currently capable of stating.
Mario
David A. Wheeler
Oct 17, 2017, 10:43:02 PM10/17/17
to metamath, metamath
> On Tue, Oct 17, 2017 at 1:20 PM, David A. Wheeler wrote:
> > Cool! Can you show an example of how those definitions would be used
> > together? (No need to write a proof, I just want to see them used together.)
> > Cool! Can you show an example of how those definitions would be used
> > together? (No need to write a proof, I just want to see them used together.)
On Tue, 17 Oct 2017 21:27:56 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I guess ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s ( 1 ... N ) ) ) is
> an example?
No, I meant an example of how these definitions would be *used* :-).
> I guess ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s ( 1 ... N ) ) ) is
> an example?
For a trivial example, this would be a correct (and common) use of RR^ , yes?:
( RR^ ` ( 1 ... N ) )
Also, I presume the use of Xs_ (per df-prds) would stay the same,
e.g., in prdsmndd we have:
Y = ( S Xs_ R )
and in df-pws we would still have:
$a |- ^s = ( r e. _V , i e. _V |->
( ( Scalar ` r ) Xs_ ( i X. { r } ) ) ) $.
> This little incantation takes the field of complex numbers,
> restricts it to RR to get RR as a field, then applies ringLMod to get RR as
> a 1-dimensional RR vector space (with an inner product that makes it a
> Hilbert space), then builds the space of functions from 1...N to RR (which
> is an n-dimensional RR vector space which is still a Hilbert space), then
> finally uses the inner product to give it a norm that is compatible with
> the inner product, turning it into a CHil (a complex Hilbert space where
> "complex" actually means the scalar field is a subset of the complexes,
> i.e. RR). I'm pretty sure the result has all the slots and compatibilities
> of RR^n we are currently capable of stating.
--- David A. Wheeler
Mario Carneiro
Oct 17, 2017, 11:10:59 PM10/17/17
to metamath
On Tue, Oct 17, 2017 at 10:43 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> On Tue, Oct 17, 2017 at 1:20 PM, David A. Wheeler wrote:
> > Cool! Can you show an example of how those definitions would be used
> > together? (No need to write a proof, I just want to see them used together.)
On Tue, 17 Oct 2017 21:27:56 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I guess ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s ( 1 ... N ) ) ) is
> an example?
No, I meant an example of how these definitions would be *used* :-).
For a trivial example, this would be a correct (and common) use of RR^ , yes?:
( RR^ ` ( 1 ... N ) )
I guess I'm still confused at the distinction. We're still just applying functions. That there is RR^n, the structure, with all its technology built in. It satisfies a bunch of things:
( RR^ ` ( 1 ... N ) ) e. Group
( RR^ ` ( 1 ... N ) ) e. Abel
( RR^ ` ( 1 ... N ) ) e. LMod ( RR^ ` ( 1 ... N ) ) e. LVec
( RR^ ` ( 1 ... N ) ) e. NrmVec
( RR^ ` ( 1 ... N ) ) e. PreHil
( RR^ ` ( 1 ... N ) ) e. CHil
and with this comes a bunch of general theorems about it. But if course it's not just any complex hilbert space, it's R^n, and there are a few more things we can say about it, like Jeff Madsen's work:
rrntotbnd.r $e |- R = ( RR^ ` I ) $.
rrntotbnd.m $e |- M = ( ( dist ` R ) |` ( Y X. Y ) ) $.
$( A set in Euclidean space is totally bounded iff its is bounded.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
16-Sep-2015.) $)
rrntotbnd $p |- ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) ) $=
rrntotbnd.m $e |- M = ( ( dist ` R ) |` ( Y X. Y ) ) $.
$( A set in Euclidean space is totally bounded iff its is bounded.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
16-Sep-2015.) $)
rrntotbnd $p |- ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) ) $=
He stated it using "Rn" which is just the distance component of the new "RR^", so the retrofit is simple. Dimension is probably a bad example, since we don't have a theory of dimension yet, but it might look like:
|- ( I e. dom card -> ( dim ` ( RR^ ` I ) ) = ( card ` I ) )
where
|- dim = ( w e. _V |-> |^| ( card " ( LBasis ` w ) ) )
(thinking again) Oh, I guess this theorem doesn't work for infinite I, because the basis vectors don't actually form a basis. Maybe it would make more sense to use freeLMod after all, since as previously mentioned a few of the slots will be trashed for infinite I, and it would be nice to have all those statements like (RR^ ` I) e. CHil hold for all I, not just the finite ones. That is, I make the following recommendation:
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) freeLMod i ) ) ) $.
Obviously this means df-frlm needs to leave Stefan's mathbox, but I think it is very nicely developed and support this in any case.
Also, I presume the use of Xs_ (per df-prds) would stay the same,
e.g., in prdsmndd we have:
Y = ( S Xs_ R )
and in df-pws we would still have:
$a |- ^s = ( r e. _V , i e. _V |->
( ( Scalar ` r ) Xs_ ( i X. { r } ) ) ) $.
Yes, I am jumping straight to the place where the technology is implemented, and so all the things that are defined as special cases will just inherit the new stuff.
Mario
savask
Oct 17, 2017, 11:17:59 PM10/17/17
to Metamath
(thinking again) Oh, I guess this theorem doesn't work for infinite I, because the basis vectors don't actually form a basis. Maybe it would make more sense to use freeLMod after all, since as previously mentioned a few of the slots will be trashed for infinite I, and it would be nice to have all those statements like (RR^ ` I) e. CHil hold for all I, not just the finite ones.
Won't it confuse people, though? For example, Munkres in his book on topology distinguishes between R^omega (a countable product of copies of R) and R^inf (a finitely supported subspace of R^omega).
Mario Carneiro
Oct 17, 2017, 11:41:28 PM10/17/17
to metamath
On Tue, Oct 17, 2017 at 11:17 PM, savask <sav...@yandex.ru> wrote:
(thinking again) Oh, I guess this theorem doesn't work for infinite I, because the basis vectors don't actually form a basis. Maybe it would make more sense to use freeLMod after all, since as previously mentioned a few of the slots will be trashed for infinite I, and it would be nice to have all those statements like (RR^ ` I) e. CHil hold for all I, not just the finite ones.
Won't it confuse people, though? For example, Munkres in his book on topology distinguishes between R^omega (a countable product of copies of R) and R^inf (a finitely supported subspace of R^omega).
Of course it is important to communicate the choice we make in the end. Probably theorems that mention infinite I should call this out, but I don't see any good notational way to indicate this that isn't confusing in the finite case.
(I'm not so sure that omega vs inf is a good notation to indicate this either. I would keep forgetting which is which.)
Mario
savask
Oct 18, 2017, 12:15:19 AM10/18/17
to Metamath
Probably theorems that mention infinite I should call this out, but I don't see any good notational way to indicate this that isn't confusing in the finite case.
My point is that probably there are not a lot of interesting theorems about the infinite case anyway. The only sane use for R^omega I can think of is defining l_p spaces, but in this case finitely supported sequences won't work.
Mario Carneiro
Oct 18, 2017, 12:27:18 AM10/18/17
to metamath
On Wed, Oct 18, 2017 at 12:15 AM, savask <sav...@yandex.ru> wrote:
Probably theorems that mention infinite I should call this out, but I don't see any good notational way to indicate this that isn't confusing in the finite case.
My point is that probably there are not a lot of interesting theorems about the infinite case anyway. The only sane use for R^omega I can think of is defining l_p spaces, but in this case finitely supported sequences won't work.
In the contrary, I think that most theorems about R^n generalize to the finitely supported R^omega, whereas R^inf is a much stranger thing. As a vector space, it is the more natural generalization, with a simple canonical basis against which all infinite dimensional vector spaces are measured. As a Hilbert space, it of course is one, and is a subspace of all the l_p spaces. So it's not so much that there are no interesting theorems about R^omega but rather that there are no *new* theorems - almost all the old theorems about finite dimensional vector spaces generalize without having to do anything extra, which is the kind of generalization I like to see (no extra work, just don't unnaturally limit yourself).
Mario
savask
Oct 18, 2017, 1:29:32 AM10/18/17
to Metamath
So it's not so much that there are no interesting theorems about R^omega but rather that there are no *new* theorems - almost all the old theorems about finite dimensional vector spaces generalize without having to do anything extra, which is the kind of generalization I like to see (no extra work, just don't unnaturally limit yourself).
I wanted to say that while some results from R^n can be generalized to finitely supported R^I for an infinite I, but they hardly will find any application. I'm just afraid that we can make the definition more convoluted and not intuitive for the means of having several "pretty" theorems which won't get used anywhere anyway. And in case if we will need "the real" R^I one day, it would rise an interesting question of picking good notation for it :-)
Maybe it's only my opinion that having a finitely supported R^I by default is a confusing convention, so of course it would be interesting to hear some other opinions.
fl
Oct 18, 2017, 7:40:22 AM10/18/17
to Metamath
Okay, so it looks like there are a few issues with MY previous proposal in MY previous email.
Nice.
The problem with all that is that you try to make a unique definition for many cases. Those with the finite
case. Those where the infinite case with no restriction is wanted. Those where the infinite case finitely supported is
intended. And anyway there are no for alternative distance and so on.
Untractable. At the end you take a sledge-hammer to crack a nut. And many other nuts have not been tried.
In fact you are not defining RR ^ N you are defining a finitely supported product of an undefinite number of copies of RR
in the standard case.
--
FL
Benoit
Oct 18, 2017, 8:31:57 AM10/18/17
to Metamath
I'll have more time to elaborate tonight, but just for now, I suggest:
- define |- RRfld = ( CCfld |`s RR ) (why wait? you cannot go wrong with this one)
- df-rrx $a |- RR^ = ( i e. _V |-> ( ( ringLMod ` RRfld ) ) ^s i ) ) $. (Mario's one-but-last proposal)
- deal with inner products later
In particular, do NOT define RR^ with the free module function (Mario's last proposal). The notation \R^I is completely standard and does NOT mean "direct sum". A common notation for direct sum is \R^{(I)} so maybe one could define " RR^() " and then write "( RR^() ` I )" for the wanted direct sum.
Both structures are important: direct sum (which is the coproduct for modules) and direct product (which is the product for modules), both are natural for different kinds of problems, and there are important theorems for both. You won't have RR^ I e. Hilb but you'll have to live with that: many categories lack products. (Even more: two objects can have different products when considered in different categories, which shows the limits of df-prds.)
As for "sSet": since it "adds an additional structure", maybe "addStruct" ?
--
Benoit
- define |- RRfld = ( CCfld |`s RR ) (why wait? you cannot go wrong with this one)
- df-rrx $a |- RR^ = ( i e. _V |-> ( ( ringLMod ` RRfld ) ) ^s i ) ) $. (Mario's one-but-last proposal)
- deal with inner products later
In particular, do NOT define RR^ with the free module function (Mario's last proposal). The notation \R^I is completely standard and does NOT mean "direct sum". A common notation for direct sum is \R^{(I)} so maybe one could define " RR^() " and then write "( RR^() ` I )" for the wanted direct sum.
Both structures are important: direct sum (which is the coproduct for modules) and direct product (which is the product for modules), both are natural for different kinds of problems, and there are important theorems for both. You won't have RR^ I e. Hilb but you'll have to live with that: many categories lack products. (Even more: two objects can have different products when considered in different categories, which shows the limits of df-prds.)
As for "sSet": since it "adds an additional structure", maybe "addStruct" ?
--
Benoit
Mario Carneiro
Oct 18, 2017, 8:48:25 AM10/18/17
to metamath
Okay, it looks like the finite support suggestion is a bust. So let's say this then:
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
We still want the toCHil function stuck in there, because it is what fixes the distance component so that you actually get the pythagorean theorem metric in the finite case, and since this is supposed to generalize JM's "Rn" this is important. In the infinite case, the distance function and inner product will fall out of domain, but the finitely supported part will still be well defined, so that we can define the direct sum version as a subspace:df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
Benoit
Oct 18, 2017, 9:27:19 AM10/18/17
to Metamath
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
Ok. (But I still think RRfld is worth it.)
df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
It would be more natural to use freeLmod, here (same definition as RR^, with freeLmod replacing ^s).
Then we will have ( RR^() ` I ) e. CHil for all I, and ( RR^() ` I ) = ( RR^ ` I ) for finite I
Yes, and this is even a characterization of finiteness.
I'm not a big fan of addStruct because that's an awfully large token for a binary operator, even if it's not used really often. How about ":=s"? This is reminiscent of the := assignment operator in some languages, with an "s" subscript like the other structure operators. An alternative is something based on the [ A / x ] ph notation, because it is very similar in spirit, taking an existing thing and modifying just one part of it to set it to something else.
Maybe (with "s" being displayed as a subscript):
class [ C / B ]s A
|- [ C / B ]s A = ( ( A |` ( _V \ ( B ` ndx ) ) u. { <. ( B ` ndx ) , C >. } )
--
Benoit
On Wed, Oct 18, 2017 at 8:31 AM, Benoit <benoit...@gmail.com> wrote:
I'll have more time to elaborate tonight, but just for now, I suggest:
- define |- RRfld = ( CCfld |`s RR ) (why wait? you cannot go wrong with this one)
- df-rrx $a |- RR^ = ( i e. _V |-> ( ( ringLMod ` RRfld ) ) ^s i ) ) $. (Mario's one-but-last proposal)
- deal with inner products later
In particular, do NOT define RR^ with the free module function (Mario's last proposal). The notation \R^I is completely standard and does NOT mean "direct sum". A common notation for direct sum is \R^{(I)} so maybe one could define " RR^() " and then write "( RR^() ` I )" for the wanted direct sum.
Both structures are important: direct sum (which is the coproduct for modules) and direct product (which is the product for modules), both are natural for different kinds of problems, and there are important theorems for both. You won't have RR^ I e. Hilb but you'll have to live with that: many categories lack products. (Even more: two objects can have different products when considered in different categories, which shows the limits of df-prds.)
As for "sSet": since it "adds an additional structure", maybe "addStruct" ?
--
Benoit
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
Norman Megill
Oct 18, 2017, 3:15:16 PM10/18/17
to Metamath
On Wednesday, October 18, 2017 at 9:27:19 AM UTC-4, Benoit wrote:
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
Ok. (But I still think RRfld is worth it.)df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
It would be more natural to use freeLmod, here (same definition as RR^, with freeLmod replacing ^s).Then we will have ( RR^() ` I ) e. CHil for all I, and ( RR^() ` I ) = ( RR^ ` I ) for finite I
Yes, and this is even a characterization of finiteness.I'm not a big fan of addStruct because that's an awfully large token for a binary operator, even if it's not used really often. How about ":=s"? This is reminiscent of the := assignment operator in some languages, with an "s" subscript like the other structure operators. An alternative is something based on the [ A / x ] ph notation, because it is very similar in spirit, taking an existing thing and modifying just one part of it to set it to something else.
Maybe (with "s" being displayed as a subscript):
class [ C / B ]s A
|- [ C / B ]s A = ( ( A |` ( _V \ ( B ` ndx ) ) u. { <. ( B ` ndx ) , C >. } )
Just a general remark.
We have always encouraged new definitions to be class constants instead of new syntax structures with arguments, unless there is a compelling reason such as the arguments can meaningfully be proper classes or one of the arguments is a bound variable. There are a handful of exceptions such as -u for unary minus, but they aren't common, and we've tried to avoid them.
Defining a function or operation or relation as a class constant gives us immediate access to our large collection of general theorems about functions, operations and relations, which we would otherwise have to prove again for the new syntax. In many cases, theorems about the operation or function itself (with no arguments) can be useful. For example, sinf, which says sin : CC --> CC, would be more awkward if we had defined "sin A" with a 1-argument syntax rather than "sin" as a class constant. Sometimes theorems can be expressed more compactly, such as dfsdom2, "~< = ( ~<_ \ `' ~<_ )".
I am used to most unfamiliar symbols being new class constants, meaning I can often parse the expression in my head without knowing the definition yet. When an unfamiliar symbol with arguments shows up, I may have to go back to its definition before I can even understand how to parse the expression.
Norm
Benoit
Oct 18, 2017, 3:49:32 PM10/18/17
to Metamath
Norm: ok, I have no strong opinion on this sSet issue (apart from finding another name) and I agree with the advantages you mention of defining new things as class constants whenever possible. Actually, I think the whole extensible structure thing is a clever hack but is very "unmathematical", and the current discussion about sSet is an illustration of this.
--
Benoit
--
Benoit
fl
Oct 18, 2017, 4:03:35 PM10/18/17
to Metamath
Norm: ok, I have no strong opinion on this sSet issue (apart from finding another name) and I agree with the advantages you mention of defining new things as class constants whenever possible. Actually, I think the whole extensible structure thing is a clever hack but is very "unmathematical", and the current discussion about sSet is an illustration of this.
It is clever but this is a hack. It looks like an object language that would have never been finished. (For reasons independent of Norm's will: set.mm is not a programming language.)
It is just the moment you realize C++ is a nice thing.
--
FL
fl
Oct 18, 2017, 4:38:42 PM10/18/17
to Metamath
But as a consequence, it has many drawbacks and limitations and it plagues the structures net.
--
FL
Cris Perdue
Oct 18, 2017, 4:51:24 PM10/18/17
to meta...@googlegroups.com, Benoit
Regarding the field of real numbers, I would be delighted for it to have its own definition.
Construction of the reals is a pretty famous connection between set theory and traditional mathematics. It seems to me that RRfld having its own definition would feel most natural for people orienting themselves to Metamath. I know I was a bit disappointed to have to look at complex numbers to get to real numbers.
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
Mario Carneiro
Oct 18, 2017, 9:28:13 PM10/18/17
to metamath
On Wed, Oct 18, 2017 at 9:27 AM, Benoit <benoit...@gmail.com> wrote:
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
Ok. (But I still think RRfld is worth it.)df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
It would be more natural to use freeLmod, here (same definition as RR^, with freeLmod replacing ^s).
One thing which I want to preserve is that ( RR^() ` I ) has the form (or is provably equal to) ( ( RR^ ` I ) |`s S ), for some S. This will make it the easiest to transfer theorems from RR^`I to RR^()`I. It's not necessary to write the set explicitly - alternatively you could just say ( ( RR^ ` I ) |`s ( Base ` ( RRfld freeLMod i ) ) ), but redoing the definition with freeLMod instead of ^s will put the toCHil application in a different place, and that won't necessarily produce the same structure, so that the relation between RR^ and RR^() becomes much more complicated and theorem transfer becomes harder.
On Wed, Oct 18, 2017 at 3:49 PM, Benoit <benoit...@gmail.com> wrote:
Norm: ok, I have no strong opinion on this sSet issue (apart from finding another name) and I agree with the advantages you mention of defining new things as class constants whenever possible. Actually, I think the whole extensible structure thing is a clever hack but is very "unmathematical", and the current discussion about sSet is an illustration of this.
That moment when you realize that formal theorem proving is more like engineering than mathematics. :)
On Wed, Oct 18, 2017 at 4:51 PM, Cris Perdue <cris....@gmail.com> wrote:
Regarding the field of real numbers, I would be delighted for it to have its own definition.Construction of the reals is a pretty famous connection between set theory and traditional mathematics. It seems to me that RRfld having its own definition would feel most natural for people orienting themselves to Metamath. I know I was a bit disappointed to have to look at complex numbers to get to real numbers.
Well, we've had the construction of the reals, as an unbundled structure, for a long time. What we didn't have is the construction of a tuple that formally satisfies the properties of a general group, ring, field, so that the general theorems apply to real numbers. I don't see that RRfld having it's own definition (in terms of CCfld) is any different from RR having its own definition in terms of CC, so it's not like your "I don't want to see CC on the way to RR" problem would at all be addressed.
Mario
Benoit
Oct 19, 2017, 10:24:45 AM10/19/17
to Metamath
As for adding a definition of RRfld: we have discussed its advantages: for some, important, for others, minor. But what about the drawbacks? I can't really see them...
That moment when you realize that formal theorem proving is more like engineering than mathematics. :)
Does this have to be the case? I mean, maybe formal theorem *proving* is more like engineering, but the end-result (the $a and $p statements, as opposed to the proofs) can still be closer to mathematics than to programming. This should even be one of the priorities of formal mathematics according to e.g. "The QED manifesto revisited" by Freek. Of course, a mathematical object is necessarily different from its representation in a computer, but extensible structures are a bit of a stretch. If you ask around what a group is, you'll get: "it's a set with a binary operation such that..." (or better, "it's a set with a binary operation, a constant, and a unary operation such that..."), but you won't have many "it's a function f from a subset of \N to classes such that f(0) is a set, f(1) is a binary operation on f(0), f(2) \in f(0)...".
--
Benoit
David Starner
Oct 19, 2017, 10:39:31 AM10/19/17
to meta...@googlegroups.com
On Thu, Oct 19, 2017 at 7:24 AM Benoit <benoit...@gmail.com> wrote:
Of course, a mathematical object is necessarily different from its representation in a computer, but extensible structures are a bit of a stretch. If you ask around what a group is, you'll get: "it's a set with a binary operation such that..." (or better, "it's a set with a binary operation, a constant, and a unary operation such that..."), but you won't have many "it's a function f from a subset of \N to classes such that f(0) is a set, f(1) is a binary operation on f(0), f(2) \in f(0)...".
What does it mean to be a set with a binary operation? If we're talking about proving something in set theory, a group can't be a set with a binary operation. If a group is a single mathematical object, it is a set. This set may be an ordered set, under some definition of an ordered set, of multiple sets, but that's not any less arbitrary then a function from a subset of N to classes (under some definition of function).
savask
Oct 19, 2017, 10:39:33 AM10/19/17
to Metamath
Of course, a mathematical object is necessarily different from its representation in a computer, but extensible structures are a bit of a stretch. If you ask around what a group is, you'll get: "it's a set with a binary operation such that..." (or better, "it's a set with a binary operation, a constant, and a unary operation such that..."), but you won't have many "it's a function f from a subset of \N to classes such that f(0) is a set, f(1) is a binary operation on f(0), f(2) \in f(0)...".
Personally I like thinking about extensible structures as an analogue of models in mathematical logic: the set of natural numbers serves as a common signature for all types of objects we want to define, and the "structure" itself is just an interpretation function. So people saying that a group is a set equipped with a binary operation are no further from metamath than they are from logicians.
Benoit
Oct 19, 2017, 11:52:09 AM10/19/17
to Metamath
What does it mean to be a set with a binary operation?
You can read in most textbooks: "A group is a couple (G, * ) where G is a set and * is a binary operation on G such that...". If you want to stay close to mathematical practice, then in metamath you define (I do it for magmas for simplicity):
wisMagma $a wff isMagma A $.
df-isMagma $a |- ( isMagma A <-> E. x E. y ( A = <. x , y >. /\ y : ( x X. x ) --> x ) ) $.
--
Benoit
Mario Carneiro
Oct 19, 2017, 12:07:50 PM10/19/17
to metamath
This is actually the approach that predates extensible structures in Metamath. The reason we moved away from it is simple, and is right in the name: it's not extensible to new components. If a group is just a pair, then it can't have any additional data beyond what is relevant for group theory, but this is limiting if you want to say that a ring is a group because it's not technically true - you have to say something much more cumbersome like
If <A,B,C> is a ring, then <A,B> is a group--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
Dan Connolly
Oct 19, 2017, 12:17:08 PM10/19/17
to Metamath
On Oct 18, 2017 2:15 PM, "Norman Megill" <n...@alum.mit.edu> wrote:
On Wednesday, October 18, 2017 at 9:27:19 AM UTC-4, Benoit wrote:
Maybe (with "s" being displayed as a subscript):
class [ C / B ]s A
|- [ C / B ]s A = ( ( A |` ( _V \ ( B ` ndx ) ) u. { <. ( B ` ndx ) , C >. } )Just a general remark.We have always encouraged new definitions to be class constants instead of new syntax structures with arguments,
sUpdate comes to mind, as in updating a record in a functional programming language.
Benoit
Oct 19, 2017, 12:47:54 PM10/19/17
to Metamath
If a group is just a pair, then it can't have any additional data beyond what is relevant for group theory
Yes, that's the point.
but this is limiting if you want to say that a ring is a group because it's not technically true
Yes, and this is fortunate: indeed, a ring is not a group.
- you have to say something much more cumbersome likeIf <A,B,C> is a ring, then <A,B> is a group
Indeed, my idea was to define the (object component of the) appropriate functors, e.g., in pseudo-metamath,
$a |- RingToGroup = ( <. x , y , z >. e. Ring |-> <. x , y >. )
$p |- RingToGroup : Ring --> Group
I realize it is more cumbersome and makes life harder, but it also looks neater. I also understand your point of view, and maybe my suggestion would hamper too much further development of set.mm (but again: what are the objectives of this development?).
> maximize the use of the "identity coercion" to produce hierarchies of literal subclasses Monoid C_ Group C_ Ring C_ DivRing C_ Field etc.
You probably meant it in the other direction, but the inclusion Ring C_ Group is abusive.
--
Benoit
--
Benoit
Norman Megill
Oct 19, 2017, 12:48:51 PM10/19/17
to Metamath
The problem with the textbook definition is that on the one hand it is claimed that every ring is a group, for example, yet a group is defined as a binary pair and a ring as a triple, so no ring can actually be a group under that definition. Of course we informally "know" what is meant, but Metamath needs precise definitions. So we define a group as any ordered n-tuple (n >= 2) with the first two members having the textbook properties. It is really that simple. Perhaps that is a hack, but I don't see how there could be anything simpler that would let us say, "every ring is a group" and thus reuse for rings all of the theorems we developed for groups.
Over time, additional ways to access and manipulate structure members were introduced for convenience. For example, "( Base ` ndx )" returns the slot number of the Base component to avoid hard-coded numbers for referencing the components. sSet is another example. While they are very useful for our purposes, they are unfamiliar to mathematicians and may make the structure-related functions seem like hacks.
Of course we are always looking for better names for things and appreciate your input. For example, I have come to think that Carrier might be a better word than Base. I can't remember now why I picked Base. Books rarely have either term, but simply use the same letter for the carrier set as for the group itself, relying on context to distinguish the two.
Norm
Over time, additional ways to access and manipulate structure members were introduced for convenience. For example, "( Base ` ndx )" returns the slot number of the Base component to avoid hard-coded numbers for referencing the components. sSet is another example. While they are very useful for our purposes, they are unfamiliar to mathematicians and may make the structure-related functions seem like hacks.
Of course we are always looking for better names for things and appreciate your input. For example, I have come to think that Carrier might be a better word than Base. I can't remember now why I picked Base. Books rarely have either term, but simply use the same letter for the carrier set as for the group itself, relying on context to distinguish the two.
Norm
Benoit
Oct 19, 2017, 1:11:48 PM10/19/17
to Metamath
The problem with the textbook definition is that on the one hand it is claimed that every ring is a group
Then we have not been reading the same textbooks ! The phrase "the additive group of a/the ring" is pretty common, and this is what I implemented with the function RingToGroup (the object component of a functor).
but I don't see how there could be anything simpler that would let us say, "every ring is a group"
But I don't want to let you say this ;-)
Anyway, I understand your point of view and how this simplifies things (our previous messages were simultaneous and probably crossed).
--
Benoit
Mario Carneiro
Oct 19, 2017, 1:19:39 PM10/19/17
to metamath
On Thu, Oct 19, 2017 at 12:47 PM, Benoit <benoit...@gmail.com> wrote:
If a group is just a pair, then it can't have any additional data beyond what is relevant for group theory
Yes, that's the point.but this is limiting if you want to say that a ring is a group because it's not technically true
Yes, and this is fortunate: indeed, a ring is not a group.- you have to say something much more cumbersome likeIf <A,B,C> is a ring, then <A,B> is a group
Indeed, my idea was to define the (object component of the) appropriate functors, e.g., in pseudo-metamath,
$a |- RingToGroup = ( <. x , y , z >. e. Ring |-> <. x , y >. )
$p |- RingToGroup : Ring --> Group
I realize it is more cumbersome and makes life harder, but it also looks neater. I also understand your point of view, and maybe my suggestion would hamper too much further development of set.mm (but again: what are the objectives of this development?).
The objectives, as always, are to make group theory, ring theory, etc as well developed as possible within themselves, but also maximize "communication" between the different fields of abstract algebra and between abstract algebra and concrete instantiations. Some encoding decisions need to be made in order to make progress; but they should make everything work well together and limit the cognitive load of the user trying to make use of the library.
What of compositions? I really wouldn't want to have to talk about (GroupToMonoid ` (RingToGroup ` (DivRingToRing ` (FieldToDivRing ` F)))). But adding even more functions for the compositions leads to a quadratic growth of coercion functions, each of which needs a nontrivial number of translation theorems saying what maps to what. As it is now, the quadratic growth is limited to simple theorems like (F e. Field -> F e. Monoid), which have easy two step proofs and don't require any other supporting material.
> maximize the use of the "identity coercion" to produce hierarchies of literal subclasses Monoid C_ Group C_ Ring C_ DivRing C_ Field etc.
You probably meant it in the other direction, but the inclusion Ring C_ Group is abusive.
If you think that the identity subtype coercion is abusive, perhaps you should look into type theory instead of Metamath's untyped foundations.
I want to reiterate that this is a pragmatic decision, made for extramathematical reasons (although in a sense, helping mathematicians do their jobs better has mathematical import). It is *convenient* to talk about a vector space using group terminology because it is a group in an obvious sense, and inserting a gigantic token just for this is just obfuscating the obvious for no clear gain.
Maybe considering the gain is a more profitable angle here. Do you agree that (abusive though it may be) using the identity function instead of an explicit coercion is strictly easier (produces shorter proofs and less symbols) when it is possible to do so? I use explicit coercions only when there is a barrier of some kind to the use of the identity coercion, as with mulGrp (the barrier here being that there are two structures that ring inherits from and they can't both be interpreted as subclassing). If you use coercions for everything instead, what do you gain, besides "purity" (which doesn't assist in proof building)? Especially in a system as austere as Metamath (nothing is hidden), purity comes at a high price, and I've not seen convincing evidence that it helps people get the job done.
Mario
fl
Oct 19, 2017, 1:32:25 PM10/19/17
to Metamath
Perhaps that is a hack, but I don't see how there could be anything simpler that would let us say, "every ring is a group" and thus reuse for rings all of the theorems we developed for groups.
It is also a monoid for the multiplication and there is no way to inherit the properties of a monoid.That it the reason why it is a hack.
See Mario's remark about diamond inheritance. I suppose we could continue and see what polymorphism and encapsulation
could mean in that case and see they are not respected either.
--
FL
Norman Megill
Oct 19, 2017, 1:48:51 PM10/19/17
to Metamath
On Thursday, October 19, 2017 at 1:11:48 PM UTC-4, Benoit wrote:
The problem with the textbook definition is that on the one hand it is claimed that every ring is a group
Then we have not been reading the same textbooks ! The phrase "the additive group of a/the ring" is pretty common, and this is what I implemented with the function RingToGroup (the object component of a functor).
I think I have seen the definition "a ring is a group with an additional operation..." though maybe not with exactly with those words, not sure. Anyway, that is probably not a great example because we don't ordinarily think of rings as specialized groups. A better example might be "a star ring is a ring with involution", which adds an additional component to a ring. I think we would typically think of star rings as specialized rings.
Norm
Benoit
Oct 19, 2017, 6:15:11 PM10/19/17
to Metamath
Thanks for your answers. I know I'm being a bit stubborn, but it's to understand better the constraints specific to set.mm.
Mario: you suggest looking at type theories, do you know something similar to metamath but "typed", that I could look at? Would it be possible/interesting to emulate (some flavor of) type theory in metamath (as a project disjoint from set.mm, of course) ?
In your previous post, you ask: "what's the gain, besides purity"? To me, purity is a gain in itself ! Where can purity be found, if not in metamath ? Do you really want to shatter my last dreams ?
Norm: I know it's vague, but I have no problem with "a ring is a group with an additional operation such that..." (same as "a group is a set with a binary operation such that...") because it is written informallly and it is understood that this should be formalized as a tuple, but on the other hand, I'm not comfortable with "every ring is a group" (maybe it's just me being too rigid). Your example of star-rings is better: it would be a bit extreme to say "we call a star-ring commutative if its underlying ring is commutative", or similarly "we call a topological group compact if its underlying topological space is compact".
As for the names:
sSet |-> no idea
Base |-> I think Base is better than "Carrier"; the most descriptive phrase would be "underlying set", but it's long and has two words; there is also Ground (though it's rather used for the ground ring in linear algebra)
mulGrp |-> this is problematic, since the multiplicative group of a ring is generally understood to be its group of units; maybe mulMnd, since it will most often yield a monoid ?
Ok with Mario's proposals for RR^ and RR^()
--
Benoit
Mario: you suggest looking at type theories, do you know something similar to metamath but "typed", that I could look at? Would it be possible/interesting to emulate (some flavor of) type theory in metamath (as a project disjoint from set.mm, of course) ?
In your previous post, you ask: "what's the gain, besides purity"? To me, purity is a gain in itself ! Where can purity be found, if not in metamath ? Do you really want to shatter my last dreams ?
Norm: I know it's vague, but I have no problem with "a ring is a group with an additional operation such that..." (same as "a group is a set with a binary operation such that...") because it is written informallly and it is understood that this should be formalized as a tuple, but on the other hand, I'm not comfortable with "every ring is a group" (maybe it's just me being too rigid). Your example of star-rings is better: it would be a bit extreme to say "we call a star-ring commutative if its underlying ring is commutative", or similarly "we call a topological group compact if its underlying topological space is compact".
As for the names:
sSet |-> no idea
Base |-> I think Base is better than "Carrier"; the most descriptive phrase would be "underlying set", but it's long and has two words; there is also Ground (though it's rather used for the ground ring in linear algebra)
mulGrp |-> this is problematic, since the multiplicative group of a ring is generally understood to be its group of units; maybe mulMnd, since it will most often yield a monoid ?
Ok with Mario's proposals for RR^ and RR^()
--
Benoit
David Starner
Oct 19, 2017, 9:59:09 PM10/19/17
to meta...@googlegroups.com
On Thu, Oct 19, 2017 at 8:52 AM Benoit <benoit...@gmail.com> wrote:
What does it mean to be a set with a binary operation?
You can read in most textbooks: "A group is a couple (G, * ) where G is a set and * is a binary operation on G such that...".
And what's a couple but a function with domain (1, 2)?
Benoit
Oct 20, 2017, 5:03:56 AM10/20/17
to Metamath
And what's a couple but a function with domain (1, 2)?
Of course this emulates a couple (you probably meant {1, 2}), with evaluation at 1 being the first component, etc. And of course extensible structures correctly emulate the usual structures (which is the least we can ask of an implementation), I never said the contrary: I even said it was a clever implementation. But this is not really the point.
fl
Oct 20, 2017, 12:12:06 PM10/20/17
to Metamath
Of course we are always looking for better names for things and appreciate your input. For example, I have come to think that Carrier might be a better word than Base. I can't remember now why I picked Base.
The set on which the strucure is "based", I guess.
Carrier is used by Mizar.
All those debates are somewhat byzantine in my opinion.
--
FL
Reply all
Reply to author
Forward
0 new messages