5.4. Barycenters

This page is under construction.

Vector spaces

Linear geometry can be conceived as equivalent to affine geometry with an additional constant symbol 0 called origin or zero (no additional axiom could be relevant since affine groups have only one orbit): This does not formalize linear geometry, as we did not formalize affine geometry here assumed. Optimal formalizations of linear geometry do not even go this way, but logically come first, as affine geometry can be more usefully formalized using it.
Indeed, affine subspaces F of vector spaces E are still affine spaces: affine structures of F are definable from linear structures of E with the choice of F, in the sense that the group GF⊂GLE of automorphisms of E which preserve F, is morphed by restriction into Aff F.
Now for this to form an equivalent presentation of the affine geometry of F, this morphism from GF to Aff F must be bijective:

Basis of affine spaces

Now let us start a proper formalization of affine and linear geometries in terms of basis.
A fundamental feature of affine geometry is that for any n∈ℕ, n-dimensional spaces have basis of n+1 elements, and any point belongs to some basis. Then a possible presentation of linear geometry (but not the most formally convenient),

The barycenter of points x and y with coefficients (1-a) and a is the image of a by the unique affine map from ℝ to M which sends 0 to x and 1 to y.

Ratio of lengths of parallel segments; middles of segments, are defined from barycenters. The notion of segment; equivalently, the 3-ary relation of betweenness B∈[AC], and the notion of (straight) half-line. This is a specificity of the use of (a real closed fields) as opposed to other fields such as ℂ.

k-dimensional subspaces are generated by a set of k+1 points but not generated by any set of k points or less.

Affine forms

An affine form on an affine space M is an affine map from M to ℝ.
A coordinates system is a tuple of affine forms.

More detailed study of affine geometry in another page.


Preimages of 0 (or any number) by non-constant affine forms, are the closed hyperplanes.
Up: 5. Geometry

Homepage : Set Theory and Foundations of Mathematics