Geometry: origin and unit points

[Thierry Arnoux]

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

[Mario Carneiro]

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.

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/B590B30A-90AB-4377-A2FB-315035FA468B%40gmx.net.

[Thierry Arnoux]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStXHMGGtx88qOFdAi%3D%2Bs0vBkjKDb4b8_5K7tcFPCjL_Vg%40mail.gmail.com.

[Mario Carneiro]

Yes, that's exactly right. I agree that it's best to build the whole real vector space in one go.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/FB476846-81C3-4AFD-8F23-247D1B7B2B95%40gmx.net.

[Thierry Arnoux]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvq_FVQTV7WBKWnY4U6ybx8ZM_bYWCwACY2y41_JtgDtA%40mail.gmail.com.