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.Normed.Affine.AddTorsor and
Topology.Algebra.Affine.
References #
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)
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
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]
(self : P1 →ᵃ[k] P2)
(p : P1)
(v : V1)
:
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
instance
AffineMap.instFunLike
(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]
:
Equations
- AffineMap.instFunLike k P1 P2 = { coe := AffineMap.toFun, coe_injective' := ⋯ }
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.
Equations
- f.toAffineMap = { toFun := ⇑f, linear := f, map_vadd' := ⋯ }
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₂)
:
⇑f.toAffineMap = ⇑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₂)
:
f.toAffineMap.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 DFunLike.coe
theorem
AffineMap.ext_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 →ᵃ[k] P2}
{g : P1 →ᵃ[k] P2}
(h₁ : f.linear = g.linear)
{p : P1}
(h₂ : f p = g p)
:
f = g
Two affine maps are equal if they have equal linear maps and are equal at some point.
theorem
AffineMap.ext_linear_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}
{g : P1 →ᵃ[k] P2}
:
Two affine maps are equal if they have equal linear maps and are equal at some point.
def
AffineMap.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)
:
The constant function as an AffineMap.
Equations
- AffineMap.const k P1 p = { toFun := Function.const P1 p, linear := 0, map_vadd' := ⋯ }
Instances For
@[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 : P2), 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.
Equations
- AffineMap.mk' f f' p h = { toFun := f, linear := f', map_vadd' := ⋯ }
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.
Equations
- AffineMap.mulAction = MulAction.mk ⋯ ⋯
@[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)
Equations
- ⋯ = ⋯
instance
AffineMap.instAdd
{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.instSub
{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.instNeg
{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]
:
AffineMap.linear 0 = 0
instance
AffineMap.instAddCommGroup
{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.
Equations
- AffineMap.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
AffineMap.instAddTorsor
{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.
Equations
- AffineMap.instAddTorsor = AddTorsor.mk ⋯ ⋯
@[simp]
@[simp]
def
AffineMap.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]
:
Equations
- AffineMap.fst = { toFun := Prod.fst, linear := LinearMap.fst k V1 V2, map_vadd' := ⋯ }
Instances For
@[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
def
AffineMap.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]
:
Equations
- AffineMap.snd = { toFun := Prod.snd, linear := LinearMap.snd k V1 V2, map_vadd' := ⋯ }
Instances For
@[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
def
AffineMap.id
(k : Type u_1)
{V1 : Type u_2}
(P1 : Type u_3)
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
Identity map as an affine map.
Equations
- AffineMap.id k P1 = { toFun := id, linear := LinearMap.id, map_vadd' := ⋯ }
Instances For
@[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.
instance
AffineMap.instInhabited
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
Equations
- AffineMap.instInhabited = { default := AffineMap.id k P1 }
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)
:
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)
:
(f.comp 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)
:
f.comp (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.id k P2).comp 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)
:
(f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp 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
def
AffineMap.linearHom
{k : Type u_1}
{V1 : Type u_2}
{P1 : Type u_3}
[Ring k]
[AddCommGroup V1]
[Module k V1]
[AddTorsor V1 P1]
:
AffineMap.linear on endomorphisms is a MonoidHom.
Equations
- AffineMap.linearHom = { toFun := AffineMap.linear, map_one' := ⋯, map_mul' := ⋯ }
Instances For
@[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 #
def
AffineMap.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)
:
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
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 : k) => 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.id.smulRight (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)
:
f.comp (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).1 = (AffineMap.lineMap p₀.1 p₁.1) 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).2 = (AffineMap.lineMap p₀.2 p₁.2) 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.lineMap p₁ p₀).comp (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
@[simp]
theorem
AffineMap.lineMap_lineMap_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)
(d : k)
:
(AffineMap.lineMap p₀ ((AffineMap.lineMap p₀ p₁) c)) d = (AffineMap.lineMap p₀ p₁) (d * c)
@[simp]
theorem
AffineMap.lineMap_lineMap_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)
(d : k)
:
(AffineMap.lineMap ((AffineMap.lineMap p₀ p₁) c) p₁) d = (AffineMap.lineMap p₀ p₁) (1 - (1 - d) * (1 - 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)
:
def
AffineMap.proj
{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 : ι)
:
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
@[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.
Equations
- AffineMap.distribMulAction = DistribMulAction.mk ⋯ ⋯
instance
AffineMap.instModule
{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.
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]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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))
:
(AffineMap.toConstProdLinearMap R).symm p = p.2.toAffineMap + AffineMap.const k V1 p.1
@[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)
def
AffineMap.pi
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
{ι : Type u_9}
{φv : ι → Type u_10}
{φp : ι → Type u_11}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[(i : ι) → AddTorsor (φv i) (φp i)]
(f : (i : ι) → P1 →ᵃ[k] φp i)
:
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
@[simp]
theorem
AffineMap.pi_apply
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
{ι : Type u_9}
{φv : ι → Type u_10}
{φp : ι → Type u_11}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[(i : ι) → AddTorsor (φv i) (φp i)]
(fp : (i : ι) → P1 →ᵃ[k] φp i)
(c : P1)
(i : ι)
:
(AffineMap.pi fp) c i = (fp i) c
theorem
AffineMap.pi_comp
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
{V3 : Type u_7}
{P3 : Type u_8}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[AddCommGroup V3]
[AddTorsor V3 P3]
[Module k V1]
[Module k V3]
{ι : Type u_9}
{φv : ι → Type u_10}
{φp : ι → Type u_11}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[(i : ι) → AddTorsor (φv i) (φp i)]
(fp : (i : ι) → P1 →ᵃ[k] φp i)
(g : P3 →ᵃ[k] P1)
:
(AffineMap.pi fp).comp g = AffineMap.pi fun (i : ι) => (fp i).comp g
theorem
AffineMap.pi_eq_zero
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
{ι : Type u_9}
{φv : ι → Type u_10}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
(fv : (i : ι) → P1 →ᵃ[k] φv i)
:
AffineMap.pi fv = 0 ↔ ∀ (i : ι), fv i = 0
theorem
AffineMap.pi_zero
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
{ι : Type u_9}
{φv : ι → Type u_10}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
:
(AffineMap.pi fun (x : ι) => 0) = 0
theorem
AffineMap.proj_pi
{k : Type u_2}
{V1 : Type u_3}
{P1 : Type u_4}
[Ring k]
[AddCommGroup V1]
[AddTorsor V1 P1]
[Module k V1]
{ι : Type u_9}
{φv : ι → Type u_10}
{φp : ι → Type u_11}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[(i : ι) → AddTorsor (φv i) (φp i)]
(fp : (i : ι) → P1 →ᵃ[k] φp i)
(i : ι)
:
(AffineMap.proj i).comp (AffineMap.pi fp) = fp i
theorem
AffineMap.pi_ext_zero
{k : Type u_2}
{V2 : Type u_5}
{P2 : Type u_6}
[Ring k]
[AddCommGroup V2]
[AddTorsor V2 P2]
[Module k V2]
{ι : Type u_9}
{φv : ι → Type u_10}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[Finite ι]
[DecidableEq ι]
{f : ((i : ι) → φv i) →ᵃ[k] P2}
{g : ((i : ι) → φv i) →ᵃ[k] P2}
(h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x))
(h₂ : f 0 = g 0)
:
f = g
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 ι.
theorem
AffineMap.pi_ext_nonempty
{k : Type u_2}
{V2 : Type u_5}
{P2 : Type u_6}
[Ring k]
[AddCommGroup V2]
[AddTorsor V2 P2]
[Module k V2]
{ι : Type u_9}
{φv : ι → Type u_10}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[Finite ι]
[DecidableEq ι]
{f : ((i : ι) → φv i) →ᵃ[k] P2}
{g : ((i : ι) → φv i) →ᵃ[k] P2}
[Nonempty ι]
(h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x))
:
f = g
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.
theorem
AffineMap.pi_ext_nonempty'
{k : Type u_2}
{V2 : Type u_5}
{P2 : Type u_6}
[Ring k]
[AddCommGroup V2]
[AddTorsor V2 P2]
[Module k V2]
{ι : Type u_9}
{φv : ι → Type u_10}
[(i : ι) → AddCommGroup (φv i)]
[(i : ι) → Module k (φv i)]
[Finite ι]
[DecidableEq ι]
{f : ((i : ι) → φv i) →ᵃ[k] P2}
{g : ((i : ι) → φv i) →ᵃ[k] P2}
[Nonempty ι]
(h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap)
:
f = g
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'
def
AffineMap.homothety
{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)
:
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
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.homothety c r₁).comp (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₂
def
AffineMap.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)
:
homothety as a multiplicative monoid homomorphism.
Equations
- AffineMap.homothetyHom c = { toFun := AffineMap.homothety c, map_one' := ⋯, map_mul' := ⋯ }
Instances For
@[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)
:
def
AffineMap.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)
:
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
@[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.