mathlib documentation

linear_algebra.affine_space.affine_map

Affine maps

This file defines affine maps.

Main definitions

Notations

Implementation notes

out_param is used in the definition of [add_torsor V P] to make V an implicit argument (deduced from P) in most cases; include V is needed in many cases for V, and type classes using it, to be added as implicit arguments to individual lemmas. 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_space.add_torsor and topology.algebra.affine.

References

structure affine_map (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :
Type (max u_2 u_3 u_4 u_5)

An affine_map k P1 P2 (notation: P1 →ᵃ[k] P2) is a map from P1 to P2 that induces a corresponding linear map from V1 to V2.

@[instance]
def affine_map.has_coe_to_fun (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

Equations
def linear_map.to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [module k V₁] [add_comm_group V₂] [module k V₂] (f : V₁ →ₗ[k] V₂) :
V₁ →ᵃ[k] V₂

Reinterpret a linear map as an affine map.

Equations
@[simp]
theorem linear_map.coe_to_affine_map {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [module k V₁] [add_comm_group V₂] [module k V₂] (f : V₁ →ₗ[k] V₂) :

@[simp]
theorem linear_map.to_affine_map_linear {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [ring k] [add_comm_group V₁] [module k V₁] [add_comm_group V₂] [module k V₂] (f : V₁ →ₗ[k] V₂) :

@[simp]
theorem affine_map.coe_mk {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2) (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p) :
{to_fun := f, linear := linear, map_vadd' := add} = f

Constructing an affine map and coercing back to a function produces the same map.

@[simp]
theorem affine_map.to_fun_eq_coe {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) :

to_fun is the same as the result of coercing to a function.

@[simp]
theorem affine_map.map_vadd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space 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 affine_map.linear_map_vsub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) (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.

@[ext]
theorem affine_map.ext {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] {f 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 affine_map.ext_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] {f g : P1 →ᵃ[k] P2} :
f = g ∀ (p : P1), f p = g p

theorem affine_map.injective_coe_fn {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :
function.injective (λ (f : P1 →ᵃ[k] P2) (x : P1), f x)

theorem affine_map.congr_arg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) :
f x = f y

theorem affine_map.congr_fun {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] {f g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) :
f x = g x

def affine_map.const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (p : P2) :
P1 →ᵃ[k] P2

Constant function as an affine_map.

Equations
@[simp]
theorem affine_map.coe_const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (p : P2) :

@[simp]
theorem affine_map.const_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (p : P2) :

@[instance]
def affine_map.nonempty {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

def affine_map.mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 → P2) (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
@[simp]
theorem affine_map.coe_mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
(affine_map.mk' f f' p h) = f

@[simp]
theorem affine_map.mk'_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
(affine_map.mk' f f' p h).linear = f'

@[instance]
def affine_map.add_comm_group {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] :

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

Equations
@[simp]
theorem affine_map.coe_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] :
0 = 0

@[simp]
theorem affine_map.zero_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] :
0.linear = 0

@[simp]
theorem affine_map.coe_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] (f g : P1 →ᵃ[k] V2) :
(f + g) = f + g

@[simp]
theorem affine_map.add_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] (f g : P1 →ᵃ[k] V2) :
(f + g).linear = f.linear + g.linear

@[instance]
def affine_map.add_torsor {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :
affine_space (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 affine_map.vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) :
(f +ᵥ g) p = f p +ᵥ g p

@[simp]
theorem affine_map.vsub_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f g : P1 →ᵃ[k] P2) (p : P1) :
(f -ᵥ g) p = f p -ᵥ g p

def affine_map.fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :
P1 × P2 →ᵃ[k] P1

prod.fst as an affine_map.

Equations
@[simp]
theorem affine_map.coe_fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

@[simp]
theorem affine_map.fst_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

def affine_map.snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :
P1 × P2 →ᵃ[k] P2

prod.snd as an affine_map.

Equations
@[simp]
theorem affine_map.coe_snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

@[simp]
theorem affine_map.snd_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] :

def affine_map.id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :
P1 →ᵃ[k] P1

Identity map as an affine map.

Equations
@[simp]
theorem affine_map.coe_id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :

The identity affine map acts as the identity.

@[simp]
theorem affine_map.id_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :

theorem affine_map.id_apply (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p : P1) :
(affine_map.id k P1) p = p

The identity affine map acts as the identity.

@[instance]
def affine_map.inhabited {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :

Equations
def affine_map.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] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] [add_comm_group V3] [module k V3] [affine_space V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) :
P1 →ᵃ[k] P3

Composition of affine maps.

Equations
@[simp]
theorem affine_map.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] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] [add_comm_group V3] [module k V3] [affine_space 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 affine_map.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] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] [add_comm_group V3] [module k V3] [affine_space 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 affine_map.comp_id {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) :
f.comp (affine_map.id k P1) = f

@[simp]
theorem affine_map.id_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) :
(affine_map.id k P2).comp f = f

theorem affine_map.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] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] [add_comm_group V3] [module k V3] [affine_space V3 P3] [add_comm_group V4] [module k V4] [affine_space 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]
def affine_map.monoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :
monoid (P1 →ᵃ[k] P1)

Equations
@[simp]
theorem affine_map.coe_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (f g : P1 →ᵃ[k] P1) :
f * g = f g

@[simp]
theorem affine_map.coe_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] :

Definition of affine_map.line_map and lemmas about it

def affine_map.line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :
k →ᵃ[k] P1

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

Equations
theorem affine_map.coe_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :
(affine_map.line_map p₀ p₁) = λ (c : k), c (p₁ -ᵥ p₀) +ᵥ p₀

theorem affine_map.line_map_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
(affine_map.line_map p₀ p₁) c = c (p₁ -ᵥ p₀) +ᵥ p₀

theorem affine_map.line_map_apply_module' {k : Type u_1} {V1 : Type u_2} [ring k] [add_comm_group V1] [module k V1] (p₀ p₁ : V1) (c : k) :
(affine_map.line_map p₀ p₁) c = c (p₁ - p₀) + p₀

theorem affine_map.line_map_apply_module {k : Type u_1} {V1 : Type u_2} [ring k] [add_comm_group V1] [module k V1] (p₀ p₁ : V1) (c : k) :
(affine_map.line_map p₀ p₁) c = (1 - c) p₀ + c p₁

theorem affine_map.line_map_apply_ring' {k : Type u_1} [ring k] (a b c : k) :
(affine_map.line_map a b) c = c * (b - a) + a

theorem affine_map.line_map_apply_ring {k : Type u_1} [ring k] (a b c : k) :
(affine_map.line_map a b) c = (1 - c) * a + c * b

theorem affine_map.line_map_vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p : P1) (v : V1) (c : k) :

@[simp]
theorem affine_map.line_map_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :

theorem affine_map.line_map_same_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p : P1) (c : k) :

@[simp]
theorem affine_map.line_map_same {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p : P1) :

@[simp]
theorem affine_map.line_map_apply_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :
(affine_map.line_map p₀ p₁) 0 = p₀

@[simp]
theorem affine_map.line_map_apply_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :
(affine_map.line_map p₀ p₁) 1 = p₁

@[simp]
theorem affine_map.apply_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
f ((affine_map.line_map p₀ p₁) c) = (affine_map.line_map (f p₀) (f p₁)) c

@[simp]
theorem affine_map.comp_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) :
f.comp (affine_map.line_map p₀ p₁) = affine_map.line_map (f p₀) (f p₁)

@[simp]
theorem affine_map.fst_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (p₀ p₁ : P1 × P2) (c : k) :

@[simp]
theorem affine_map.snd_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] [affine_space V2 P2] (p₀ p₁ : P1 × P2) (c : k) :

theorem affine_map.line_map_symm {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) :

theorem affine_map.line_map_apply_one_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
(affine_map.line_map p₀ p₁) (1 - c) = (affine_map.line_map p₁ p₀) c

@[simp]
theorem affine_map.line_map_vsub_left {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
(affine_map.line_map p₀ p₁) c -ᵥ p₀ = c (p₁ -ᵥ p₀)

@[simp]
theorem affine_map.left_vsub_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
p₀ -ᵥ (affine_map.line_map p₀ p₁) c = c (p₀ -ᵥ p₁)

@[simp]
theorem affine_map.line_map_vsub_right {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
(affine_map.line_map p₀ p₁) c -ᵥ p₁ = (1 - c) (p₀ -ᵥ p₁)

@[simp]
theorem affine_map.right_vsub_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₀ p₁ : P1) (c : k) :
p₁ -ᵥ (affine_map.line_map p₀ p₁) c = (1 - c) (p₁ -ᵥ p₀)

theorem affine_map.line_map_vadd_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) :
(affine_map.line_map v₁ v₂) c +ᵥ (affine_map.line_map p₁ p₂) c = (affine_map.line_map (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c

theorem affine_map.line_map_vsub_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (p₁ p₂ p₃ p₄ : P1) (c : k) :
(affine_map.line_map p₁ p₂) c -ᵥ (affine_map.line_map p₃ p₄) c = (affine_map.line_map (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c

theorem affine_map.decomp {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [add_comm_group V2] [module k V2] (f : V1 →ᵃ[k] V2) :
f = (f.linear) + λ (z : V1), f 0

Decomposition of an affine map in the special case when the point space and vector space are the same.

theorem affine_map.decomp' {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [ring k] [add_comm_group V1] [module k V1] [add_comm_group V2] [module k V2] (f : V1 →ᵃ[k] V2) :
(f.linear) = f - λ (z : V1), f 0

Decomposition of an affine map in the special case when the point space and vector space are the same.

theorem affine_map.image_interval {k : Type u_1} [linear_ordered_field k] (f : k →ᵃ[k] k) (a b : k) :

def affine_map.proj {k : Type u_1} [ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [Π (i : ι), add_comm_group (V i)] [Π (i : ι), semimodule k (V i)] [Π (i : ι), affine_space (V i) (P i)] (i : ι) :
(Π (i : ι), P i) →ᵃ[k] P i

Evaluation at a point as an affine map.

Equations
@[simp]
theorem affine_map.proj_apply {k : Type u_1} [ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [Π (i : ι), add_comm_group (V i)] [Π (i : ι), semimodule k (V i)] [Π (i : ι), affine_space (V i) (P i)] (i : ι) (f : Π (i : ι), P i) :

@[simp]
theorem affine_map.proj_linear {k : Type u_1} [ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [Π (i : ι), add_comm_group (V i)] [Π (i : ι), semimodule k (V i)] [Π (i : ι), affine_space (V i) (P i)] (i : ι) :

theorem affine_map.pi_line_map_apply {k : Type u_1} [ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [Π (i : ι), add_comm_group (V i)] [Π (i : ι), semimodule k (V i)] [Π (i : ι), affine_space (V i) (P i)] (f g : Π (i : ι), P i) (c : k) (i : ι) :

@[instance]
def affine_map.module {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] :
module k (P1 →ᵃ[k] V2)

If k is a commutative ring, then the set of affine maps with codomain in a k-module is a k-module.

Equations
@[simp]
theorem affine_map.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2] (c : k) (f : P1 →ᵃ[k] V2) :
(c f) = c f

def affine_map.homothety {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r : k) :
P1 →ᵃ[k] P1

homothety c r is the homothety about c with scale factor r.

Equations
theorem affine_map.homothety_def {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r : k) :

theorem affine_map.homothety_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r : k) (p : P1) :

theorem affine_map.homothety_eq_line_map {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r : k) (p : P1) :

@[simp]
theorem affine_map.homothety_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :

theorem affine_map.homothety_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r₁ r₂ : k) :

@[simp]
theorem affine_map.homothety_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :

@[simp]
theorem affine_map.homothety_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) (r₁ r₂ : k) :

def affine_map.homothety_hom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :
k →* P1 →ᵃ[k] P1

homothety as a multiplicative monoid homomorphism.

Equations
@[simp]
theorem affine_map.coe_homothety_hom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :

def affine_map.homothety_affine {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :
k →ᵃ[k] P1 →ᵃ[k] P1

homothety as an affine map.

Equations
@[simp]
theorem affine_map.coe_homothety_affine {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [comm_ring k] [add_comm_group V1] [module k V1] [affine_space V1 P1] (c : P1) :