Affine spaces
This file defines affine spaces (over modules) and subspaces, affine
maps, and the affine span of a set of points. For affine combinations
of points, see linear_algebra.affine_space.combination. For
affinely independent families of points, see
linear_algebra.affine_space.independent. For some additional
results relating to finite-dimensional subspaces of affine spaces, see
linear_algebra.affine_space.finite_dimensional.
Main definitions
affine_space V Pis an abbreviation foradd_torsor V Pin the case ofmodule k V.Pis the type of points in the space andVthek-module of displacement vectors. Definitions and results not depending on themodulestructure appear inalgebra.add_torsorinstead of here; that includes the instance of anadd_groupas anadd_torsorover itself, which thus gives amoduleas anaffine_spaceover itself. Definitions of affine spaces vary as to whether a space with no points is permitted; here, we require a nonempty type of points (via the definition of torsors requiring a nonempty type). Affine spaces are defined over any module, with stronger type class requirements onkbeing used for individual lemmas where needed.affine_subspace k Pis the type of affine subspaces. Unlike affine spaces, affine subspaces are allowed to be empty, and lemmas that do not apply to empty affine subspaces havenonemptyhypotheses. There is acomplete_latticestructure on affine subspaces.affine_subspace.directiongives thesubmodulespanned by the pairwise differences of points in anaffine_subspace. There are various lemmas relating to the set of vectors in thedirection, and relating the lattice structure on affine subspaces to that on their directions.affine_spangives the affine subspace spanned by a set of points, withvector_spangiving its direction.affine_spanis defined in terms ofspan_points, which gives an explicit description of the points contained in the affine span;span_pointsitself should generally only be used when that description is required, withaffine_spanbeing the main definition for other purposes. Two other descriptions of the affine span are proved equivalent: it is theInfof affine subspaces containing the points, and (if[nontrivial k]) it contains exactly those points that are affine combinations of points in the given set.affine_mapis the type of affine maps between two affine spaces with the same ringk. Various basic examples of affine maps are defined, includingconst,id,line_mapandhomothety.
Implementation notes
out_param is used to make V an implicit argument (deduced from
P) in most cases; include V is needed in many cases for V, and
type classes using it, to be added as implicit arguments to
individual lemmas. As for modules, k is an explicit argument rather
than implied by P or V.
This file only provides purely algebraic definitions and results.
Those depending on analysis or topology are defined elsewhere; see
analysis.normed_space.add_torsor and topology.algebra.affine.
TODO: Some key definitions are not yet present.
- Coercions from an
affine_subspaceto the subtype of its points, and a correspondingaffine_spaceinstance on that subtype in the case of a nonempty subspace. affine_equiv(see issue #2909).- Affine frames. An affine frame might perhaps be represented as an
affine_equivto afinsupp(in the general case) or function type (in the finite-dimensional case) that gives the coordinates, with appropriate proofs of existence whenkis a field. - Although results on affine combinations implicitly provide barycentric frames and coordinates, there is no explicit representation of the map from a point to its coordinates.
References
- https://en.wikipedia.org/wiki/Affine_space
- https://en.wikipedia.org/wiki/Principal_homogeneous_space
The submodule spanning the differences of a (possibly empty) set of points.
Equations
- vector_span k s = submodule.span k (vsub_set s)
The definition of vector_span, for rewriting.
The vector_span of the empty set is ⊥.
The vector_span of a single point is ⊥.
The vsub_set lies within the vector_span.
Each pairwise difference is in the vector_span.
The points in the affine span of a (possibly empty) set of
points. Use affine_span instead to get an affine_subspace k P.
Equations
- span_points k s = {p : P | ∃ (p1 : P) (H : p1 ∈ s) (v : V) (H : v ∈ vector_span k s), p = v +ᵥ p1}
A point in a set is in its affine span.
A set is contained in its span_points.
The span_points of a set is nonempty if and only if that set
is.
Adding a point in the affine span and a vector in the spanning submodule produces a point in the affine span.
Subtracting two points in the affine span produces a vector in the spanning submodule.
- carrier : set P
- smul_vsub_vadd_mem : ∀ (c_1 : k) {p1 p2 p3 : P}, p1 ∈ c.carrier → p2 ∈ c.carrier → p3 ∈ c.carrier → c_1 • (p1 -ᵥ p2) +ᵥ p3 ∈ c.carrier
An affine_subspace k P is a subset of an affine_space V P
that, if not empty, has an affine space structure induced by a
corresponding subspace of the module k V.
Equations
- affine_subspace.has_coe k P = {coe := affine_subspace.carrier _inst_4}
Equations
- affine_subspace.has_mem k P = {mem := λ (p : P) (s : affine_subspace k P), p ∈ ↑s}
A point is in an affine subspace coerced to a set if and only if it is in that affine subspace.
The direction of an affine subspace is the submodule spanned by the pairwise differences of points. (Except in the case of an empty affine subspace, where the direction is the zero submodule, every vector in the direction is the difference of two points in the affine subspace.)
Equations
- s.direction = vector_span k ↑s
The direction equals the vector_span.
Alternative definition of the direction when the affine subspace
is nonempty. This is defined so that the order on submodules (as used
in the definition of submodule.span) can be used in the proof of
coe_direction_eq_vsub_set, and is not intended to be used beyond
that proof.
direction_of_nonempty gives the same submodule as
direction.
The set of vectors in the direction of a nonempty affine subspace
is given by vsub_set.
A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction of two vectors in the subspace.
Adding a vector in the direction to a point in the subspace produces a point in the subspace.
Subtracting two points in the subspace produces a vector in the direction.
Adding a vector to a point in a subspace produces a point in the subspace if and only if the vector is in the direction.
Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the right.
Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the left.
Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the right.
Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the left.
Given a point in an affine subspace, a result of subtracting that point on the right is in the direction if and only if the other point is in the subspace.
Given a point in an affine subspace, a result of subtracting that point on the left is in the direction if and only if the other point is in the subspace.
Two affine subspaces are equal if they have the same points.
Two affine subspaces with the same direction and nonempty intersection are equal.
Construct an affine subspace from a point and a direction.
Equations
- affine_subspace.mk' p direction = {carrier := {q : P | ∃ (v : V) (H : v ∈ direction), q = v +ᵥ p}, smul_vsub_vadd_mem := _}
An affine subspace constructed from a point and a direction contains that point.
An affine subspace constructed from a point and a direction contains the result of adding a vector in that direction to that point.
An affine subspace constructed from a point and a direction is nonempty.
The direction of an affine subspace constructed from a point and a direction.
Constructing an affine subspace from a point in a subspace and that subspace's direction yields the original subspace.
If an affine subspace contains a set of points, it contains the
span_points of that set.
The affine span of a set of points is the smallest affine subspace containing those points. (Actually defined here in terms of spans in modules.)
Equations
- affine_span k s = {carrier := span_points k s, smul_vsub_vadd_mem := _}
The affine span, converted to a set, is span_points.
The direction of the affine span is the vector_span.
A point in a set is in its affine span.
Equations
- affine_subspace.complete_lattice = {sup := λ (s1 s2 : affine_subspace k P), affine_span k (↑s1 ∪ ↑s2), le := partial_order.le (partial_order.lift coe affine_subspace.complete_lattice._proof_1), lt := partial_order.lt (partial_order.lift coe affine_subspace.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (s1 s2 : affine_subspace k P), {carrier := ↑s1 ∩ ↑s2, smul_vsub_vadd_mem := _}, inf_le_left := _, inf_le_right := _, le_inf := _, top := {carrier := set.univ P, smul_vsub_vadd_mem := _}, le_top := _, bot := {carrier := ∅, smul_vsub_vadd_mem := _}, bot_le := _, Sup := λ (s : set (affine_subspace k P)), affine_span k (⋃ (s' : affine_subspace k P) (H : s' ∈ s), ↑s'), Inf := λ (s : set (affine_subspace k P)), {carrier := ⋂ (s' : affine_subspace k P) (H : s' ∈ s), ↑s', smul_vsub_vadd_mem := _}, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
Equations
The ≤ order on subspaces is the same as that on the corresponding
sets.
One subspace is less than or equal to another if and only if all its points are in the second subspace.
The < order on subspaces is the same as that on the corresponding
sets.
One subspace is not less than or equal to another if and only if it has a point not in the second subspace.
If a subspace is less than another, there is a point only in the second.
A subspace is less than another if and only if it is less than or equal to the second subspace and there is a point only in the second.
The affine span is the Inf of subspaces containing the given
points.
The Galois insertion formed by affine_span and coercion back to
a set.
Equations
- affine_subspace.gi k V P = {choice := λ (s : set P) (_x : ↑(affine_span k s) ≤ s), affine_span k s, gc := _, le_l_u := _, choice_eq := _}
The span of the empty set is ⊥.
The span of univ is ⊤.
The affine span of a single point, coerced to a set, contains just that point.
A point is in the affine span of a single point if and only if they are equal.
The span of a union of sets is the sup of their spans.
The span of a union of an indexed family of sets is the sup of their spans.
⊤, coerced to a set, is the whole set of points.
All points are in ⊤.
The direction of ⊤ is the whole module as a submodule.
⊥, coerced to a set, is the empty set.
No points are in ⊥.
The direction of ⊥ is the submodule ⊥.
A nonempty affine subspace is ⊤ if and only if its direction is
⊤.
The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of points.
A point is in the inf of two affine subspaces if and only if it is in both of them.
The direction of the inf of two affine subspaces is less than or equal to the inf of their directions.
If two affine subspaces have a point in common, the direction of their inf equals the inf of their directions.
If two affine subspaces have a point in their inf, the direction of their inf equals the inf of their directions.
If one affine subspace is less than or equal to another, the same applies to their directions.
If one nonempty affine subspace is less than another, the same applies to their directions
The sup of the directions of two affine subspaces is less than or equal to the direction of their sup.
The sup of the directions of two nonempty affine subspaces with empty intersection is less than the direction of their sup.
If the directions of two nonempty affine subspaces span the whole module, they have nonempty intersection.
If the directions of two nonempty affine subspaces are complements of each other, they intersect in exactly one point.
Coercing a subspace to a set then taking the affine span produces the original subspace.
The vector_span is the span of the pairwise subtractions with a
given point on the left.
The vector_span is the span of the pairwise subtractions with a
given point on the right.
The vector_span is the span of the pairwise subtractions with a
given point on the left, excluding the subtraction of that point from
itself.
The vector_span is the span of the pairwise subtractions with a
given point on the right, excluding the subtraction of that point from
itself.
The vector_span of the image of a function is the span of the
pairwise subtractions with a given point on the left, excluding the
subtraction of that point from itself.
The vector_span of the image of a function is the span of the
pairwise subtractions with a given point on the right, excluding the
subtraction of that point from itself.
The vector_span of an indexed family is the span of the pairwise
subtractions with a given point on the left.
The vector_span of an indexed family is the span of the pairwise
subtractions with a given point on the right.
The affine span of a set is nonempty if and only if that set is.
Suppose a set of vectors spans V. Then a point p, together
with those vectors added to p, spans P.
The direction of the sup of two nonempty affine subspaces is the sup of the two directions and of any one difference between points in the two subspaces.
The direction of the span of the result of adding a point to a nonempty affine subspace is the sup of the direction of that subspace and of any one difference between that point and a point in the subspace.
Given a point p1 in an affine subspace s, and a point p2, a
point p is in the span of s with p2 added if and only if it is a
multiple of p2 -ᵥ p1 added to a point in s.
- to_fun : P1 → P2
- linear : V1 →ₗ[k] V2
- map_vadd' : ∀ (p : P1) (v : V1), c.to_fun (v +ᵥ p) = ⇑(c.linear) v +ᵥ c.to_fun p
An affine_map k P1 P2 is a map from P1 to P2 that
induces a corresponding linear map from V1 to V2.
Equations
- affine_map.has_coe_to_fun = {F := λ (x : affine_map k P1 P2), P1 → P2, coe := affine_map.to_fun _inst_7}
Constructing an affine map and coercing back to a function produces the same map.
to_fun is the same as the result of coercing to a function.
An affine map on the result of adding a vector to a point produces the same result as the linear map applied to that vector, added to the affine map applied to that point.
The linear map on the result of subtracting two points is the result of subtracting the result of the affine map on those two points.
Two affine maps are equal if they coerce to the same function.
Constant function as an affine_map.
Equations
- affine_map.const k P1 p = {to_fun := function.const P1 p, linear := 0, map_vadd' := _}
Equations
Construct an affine map by verifying the relation between the map and its linear part at one
base point. Namely, this function takes a map f : P₁ → P₂, a linear map f' : V₁ →ₗ[k] V₂, and
a point p such that for any other point p' we have f p' = f' (p' -ᵥ p) +ᵥ f p.
The set of affine maps to a vector space is an additive commutative group.
Equations
- affine_map.add_comm_group = {add := λ (f g : affine_map k P1 V2), {to_fun := ⇑f + ⇑g, linear := f.linear + g.linear, map_vadd' := _}, add_assoc := _, zero := {to_fun := 0, linear := 0, map_vadd' := _}, zero_add := _, add_zero := _, neg := λ (f : affine_map k P1 V2), {to_fun := -⇑f, linear := -f.linear, map_vadd' := _}, add_left_neg := _, add_comm := _}
The space of affine maps from P1 to P2 is an affine space over the space of affine spaces
from P1 to the vector V2 corresponding to P2.
Equations
- affine_map.add_torsor = {vadd := λ (f : affine_map k P1 V2) (g : affine_map k P1 P2), {to_fun := λ (p : P1), ⇑f p +ᵥ ⇑g p, linear := f.linear + g.linear, map_vadd' := _}, zero_vadd' := _, vadd_assoc' := _, vsub := λ (f g : affine_map k P1 P2), {to_fun := λ (p : P1), ⇑f p -ᵥ ⇑g p, linear := f.linear - g.linear, map_vadd' := _}, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}
Identity map as an affine map.
Equations
- affine_map.id k P1 = {to_fun := id P1, linear := linear_map.id _inst_3, map_vadd' := _}
The identity affine map acts as the identity.
The identity affine map acts as the identity.
Equations
- affine_map.inhabited = {default := affine_map.id k P1 _inst_4}
Composition of affine maps.
Composition of affine maps acts as applying the two functions.
Composition of affine maps acts as applying the two functions.
Equations
- affine_map.monoid = {mul := affine_map.comp _inst_4, mul_assoc := _, one := affine_map.id k P1 _inst_4, one_mul := _, mul_one := _}
The affine map from k to P1 sending 0 to p and 1 to v +ᵥ p.
Equations
- affine_map.line_map p v = {to_fun := λ (c : k), c • v +ᵥ p, linear := linear_map.id.smul_right v, map_vadd' := _}
Decomposition of an affine map in the special case when the point space and vector space are the same.
Decomposition of an affine map in the special case when the point space and vector space are the same.
If k is a commutative ring, then the set of affine maps with codomain in a k-module
is a k-module.
Equations
- affine_map.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : k) (f : affine_map k P1 V2), {to_fun := c • ⇑f, linear := c • f.linear, map_vadd' := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
homothety c r is the homothety about c with scale factor r.
Equations
- affine_map.homothety c r = r • (affine_map.id k P1 -ᵥ affine_map.const k P1 c) +ᵥ affine_map.const k P1 c
homothety as a multiplicative monoid homomorphism.
Equations
- affine_map.homothety_hom c = {to_fun := affine_map.homothety c, map_one' := _, map_mul' := _}
homothety as an affine map.
Equations
- affine_map.homothety_affine c = {to_fun := affine_map.homothety c, linear := ⇑((linear_map.lsmul k (affine_map k P1 V1)).flip) (affine_map.id k P1 -ᵥ affine_map.const k P1 c), map_vadd' := _}
Reinterpret a linear map as an affine map.