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.
