Ok, let’s say this is the working assumption then. There are more developments to come before defining the distance, so there is still time for more discussions. _ Thierry
> Le 23 mai 2019 à 14:56, Mario Carneiro <[email protected]> a écrit : > > 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. >> >> -- >> 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. > > -- > 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. -- 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/02F0DBA0-1752-4052-8C8B-AA744E880E92%40gmx.net.
