Affine maps #
This file defines affine maps.
Main definitions #
AffineMap
is the type of affine maps between two affine spaces with the same ringk
. Various basic examples of affine maps are defined, includingconst
,id
,lineMap
andhomothety
.
Notations #
P1 →ᵃ[k] P2
is a notation forAffineMap k P1 P2
;AffineSpace V P
: a localized notation forAddTorsor V P
defined inLinearAlgebra.AffineSpace.Basic
.
Implementation notes #
outParam
is used in the definition of [AddTorsor V P]
to make V
an implicit argument
(deduced from P
) in most cases. 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.NormedSpace.AddTorsor
and
Topology.Algebra.Affine
.
References #
- https://en.wikipedia.org/wiki/Affine_space
- https://en.wikipedia.org/wiki/Principal_homogeneous_space
- toFun : P1 → P2
- map_vadd' : ∀ (p : P1) (v : V1), AffineMap.toFun s (v +ᵥ p) = ↑s.linear v +ᵥ AffineMap.toFun s p
An AffineMap k P1 P2
(notation: P1 →ᵃ[k] P2
) is a map from P1
to P2
that
induces a corresponding linear map from V1
to V2
.
Instances For
An AffineMap k P1 P2
(notation: P1 →ᵃ[k] P2
) is a map from P1
to P2
that
induces a corresponding linear map from V1
to V2
.
Instances For
Reinterpret a linear map as an affine map.
Instances For
Constructing an affine map and coercing back to a function produces the same map.
toFun
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.
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
.
Instances For
The space of affine maps to a module inherits an R
-action from the action on its codomain.
The set of affine maps to a vector space is an additive commutative group.
The space of affine maps from P1
to P2
is an affine space over the space of affine maps
from P1
to the vector space V2
corresponding to P2
.
The identity affine map acts as the identity.
The identity affine map acts as the identity.
Composition of affine maps.
Instances For
Composition of affine maps acts as applying the two functions.
Composition of affine maps acts as applying the two functions.
Definition of AffineMap.lineMap
and lemmas about it #
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.
The space of affine maps to a module inherits an R
-action from the action on its codomain.
The space of affine maps taking values in an R
-module is an R
-module.
The space of affine maps between two modules is linearly equivalent to the product of the
domain with the space of linear maps, by taking the value of the affine map at (0 : V1)
and the
linear part.
See note [bundled maps over different rings]
Instances For
Applying an affine map to an affine combination of two points yields an affine combination of the images.