This page is under construction.
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.
- A vector space is an affine
space E with a chosen point 0E called "origin"
- A linear map between vector spaces E and F
is an affine map f such that f(0E) = 0F.
- A subspace of a vector space E is an affine subspace of E containing
0E (so by definition, each subspace is an affine subspace but not conversely)
- Subspaces can be used in the role of directions, as any direction contains a unique subspace.
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:
- 0E∉F (gives surjectivity : the choice of 0E
is not structuring for F).
- Then F must be an hyperplane (to give injectivity).
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.
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
Set Theory and Foundations of Mathematics