derived smooth geometry
Euclidean geometry studies the geometry of Euclidean spaces. These spaces come equipped with a canonical Riemannian metric, and Euclidean geometry can be regarded as the local model for Riemannian geometry, in some sense.
Euclidean geometry in the sense of the Idea section makes reference to the extrinsic notion of real number (to delineate the notion of Euclidean space) and whatever surrounding structure is used to found that notion, but it has also received more intrinsic axiomatic treatments in the spirit of synthetic geometry. Notable among these are Hilbert's axioms, as set out in his Grundlagen der Geometrie, and Tarski’s axioms, which form a first-order axiomatic theory.
Here we will just give an extremely sketchy description (for now, see Wikipedia for a fuller account). It should be said right away that two of the Hilbert axioms are not first-order.
Hilbert’s theory has
Six relations: betweenness (a ternary relation on points), three incidence relations (one for points and lines, one for points and planes, one for lines and planes), and two congruence relations (a relation on points whose intuitive meaning is that the the line segment is congruent to the line segment , and a relation on points whose intuitive meaning is that the angle is congruent to the angle );
A bunch of axioms (20 or 21 depending on which specific edition or translation or exposition one is working with; Wikipedia says 20 but actually has, confusingly, 21 – see the Talk page for more information). They are organized as
I (Todd Trimble) assume Hilbert’s theory is, or is at least intended to be, categorical in the model-theoretic sense, at least considered against a fixed set-theoretic background. In other words I assume the real numbers as complete ordered field would be a definable structure and the axioms are uniquely modeled by with its Euclidean structure.
Tarski’s theory EPG (Elementary Plane [Euclidean] Geometry) is a one-sorted theory in first-order logic with equality, with variables representing points. There are no constants or operations in the signature, and just two relations:
A ternary relation (betweenness), with meaning is between and ( is on the line segment between and ) – we will write instead to conserve space;
A 4-ary relation (congruence), with meaning that a line segment is congruent (of the same length) as . For readability, we write this as .
The theory can be presented (in some sense very parsimoniously) by 10 axioms and one first-order axiom scheme. Axioms 8 and 9 constrain the dimension to (Euclidean plane geometry), but there are analogues of 8 and 9 that constrain the dimension to any chosen number. Axiom 10 is an extremely disguised version of the Parallel Postulate, with a complicated history behind it. The axiom scheme 11 plays the role of a Dedekind cut axiom expressed in first-order terms.
(segment construction: given a line segment and a line from to , one can extend that line in that direction by a segment congruent to ),
(5 segment axiom),
(Pasch axiom: roughly, if a line goes through one side of a triangle and not through a vertex, then it must go through another side),
(there exist three non-collinear points: the dimension is at least 2),
(if three points are each equidistant from two given distinct points and , then those three points are collinear: the dimension is at most 2),
(Parallel Postulate (!)),
(Cut schema) Let be a formula in which variables do not occur freely, and let be a formula in which do not occur freely. Then
(if every element in the set defined by lies beyond every element in the set defined by as seen from the perspective of , then there is some between every such and every such ).
See Tarski-Givant for a thorough discussion of this and related axiom systems, and an extensive bibliography.
One important aspect of the meta-theory lies in the relation of models of this theory to real closed fields. If is a real closed field, then there is a corresponding model of EPG whose underlying set is and where the relations and are interpreted by expected conditions:
It is mostly straightforward to verify that this structure on satisfies the EPG axioms (all but the cut schema hold for any ordered field). More importantly,
For every model of EPG there is a real closed field such that as models.
Of course there is some arbitrariness involved in the choice of isomorphism; for example, any line segment can be used to stipulate a unit length and a coordinate axis. The proof is lightly sketched in Tarski; again only the first ten axioms are needed to produce an ordered field structure on , with the cut schema being used to verify the real closure.
The significance of this result is that EPG is a complete and decidable theory, just as the theory of real closed fields is complete and decidable. Hence there exists an algorithm which, on being fed a sentence in the language of Elementary Plane Geometry, will produce a proof of the sentence or a proof of its negation in the theory.
|gauge group||stabilizer subgroup||local model space||local geometry||global geometry||differential cohomology||first order formulation of gravity|
|general||Lie group/algebraic group||subgroup (monomorphism)||quotient (“coset space”)||Klein geometry||Cartan geometry||Cartan connection|
|examples||Euclidean group||rotation group||Cartesian space||Euclidean geometry||Riemannian geometry||affine connection||Euclidean gravity|
|Poincaré group||Lorentz group||Minkowski space||Lorentzian geometry||pseudo-Riemannian geometry||spin connection||Einstein gravity|
|super Poincaré group||spin group||super Minkowski spacetime||Lorentzian supergeometry||supergeometry||superconnection||supergravity|
|linear algebraic group||parabolic subgroup/Borel subgroup||flag variety||parabolic geometry|
|orthochronous Lorentz group||conformal geometry||conformal connection||conformal gravity|
|general||smooth 2-group||2-monomorphism||homotopy quotient||Klein 2-geometry||Cartan 2-geometry|
|cohesive ∞-group||∞-monomorphism (i.e. any homomorphism)||homotopy quotient of ∞-action||higher Klein geometry||higher Cartan geometry||higher Cartan connection|
|examples||extended super Minkowski spacetime||extended supergeometry||higher supergravity: type II, heterotic, 11d|
Alfred Tarski, What is elementary geometry?, in The axiomatic method. With special reference to geometry and physics Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958 (ed. L. Henkin, P. Suppes, and A. Tarski), Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland (1959), pp. 16–29. (pdf)
After a famous saying attributed to Hilbert which in some sense heralds the axiomatic spirit. ↩