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.Normed.Affine.AddTorsor
and
Topology.Algebra.Affine
.
References #
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
.
- toFun : P1 → P2
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AffineMap.instFunLike k P1 P2 = { coe := AffineMap.toFun, coe_injective' := ⋯ }
Reinterpret a linear map as an affine map.
Equations
- f.toAffineMap = { toFun := ⇑f, linear := f, map_vadd' := ⋯ }
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.
Two affine maps are equal if they have equal linear maps and are equal at some point.
Two affine maps are equal if they have equal linear maps and are equal at some point.
The constant function as an AffineMap
.
Equations
- AffineMap.const k P1 p = { toFun := Function.const P1 p, linear := 0, map_vadd' := ⋯ }
Instances For
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
.
Equations
- AffineMap.mk' f f' p h = { toFun := f, linear := f', map_vadd' := ⋯ }
Instances For
The space of affine maps to a module inherits an R
-action from the action on its codomain.
Equations
- AffineMap.mulAction = MulAction.mk ⋯ ⋯
Equations
- ⋯ = ⋯
The set of affine maps to a vector space is an additive commutative group.
Equations
- AffineMap.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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
.
Equations
- AffineMap.instAddTorsor = AddTorsor.mk ⋯ ⋯
Equations
- AffineMap.fst = { toFun := Prod.fst, linear := LinearMap.fst k V1 V2, map_vadd' := ⋯ }
Instances For
Equations
- AffineMap.snd = { toFun := Prod.snd, linear := LinearMap.snd k V1 V2, map_vadd' := ⋯ }
Instances For
Identity map as an affine map.
Equations
- AffineMap.id k P1 = { toFun := id, linear := LinearMap.id, map_vadd' := ⋯ }
Instances For
The identity affine map acts as the identity.
The identity affine map acts as the identity.
Equations
- AffineMap.instInhabited = { default := AffineMap.id k P1 }
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.
AffineMap.linear
on endomorphisms is a MonoidHom
.
Equations
- AffineMap.linearHom = { toFun := AffineMap.linear, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Definition of AffineMap.lineMap
and lemmas about it #
The affine map from k
to P1
sending 0
to p₀
and 1
to p₁
.
Equations
- AffineMap.lineMap p₀ p₁ = (LinearMap.id.smulRight (p₁ -ᵥ p₀)).toAffineMap +ᵥ AffineMap.const k k p₀
Instances For
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.
Evaluation at a point as an affine map.
Equations
- AffineMap.proj i = { toFun := fun (f : (i : ι) → P i) => f i, linear := LinearMap.proj i, map_vadd' := ⋯ }
Instances For
The space of affine maps to a module inherits an R
-action from the action on its codomain.
Equations
- AffineMap.distribMulAction = DistribMulAction.mk ⋯ ⋯
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]
Equations
- One or more equations did not get rendered due to their size.
Instances For
pi
construction for affine maps. From a family of affine maps it produces an affine
map into a family of affine spaces.
This is the affine version of LinearMap.pi
.
Equations
- AffineMap.pi f = { toFun := fun (m : P1) (a : ι) => (f a) m, linear := LinearMap.pi fun (a : ι) => (f a).linear, map_vadd' := ⋯ }
Instances For
Two affine maps from a Pi-tyoe of modules (i : ι) → φv i
are equal if they are equal in their
operation on Pi.single
and at zero. Analogous to LinearMap.pi_ext
. See also pi_ext_nonempty
,
which instead of agreement at zero requires Nonempty ι
.
Two affine maps from a Pi-tyoe of modules (i : ι) → φv i
are equal if they are equal in their
operation on Pi.single
and ι
is nonempty. Analogous to LinearMap.pi_ext
. See also
pi_ext_zero
, which instead Nonempty ι
requires agreement at 0.
This is used as the ext lemma instead of AffineMap.pi_ext_nonempty
for reasons explained in
note [partially-applied ext lemmas]. Analogous to LinearMap.pi_ext'
homothety c r
is the homothety (also known as dilation) about c
with scale factor r
.
Equations
- AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c
Instances For
homothety
as a multiplicative monoid homomorphism.
Equations
- AffineMap.homothetyHom c = { toFun := AffineMap.homothety c, map_one' := ⋯, map_mul' := ⋯ }
Instances For
homothety
as an affine map.
Equations
- AffineMap.homothetyAffine c = { toFun := AffineMap.homothety c, linear := (LinearMap.lsmul k (P1 →ᵃ[k] V1)).flip (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c), map_vadd' := ⋯ }
Instances For
Applying an affine map to an affine combination of two points yields an affine combination of the images.