# Affine maps #

This file defines affine maps.

## Main definitions #

• AffineMap is the type of affine maps between two affine spaces with the same ring k. Various basic examples of affine maps are defined, including const, id, lineMap and homothety.

## Notations #

• P1 →ᵃ[k] P2 is a notation for AffineMap k P1 P2;
• AffineSpace V P: a localized notation for AddTorsor V P defined in LinearAlgebra.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 #

structure AffineMap (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [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 : P1P2
• linear : V1 →ₗ[k] V2
• map_vadd' : ∀ (p : P1) (v : V1), self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (self : P1 →ᵃ[k] P2) (p : P1) (v : V1) :
self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun 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.

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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
FunLike (P1 →ᵃ[k] P2) P1 P2
Equations
• = { coe := AffineMap.toFun, coe_injective' := }
instance AffineMap.hasCoeToFun (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
CoeFun (P1 →ᵃ[k] P2) fun (x : P1 →ᵃ[k] P2) => P1P2
Equations
• = DFunLike.hasCoeToFun
def LinearMap.toAffineMap {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [] [Module k V₁] [] [Module k V₂] (f : V₁ →ₗ[k] V₂) :
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] [] [Module k 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] [] [Module k 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1) :
f (v +ᵥ p) = f.linear v +ᵥ f p

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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p1 : P1) (p2 : P1) :
f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

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] [] [Module k V1] [AddTorsor V1 P1] [] [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.ext_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} :
f = g ∀ (p : P1), f p = g p
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
Function.Injective DFunLike.coe
theorem AffineMap.congr_arg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) {x : P1} {y : P1} (h : x = y) :
f x = f y
theorem AffineMap.congr_fun {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) :
f x = g x
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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] {f : P1 →ᵃ[k] P2} {g : P1 →ᵃ[k] P2} :
f = g f.linear = g.linear ∃ (p : P1), f p = g p

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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (p : P2) :
P1 →ᵃ[k] P2

The constant function as an AffineMap.

Equations
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (p : P2) :
(AffineMap.const k 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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
f.linear = 0 ∃ (q : P2), f = AffineMap.const k P1 q
instance AffineMap.nonempty {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
Equations
• =
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
P1 →ᵃ[k] P2

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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1P2) (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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] {R : Type u_10} [] [] [SMulCommClass k R V2] :
MulAction R (P1 →ᵃ[k] V2)

The space of affine maps to a module inherits an R-action from the action on its codomain.

Equations
• AffineMap.mulAction =
@[simp]
theorem AffineMap.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] {R : Type u_10} [] [] [SMulCommClass k R V2] (c : R) (f : P1 →ᵃ[k] V2) :
(c f) = c f
@[simp]
theorem AffineMap.smul_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] {R : Type u_10} [] [] [SMulCommClass k R V2] (t : R) (f : P1 →ᵃ[k] V2) :
(t f).linear = t f.linear
instance AffineMap.isCentralScalar {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] {R : Type u_10} [] [] [SMulCommClass k R V2] [] [] :
Equations
• =
instance AffineMap.instZero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
Zero (P1 →ᵃ[k] V2)
Equations
• AffineMap.instZero = { zero := { toFun := 0, linear := 0, map_vadd' := } }
instance AffineMap.instAdd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
Equations
• AffineMap.instAdd = { add := fun (f g : P1 →ᵃ[k] V2) => { toFun := f + g, linear := f.linear + g.linear, map_vadd' := } }
instance AffineMap.instSub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
Sub (P1 →ᵃ[k] V2)
Equations
• AffineMap.instSub = { sub := fun (f g : P1 →ᵃ[k] V2) => { toFun := f - g, linear := f.linear - g.linear, map_vadd' := } }
instance AffineMap.instNeg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
Neg (P1 →ᵃ[k] V2)
Equations
• AffineMap.instNeg = { neg := fun (f : P1 →ᵃ[k] V2) => { toFun := -f, linear := -f.linear, map_vadd' := } }
@[simp]
theorem AffineMap.coe_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
0 = 0
@[simp]
theorem AffineMap.coe_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
(f + g) = f + g
@[simp]
theorem AffineMap.coe_neg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) :
(-f) = -f
@[simp]
theorem AffineMap.coe_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
(f - g) = f - g
@[simp]
theorem AffineMap.zero_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :
@[simp]
theorem AffineMap.add_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
(f + g).linear = f.linear + g.linear
@[simp]
theorem AffineMap.sub_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] V2) :
(f - g).linear = f.linear - g.linear
@[simp]
theorem AffineMap.neg_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] (f : P1 →ᵃ[k] V2) :
(-f).linear = -f.linear
instance AffineMap.instAddCommGroup {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] :

The set of affine maps to a vector space is an additive commutative group.

Equations
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
AddTorsor (P1 →ᵃ[k] V2) (P1 →ᵃ[k] 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
@[simp]
theorem AffineMap.vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) :
(f +ᵥ g) p = f p +ᵥ g p
@[simp]
theorem AffineMap.vsub_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P2) (p : P1) :
(f -ᵥ g) p = f p -ᵥ g p
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
P1 × P2 →ᵃ[k] P1

Prod.fst as an AffineMap.

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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] :
P1 × P2 →ᵃ[k] P2

Prod.snd as an AffineMap.

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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] :
P1 →ᵃ[k] 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] [] [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] [] [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] [] [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] [] [Module k V1] [AddTorsor V1 P1] :
Equations
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] [] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
P1 →ᵃ[k] P3

Composition of affine maps.

Equations
• f.comp g = { toFun := f g, linear := f.linear ∘ₗ g.linear, map_vadd' := }
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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] [] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
(f.comp 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] [] [Module k V3] [AddTorsor V3 P3] [] [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₁₂)
instance AffineMap.instMonoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] :
Monoid (P1 →ᵃ[k] P1)
Equations
• AffineMap.instMonoid = Monoid.mk npowRec
@[simp]
theorem AffineMap.coe_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (f : P1 →ᵃ[k] P1) (g : P1 →ᵃ[k] P1) :
(f * g) = f g
@[simp]
theorem AffineMap.coe_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] :
1 = id
@[simp]
theorem AffineMap.linearHom_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (self : P1 →ᵃ[k] P1) :
AffineMap.linearHom self = self.linear
def AffineMap.linearHom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] :
(P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1

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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
Function.Injective f.linear
@[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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
@[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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) :
Function.Bijective f.linear
theorem AffineMap.image_vsub_image {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] {s : Set P1} {t : Set P1} (f : P1 →ᵃ[k] P2) :
f '' s -ᵥ f '' t = f.linear '' (s -ᵥ t)

### 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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
k →ᵃ[k] P1

The affine map from k to P1 sending 0 to p₀ and 1 to p₁.

Equations
Instances For
theorem AffineMap.coe_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
() = 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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
() c = c (p₁ -ᵥ p₀) +ᵥ p₀
theorem AffineMap.lineMap_apply_module' {k : Type u_1} {V1 : Type u_2} [Ring k] [] [Module k V1] (p₀ : V1) (p₁ : V1) (c : k) :
() c = c (p₁ - p₀) + p₀
theorem AffineMap.lineMap_apply_module {k : Type u_1} {V1 : Type u_2} [Ring k] [] [Module k V1] (p₀ : V1) (p₁ : V1) (c : k) :
() c = (1 - c) p₀ + c p₁
theorem AffineMap.lineMap_apply_ring' {k : Type u_1} [Ring k] (a : k) (b : k) (c : k) :
() c = c * (b - a) + a
theorem AffineMap.lineMap_apply_ring {k : Type u_1} [Ring k] (a : k) (b : k) (c : k) :
() c = (1 - c) * a + c * b
theorem AffineMap.lineMap_vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
().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] [] [Module k V1] [AddTorsor V1 P1] (p : P1) (c : k) :
() c = p
@[simp]
theorem AffineMap.lineMap_same {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p : P1) :
=
@[simp]
theorem AffineMap.lineMap_apply_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
() 0 = p₀
@[simp]
theorem AffineMap.lineMap_apply_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
() 1 = p₁
@[simp]
theorem AffineMap.lineMap_eq_lineMap_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] {p₀ : P1} {p₁ : P1} {c₁ : k} {c₂ : k} :
() c₁ = () 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] [] [Module k V1] [AddTorsor V1 P1] [] {p₀ : P1} {p₁ : P1} {c : k} :
() c = p₀ p₀ = p₁ c = 0
@[simp]
theorem AffineMap.lineMap_eq_right_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] {p₀ : P1} {p₁ : P1} {c : k} :
() c = p₁ p₀ = p₁ c = 1
theorem AffineMap.lineMap_injective (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] [] {p₀ : P1} {p₁ : P1} (h : 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ : P1) (p₁ : P1) (c : k) :
f (() 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ : P1) (p₁ : P1) :
f.comp () = 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (p₀ : P1 × P2) (p₁ : P1 × P2) (c : k) :
(() 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] [] [Module k V1] [AddTorsor V1 P1] [] [Module k V2] [AddTorsor V2 P2] (p₀ : P1 × P2) (p₁ : P1 × P2) (c : k) :
(() 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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) :
= ().comp ()
theorem AffineMap.lineMap_apply_one_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
() (1 - c) = () c
@[simp]
theorem AffineMap.lineMap_vsub_left {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
() 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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
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] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
() c -ᵥ p₁ = (1 - c) (p₀ -ᵥ p₁)
@[simp]
theorem AffineMap.right_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (p₀ : P1) (p₁ : P1) (c : k) :
p₁ -ᵥ () c = (1 - c) (p₁ -ᵥ p₀)
theorem AffineMap.lineMap_vadd_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [] [Module k V1] [AddTorsor V1 P1] (v₁ : V1) (v₂ : V1) (p₁ : P1) (p₂ : P1) (c : k) :
() c +ᵥ () 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] [] [Module k V1] [AddTorsor V1 P1] (p₁ : P1) (p₂ : P1) (p₃ : P1) (p₄ : P1) (c : k) :
() c -ᵥ () 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] [] [Module k V1] [] [Module k V2] (f : V1 →ᵃ[k] V2) :
f = f.linear + fun (x : V1) => f 0

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] [] [Module k V1] [] [Module k V2] (f : V1 →ᵃ[k] V2) :
f.linear = f - fun (x : V1) => f 0

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} (f : k →ᵃ[k] k) (a : k) (b : k) :
f '' Set.uIcc a b = Set.uIcc (f a) (f b)
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 : ι) :
((i : ι) → P i) →ᵃ[k] P i

Evaluation at a point as an affine map.

Equations
• = { toFun := fun (f : (i : ι) → P i) => f i, linear := , 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) :
() 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 : ι) :
().linear =
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 : ι) :
() 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] [] [AddTorsor V1 P1] [] [Module k V1] [Module k 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.distribMulAction =
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] [] [AddTorsor V1 P1] [] [Module k V1] [Module k V2] [] [Module R V2] [SMulCommClass k R V2] :
Module R (P1 →ᵃ[k] V2)

The space of affine maps taking values in an R-module is an R-module.

Equations
• AffineMap.instModule = let __src := AffineMap.distribMulAction;
@[simp]
theorem AffineMap.toConstProdLinearMap_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [] [] [Module k V1] [Module k V2] [] [Module R V2] [SMulCommClass k R V2] (f : V1 →ᵃ[k] V2) :
= (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] [] [] [Module k V1] [Module k V2] [] [Module R V2] [SMulCommClass k R V2] (p : V2 × (V1 →ₗ[k] V2)) :
.symm p = p.2.toAffineMap + AffineMap.const k V1 p.1
def AffineMap.toConstProdLinearMap (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [] [] [Module k V1] [Module k V2] [] [Module R V2] [SMulCommClass k R V2] :
(V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] 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
def AffineMap.pi {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [] [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) :
P1 →ᵃ[k] (i : ι) → φ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
• = { 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] [] [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 : ι) :
() 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] [] [AddTorsor V1 P1] [] [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) :
().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] [] [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) :
= 0 ∀ (i : ι), fv i = 0
theorem AffineMap.pi_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [] [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] [] [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 : ι) :
().comp () = fp i
theorem AffineMap.pi_ext_zero {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [] [] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} (h : ∀ (i : ι) (x : φv i), f () = g ()) (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 agrement at zero requires Nonempty ι.

theorem AffineMap.pi_ext_nonempty {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [] [] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} [] (h : ∀ (i : ι) (x : φv i), f () = g ()) :
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] [] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ιType u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [] [] {f : ((i : ι) → φv i) →ᵃ[k] P2} {g : ((i : ι) → φv i) →ᵃ[k] P2} [] (h : ∀ (i : ι), f.comp ().toAffineMap = g.comp ().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} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
P1 →ᵃ[k] P1

homothety c r is the homothety (also known as dilation) about c with scale factor r.

Equations
Instances For
theorem AffineMap.homothety_def {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
theorem AffineMap.homothety_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) :
() p = r (p -ᵥ c) +ᵥ c
theorem AffineMap.homothety_eq_lineMap {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) :
() p = () r
@[simp]
theorem AffineMap.homothety_one {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) :
@[simp]
theorem AffineMap.homothety_apply_same {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) :
() c = c
theorem AffineMap.homothety_mul_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ : k) (r₂ : k) (p : P1) :
(AffineMap.homothety c (r₁ * r₂)) p = () (() p)
theorem AffineMap.homothety_mul {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ : k) (r₂ : k) :
AffineMap.homothety c (r₁ * r₂) = ().comp ()
@[simp]
theorem AffineMap.homothety_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) :
@[simp]
theorem AffineMap.homothety_add {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [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) +ᵥ
def AffineMap.homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) :
k →* P1 →ᵃ[k] P1

homothety as a multiplicative monoid homomorphism.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem AffineMap.coe_homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) :
def AffineMap.homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [AddTorsor V1 P1] [Module k V1] (c : P1) :
k →ᵃ[k] P1 →ᵃ[k] P1

homothety as an affine map.

Equations
Instances For
@[simp]
theorem AffineMap.coe_homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [] [] [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 𝕜] [] [] [Module 𝕜 E] [Module 𝕜 F] {x : E} {y : E} {a : 𝕜} {b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
f (a x + b y) = a f x + b f y

Applying an affine map to an affine combination of two points yields an affine combination of the images.