Yes, that's exactly right. I agree that it's best to build the whole real vector space in one go.
On Thu, May 23, 2019 at 2:41 AM Thierry Arnoux <[email protected]> wrote: > Hi Mario, > > Restating, just to make sure I understand: > > Your proposal is a “metric geometry” builder, which would take a Tarski > geometry, two reference points, and *overwrite* the ‘dist’ slot with a > metric built from those two points. We could e.g. use sSet for that. > The resulting structure would still be a geometry (we would have to prove > that of course), but ‘dist’ would have actual useful values in RR. > Ok, I assume this may work. > > I believe we may also consider, with the same function, setting also > * the group addition with a vector addition that considers points as > vectors originating from 0 and 0 as the null element, > * the scalars with the reals (Ccfld |’s RR) > * the scalar multiplication with vector multiplication. > I believe this should equip the geometry with a vector space structure. > > BR, > _ > Thierry > > Le 23 mai 2019 à 13:55, Mario Carneiro <[email protected]> a écrit : > > The reason the congruence was put in the dist slot is so that if the space > happens to already have a proper metric, it will agree with the geometry by > definition. In this case, I think the most practically useful approach is > to just start saying "dist is a metric" at some point in the development. > You can say "but wait we've lost generality" and that's true, but the point > of "the construction" is to show that once you have all of Tarski's axioms > the space of possible distances is isomorphic to RR, so it's not actually a > loss to say that it is RR. > > But somehow this is less than satisfying, since this is basically bringing > in a whole bunch more axioms unrelated to Tarski's, which are conservative > but we haven't shown it, so we've cheated in a sense. Where is the space > for a proof? What can be done is to have a structure builder that takes a > "pure-Tarski" geometric space and a unit segment in it, and produces a real > geometric space on the same set of points. Now you can prove that the > constructed real geometry is isomorphic to the original geometry, and the > unit segment has length 1 in the real geometry. > > On Thu, May 23, 2019 at 1:44 AM Thierry Arnoux <[email protected]> > wrote: > >> Hi all, >> >> Later on in the development of elementary geometry, we shall be able to >> define the “length” of a segment. This goes by comparing the segment with a >> reference unitary segment. The question is “where does the unitary segment >> come from?”. It is not part of Tarski’s axioms. I have two proposals here: >> >> - I believe we will have to define this “Unit” as two new slots (one for >> a zero, one for a one), since they cannot be derived from other slots. One >> may also think about a way to introduce multi dimensional coordinates here. >> >> - Thanks to those, we shall be able to derive a distance function. >> Retrospectively, I think the choice of ‘ dist ‘ for the congruence relation >> might be problematic here, since the constructed geometric distance shall >> really be the structure’s ‘ dist ‘ slot. It might be better to define a new >> slot for congruence, to avoid the conflict. >> >> An alternative would be to define the distance builder as a function of >> the geometry and the two unit points, which itself builds a distance >> operation. This would be nearer to the development of Schwabhaeuser, who >> uses “oe” (0- Einheit) indices everywhere (ch14 and ch15), but seems more >> complicated. >> >> Any thoughts? >> BR, >> _ >> Thierry >> >> -- >> 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 [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/B590B30A-90AB-4377-A2FB-315035FA468B%40gmx.net >> . >> > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJStXHMGGtx88qOFdAi%3D%2Bs0vBkjKDb4b8_5K7tcFPCjL_Vg%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJStXHMGGtx88qOFdAi%3D%2Bs0vBkjKDb4b8_5K7tcFPCjL_Vg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/FB476846-81C3-4AFD-8F23-247D1B7B2B95%40gmx.net > <https://groups.google.com/d/msgid/metamath/FB476846-81C3-4AFD-8F23-247D1B7B2B95%40gmx.net?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvq_FVQTV7WBKWnY4U6ybx8ZM_bYWCwACY2y41_JtgDtA%40mail.gmail.com.
