Affine maps #
This file defines affine maps.
Main definitions #
AffineMapis the type of affine maps between two affine spaces with the same ringk. Various basic examples of affine maps are defined, includingconst,id,lineMapandhomothety.
Notations #
P1 →ᵃ[k] P2is a notation forAffineMap k P1 P2;AffineSpace V P: a localized notation forAddTorsor V Pdefined 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
structure
AffineMap
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
{V2 : Type u_4}
(P2 : Type u_5)
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
Type (max (max (max u_2 u_3) u_4) u_5)
- 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
def
LinearMap.toAffineMap
{k : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddCommGroup V₂]
[Module k V₂]
(f : V₁ →ₗ[k] V₂)
:
Reinterpret a linear map as an affine map.
Instances For
@[simp]
theorem
LinearMap.coe_toAffineMap
{k : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddCommGroup V₂]
[Module k V₂]
(f : V₁ →ₗ[k] V₂)
:
↑(LinearMap.toAffineMap f) = ↑f
@[simp]
theorem
LinearMap.toAffineMap_linear
{k : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddCommGroup V₂]
[Module k V₂]
(f : V₁ →ₗ[k] V₂)
:
(LinearMap.toAffineMap f).linear = f
@[simp]
theorem
AffineMap.coe_mk
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 → P2)
(linear : V1 →ₗ[k] V2)
(add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = ↑linear v +ᵥ f p)
:
↑{ toFun := f, linear := linear, map_vadd' := add } = f
Constructing an affine map and coercing back to a function produces the same map.
@[simp]
theorem
AffineMap.toFun_eq_coe
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
f.toFun = ↑f
toFun is the same as the result of coercing to a function.
@[simp]
theorem
AffineMap.map_vadd
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
(p : P1)
(v : V1)
:
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.
@[simp]
theorem
AffineMap.linearMap_vsub
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
(p1 : P1)
(p2 : P1)
:
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.
theorem
AffineMap.ext
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
{f : P1 →ᵃ[k] P2}
{g : P1 →ᵃ[k] P2}
(h : ∀ (p : P1), ↑f p = ↑g p)
:
f = g
Two affine maps are equal if they coerce to the same function.
theorem
AffineMap.coeFn_injective
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
Function.Injective FunLike.coe
@[simp]
theorem
AffineMap.coe_const
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(p : P2)
:
↑(AffineMap.const k P1 p) = Function.const P1 p
@[simp]
theorem
AffineMap.const_apply
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(p : P2)
(q : P1)
:
↑(AffineMap.const k P1 p) q = p
@[simp]
theorem
AffineMap.const_linear
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(p : P2)
:
(AffineMap.const k P1 p).linear = 0
theorem
AffineMap.linear_eq_zero_iff_exists_const
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
f.linear = 0 ↔ ∃ q, f = AffineMap.const k P1 q
def
AffineMap.mk'
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 → P2)
(f' : V1 →ₗ[k] V2)
(p : P1)
(h : ∀ (p' : P1), f p' = ↑f' (p' -ᵥ p) +ᵥ f p)
:
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
@[simp]
theorem
AffineMap.coe_mk'
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 → P2)
(f' : V1 →ₗ[k] V2)
(p : P1)
(h : ∀ (p' : P1), f p' = ↑f' (p' -ᵥ p) +ᵥ f p)
:
↑(AffineMap.mk' f f' p h) = f
@[simp]
theorem
AffineMap.mk'_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 → P2)
(f' : V1 →ₗ[k] V2)
(p : P1)
(h : ∀ (p' : P1), f p' = ↑f' (p' -ᵥ p) +ᵥ f p)
:
(AffineMap.mk' f f' p h).linear = f'
instance
AffineMap.mulAction
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
{R : Type u_10}
[Monoid R]
[DistribMulAction R V2]
[SMulCommClass k R V2]
:
The space of affine maps to a module inherits an R-action from the action on its codomain.
@[simp]
theorem
AffineMap.coe_smul
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
{R : Type u_10}
[Monoid R]
[DistribMulAction R V2]
[SMulCommClass k R V2]
(c : R)
(f : P1 →ᵃ[k] V2)
:
@[simp]
theorem
AffineMap.smul_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
{R : Type u_10}
[Monoid R]
[DistribMulAction R V2]
[SMulCommClass k R V2]
(t : R)
(f : P1 →ᵃ[k] V2)
:
instance
AffineMap.isCentralScalar
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
{R : Type u_10}
[Monoid R]
[DistribMulAction R V2]
[SMulCommClass k R V2]
[DistribMulAction Rᵐᵒᵖ V2]
[IsCentralScalar R V2]
:
IsCentralScalar R (P1 →ᵃ[k] V2)
instance
AffineMap.instZeroAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
instance
AffineMap.instAddAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
instance
AffineMap.instSubAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
instance
AffineMap.instNegAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
@[simp]
theorem
AffineMap.coe_zero
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
↑0 = 0
@[simp]
theorem
AffineMap.zero_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
0.linear = 0
instance
AffineMap.instAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
:
AddCommGroup (P1 →ᵃ[k] V2)
The set of affine maps to a vector space is an additive commutative group.
instance
AffineMap.instAddTorsorAffineMapAddGroupIsAddTorsorToAddGroupAffineMapToAddGroupInstAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
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.
@[simp]
@[simp]
@[simp]
theorem
AffineMap.coe_fst
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
↑AffineMap.fst = Prod.fst
@[simp]
theorem
AffineMap.fst_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
AffineMap.fst.linear = LinearMap.fst k V1 V2
@[simp]
theorem
AffineMap.coe_snd
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
↑AffineMap.snd = Prod.snd
@[simp]
theorem
AffineMap.snd_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
:
AffineMap.snd.linear = LinearMap.snd k V1 V2
@[simp]
theorem
AffineMap.coe_id
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
↑(AffineMap.id k P1) = id
The identity affine map acts as the identity.
@[simp]
theorem
AffineMap.id_linear
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
(AffineMap.id k P1).linear = LinearMap.id
theorem
AffineMap.id_apply
(k : Type u_1)
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p : P1)
:
↑(AffineMap.id k P1) p = p
The identity affine map acts as the identity.
def
AffineMap.comp
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
{V3 : Type u_6}
{P3 : Type u_7}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
[AddCommGroup V3]
[Module k V3]
[AddTorsor V3 P3]
(f : P2 →ᵃ[k] P3)
(g : P1 →ᵃ[k] P2)
:
Composition of affine maps.
Instances For
@[simp]
theorem
AffineMap.coe_comp
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
{V3 : Type u_6}
{P3 : Type u_7}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
[AddCommGroup V3]
[Module k V3]
[AddTorsor V3 P3]
(f : P2 →ᵃ[k] P3)
(g : P1 →ᵃ[k] P2)
:
↑(AffineMap.comp f g) = ↑f ∘ ↑g
Composition of affine maps acts as applying the two functions.
theorem
AffineMap.comp_apply
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
{V3 : Type u_6}
{P3 : Type u_7}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
[AddCommGroup V3]
[Module k V3]
[AddTorsor V3 P3]
(f : P2 →ᵃ[k] P3)
(g : P1 →ᵃ[k] P2)
(p : P1)
:
↑(AffineMap.comp f g) p = ↑f (↑g p)
Composition of affine maps acts as applying the two functions.
@[simp]
theorem
AffineMap.comp_id
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
AffineMap.comp f (AffineMap.id k P1) = f
@[simp]
theorem
AffineMap.id_comp
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
AffineMap.comp (AffineMap.id k P2) f = f
theorem
AffineMap.comp_assoc
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
{V3 : Type u_6}
{P3 : Type u_7}
{V4 : Type u_8}
{P4 : Type u_9}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
[AddCommGroup V3]
[Module k V3]
[AddTorsor V3 P3]
[AddCommGroup V4]
[Module k V4]
[AddTorsor V4 P4]
(f₃₄ : P3 →ᵃ[k] P4)
(f₂₃ : P2 →ᵃ[k] P3)
(f₁₂ : P1 →ᵃ[k] P2)
:
AffineMap.comp (AffineMap.comp f₃₄ f₂₃) f₁₂ = AffineMap.comp f₃₄ (AffineMap.comp f₂₃ f₁₂)
@[simp]
theorem
AffineMap.coe_one
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
↑1 = id
@[simp]
theorem
AffineMap.linear_injective_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
Function.Injective ↑f.linear ↔ Function.Injective ↑f
@[simp]
theorem
AffineMap.linear_surjective_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
Function.Surjective ↑f.linear ↔ Function.Surjective ↑f
@[simp]
theorem
AffineMap.linear_bijective_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
:
Function.Bijective ↑f.linear ↔ Function.Bijective ↑f
Definition of AffineMap.lineMap and lemmas about it #
theorem
AffineMap.coe_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
:
↑(AffineMap.lineMap p₀ p₁) = fun c => c • (p₁ -ᵥ p₀) +ᵥ p₀
theorem
AffineMap.lineMap_apply
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
↑(AffineMap.lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀
theorem
AffineMap.lineMap_apply_module'
{k : Type u_1}
{V1 : Type u_2}
[Ring k]
[AddCommGroup V1]
[Module k V1]
(p₀ : V1)
(p₁ : V1)
(c : k)
:
↑(AffineMap.lineMap p₀ p₁) c = c • (p₁ - p₀) + p₀
theorem
AffineMap.lineMap_apply_module
{k : Type u_1}
{V1 : Type u_2}
[Ring k]
[AddCommGroup V1]
[Module k V1]
(p₀ : V1)
(p₁ : V1)
(c : k)
:
theorem
AffineMap.lineMap_apply_ring'
{k : Type u_1}
[Ring k]
(a : k)
(b : k)
(c : k)
:
↑(AffineMap.lineMap a b) c = c * (b - a) + a
theorem
AffineMap.lineMap_vadd_apply
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p : P1)
(v : V1)
(c : k)
:
↑(AffineMap.lineMap p (v +ᵥ p)) c = c • v +ᵥ p
@[simp]
theorem
AffineMap.lineMap_linear
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
:
(AffineMap.lineMap p₀ p₁).linear = LinearMap.smulRight LinearMap.id (p₁ -ᵥ p₀)
theorem
AffineMap.lineMap_same_apply
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p : P1)
(c : k)
:
↑(AffineMap.lineMap p p) c = p
@[simp]
theorem
AffineMap.lineMap_same
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p : P1)
:
AffineMap.lineMap p p = AffineMap.const k k p
@[simp]
theorem
AffineMap.lineMap_apply_zero
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
:
↑(AffineMap.lineMap p₀ p₁) 0 = p₀
@[simp]
theorem
AffineMap.lineMap_apply_one
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
:
↑(AffineMap.lineMap p₀ p₁) 1 = p₁
@[simp]
theorem
AffineMap.lineMap_eq_lineMap_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[NoZeroSMulDivisors k V1]
{p₀ : P1}
{p₁ : P1}
{c₁ : k}
{c₂ : k}
:
↑(AffineMap.lineMap p₀ p₁) c₁ = ↑(AffineMap.lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
@[simp]
theorem
AffineMap.lineMap_eq_left_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[NoZeroSMulDivisors k V1]
{p₀ : P1}
{p₁ : P1}
{c : k}
:
@[simp]
theorem
AffineMap.lineMap_eq_right_iff
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[NoZeroSMulDivisors k V1]
{p₀ : P1}
{p₁ : P1}
{c : k}
:
theorem
AffineMap.lineMap_injective
(k : Type u_1)
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[NoZeroSMulDivisors k V1]
{p₀ : P1}
{p₁ : P1}
(h : p₀ ≠ p₁)
:
Function.Injective ↑(AffineMap.lineMap p₀ p₁)
@[simp]
theorem
AffineMap.apply_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
(p₀ : P1)
(p₁ : P1)
(c : k)
:
↑f (↑(AffineMap.lineMap p₀ p₁) c) = ↑(AffineMap.lineMap (↑f p₀) (↑f p₁)) c
@[simp]
theorem
AffineMap.comp_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(f : P1 →ᵃ[k] P2)
(p₀ : P1)
(p₁ : P1)
:
AffineMap.comp f (AffineMap.lineMap p₀ p₁) = AffineMap.lineMap (↑f p₀) (↑f p₁)
@[simp]
theorem
AffineMap.fst_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(p₀ : P1 × P2)
(p₁ : P1 × P2)
(c : k)
:
(↑(AffineMap.lineMap p₀ p₁) c).fst = ↑(AffineMap.lineMap p₀.fst p₁.fst) c
@[simp]
theorem
AffineMap.snd_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
{V2 : Type u_4}
{P2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V2]
[AddTorsor V2 P2]
(p₀ : P1 × P2)
(p₁ : P1 × P2)
(c : k)
:
(↑(AffineMap.lineMap p₀ p₁) c).snd = ↑(AffineMap.lineMap p₀.snd p₁.snd) c
theorem
AffineMap.lineMap_symm
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
:
AffineMap.lineMap p₀ p₁ = AffineMap.comp (AffineMap.lineMap p₁ p₀) (AffineMap.lineMap 1 0)
theorem
AffineMap.lineMap_apply_one_sub
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
↑(AffineMap.lineMap p₀ p₁) (1 - c) = ↑(AffineMap.lineMap p₁ p₀) c
@[simp]
theorem
AffineMap.lineMap_vsub_left
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
↑(AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)
@[simp]
theorem
AffineMap.left_vsub_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
p₀ -ᵥ ↑(AffineMap.lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)
@[simp]
theorem
AffineMap.lineMap_vsub_right
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
@[simp]
theorem
AffineMap.right_vsub_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₀ : P1)
(p₁ : P1)
(c : k)
:
theorem
AffineMap.lineMap_vadd_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(v₁ : V1)
(v₂ : V1)
(p₁ : P1)
(p₂ : P1)
(c : k)
:
↑(AffineMap.lineMap v₁ v₂) c +ᵥ ↑(AffineMap.lineMap p₁ p₂) c = ↑(AffineMap.lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c
theorem
AffineMap.lineMap_vsub_lineMap
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
(p₁ : P1)
(p₂ : P1)
(p₃ : P1)
(p₄ : P1)
(c : k)
:
↑(AffineMap.lineMap p₁ p₂) c -ᵥ ↑(AffineMap.lineMap p₃ p₄) c = ↑(AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c
theorem
AffineMap.decomp
{k : Type u_1}
{V1 : Type u_2}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddCommGroup V2]
[Module k V2]
(f : V1 →ᵃ[k] V2)
:
Decomposition of an affine map in the special case when the point space and vector space are the same.
theorem
AffineMap.decomp'
{k : Type u_1}
{V1 : Type u_2}
{V2 : Type u_4}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddCommGroup V2]
[Module k V2]
(f : V1 →ᵃ[k] V2)
:
Decomposition of an affine map in the special case when the point space and vector space are the same.
theorem
AffineMap.image_uIcc
{k : Type u_10}
[LinearOrderedField k]
(f : k →ᵃ[k] k)
(a : k)
(b : k)
:
@[simp]
theorem
AffineMap.proj_apply
{k : Type u_1}
[Ring k]
{ι : Type u_10}
{V : ι → Type u_11}
{P : ι → Type u_12}
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
[(i : ι) → AddTorsor (V i) (P i)]
(i : ι)
(f : (i : ι) → P i)
:
↑(AffineMap.proj i) f = f i
@[simp]
theorem
AffineMap.proj_linear
{k : Type u_1}
[Ring k]
{ι : Type u_10}
{V : ι → Type u_11}
{P : ι → Type u_12}
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
[(i : ι) → AddTorsor (V i) (P i)]
(i : ι)
:
(AffineMap.proj i).linear = LinearMap.proj i
theorem
AffineMap.pi_lineMap_apply
{k : Type u_1}
[Ring k]
{ι : Type u_10}
{V : ι → Type u_11}
{P : ι → Type u_12}
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
[(i : ι) → AddTorsor (V i) (P i)]
(f : (i : ι) → P i)
(g : (i : ι) → P i)
(c : k)
(i : ι)
:
↑(AffineMap.lineMap f g) c i = ↑(AffineMap.lineMap (f i) (g i)) c
instance
AffineMap.distribMulAction
{R : Type u_1}
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
{V2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V1]
[Module k V2]
[Monoid R]
[DistribMulAction R V2]
[SMulCommClass k R V2]
:
DistribMulAction R (P1 →ᵃ[k] V2)
The space of affine maps to a module inherits an R-action from the action on its codomain.
instance
AffineMap.instModuleAffineMapAddGroupIsAddTorsorToAddGroupToAddCommMonoidInstAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup
{R : Type u_1}
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
{V2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[AddCommGroup V2]
[Module k V1]
[Module k V2]
[Semiring R]
[Module R V2]
[SMulCommClass k R V2]
:
The space of affine maps taking values in an R-module is an R-module.
@[simp]
theorem
AffineMap.toConstProdLinearMap_apply
(R : Type u_1)
{k : Type u_2}
{V1 : Type u_3}
{V2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[AddCommGroup V2]
[Module k V1]
[Module k V2]
[Semiring R]
[Module R V2]
[SMulCommClass k R V2]
(f : V1 →ᵃ[k] V2)
:
↑(AffineMap.toConstProdLinearMap R) f = (↑f 0, f.linear)
@[simp]
theorem
AffineMap.toConstProdLinearMap_symm_apply
(R : Type u_1)
{k : Type u_2}
{V1 : Type u_3}
{V2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[AddCommGroup V2]
[Module k V1]
[Module k V2]
[Semiring R]
[Module R V2]
[SMulCommClass k R V2]
(p : V2 × (V1 →ₗ[k] V2))
:
↑(LinearEquiv.symm (AffineMap.toConstProdLinearMap R)) p = LinearMap.toAffineMap p.snd + AffineMap.const k V1 p.fst
def
AffineMap.toConstProdLinearMap
(R : Type u_1)
{k : Type u_2}
{V1 : Type u_3}
{V2 : Type u_5}
[Ring k]
[AddCommGroup V1]
[AddCommGroup V2]
[Module k V1]
[Module k V2]
[Semiring R]
[Module R V2]
[SMulCommClass k R V2]
:
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
theorem
AffineMap.homothety_def
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r : k)
:
AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c
theorem
AffineMap.homothety_apply
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r : k)
(p : P1)
:
↑(AffineMap.homothety c r) p = r • (p -ᵥ c) +ᵥ c
theorem
AffineMap.homothety_eq_lineMap
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r : k)
(p : P1)
:
↑(AffineMap.homothety c r) p = ↑(AffineMap.lineMap c p) r
@[simp]
theorem
AffineMap.homothety_one
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
:
AffineMap.homothety c 1 = AffineMap.id k P1
@[simp]
theorem
AffineMap.homothety_apply_same
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r : k)
:
↑(AffineMap.homothety c r) c = c
theorem
AffineMap.homothety_mul_apply
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r₁ : k)
(r₂ : k)
(p : P1)
:
↑(AffineMap.homothety c (r₁ * r₂)) p = ↑(AffineMap.homothety c r₁) (↑(AffineMap.homothety c r₂) p)
theorem
AffineMap.homothety_mul
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r₁ : k)
(r₂ : k)
:
AffineMap.homothety c (r₁ * r₂) = AffineMap.comp (AffineMap.homothety c r₁) (AffineMap.homothety c r₂)
@[simp]
theorem
AffineMap.homothety_zero
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
:
AffineMap.homothety c 0 = AffineMap.const k P1 c
@[simp]
theorem
AffineMap.homothety_add
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
(r₁ : k)
(r₂ : k)
:
AffineMap.homothety c (r₁ + r₂) = r₁ • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.homothety c r₂
@[simp]
theorem
AffineMap.coe_homothetyHom
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
:
@[simp]
theorem
AffineMap.coe_homothetyAffine
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[CommRing k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
(c : P1)
:
theorem
Convex.combo_affine_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[Ring 𝕜]
[AddCommGroup E]
[AddCommGroup F]
[Module 𝕜 E]
[Module 𝕜 F]
{x : E}
{y : E}
{a : 𝕜}
{b : 𝕜}
{f : E →ᵃ[𝕜] F}
(h : a + b = 1)
:
Applying an affine map to an affine combination of two points yields an affine combination of the images.