# mathlibdocumentation

linear_algebra.affine_space.affine_map

# Affine maps #

This file defines affine maps.

## Main definitions #

• affine_map 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, line_map and homothety.

## Notations #

• P1 →ᵃ[k] P2 is a notation for affine_map k P1 P2;
• affine_space V P: a localized notation for add_torsor V P defined in linear_algebra.affine_space.basic.

## 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] [ V1] [ P1] [add_comm_group V2] [ 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.

Instances for affine_map
@[protected, 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
has_coe_to_fun (P1 →ᵃ[k] P2) (λ (_x : P1 →ᵃ[k] P2), P1 → 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₁] [ V₁] [add_comm_group V₂] [ 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₁] [ V₁] [add_comm_group V₂] [ 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₁] [ V₁] [add_comm_group V₂] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2) (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p) :

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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] {f g : P1 →ᵃ[k] P2} :
f = g ∀ (p : P1), f p = g p
theorem affine_map.coe_fn_injective {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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
@[protected]
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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) :
f x = f y
@[protected]
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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p : P2) :
P1 p) = p
@[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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p : P2) :
P1 p).linear = 0
theorem affine_map.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] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
f.linear = 0 ∃ (q : P2), f = P1 q
@[protected, 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) :
f' p h).linear = f'
@[protected, instance]
def affine_map.mul_action {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] {R : Type u_10} [monoid R] [ V2] [ V2] :
(P1 →ᵃ[k] V2)

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

Equations
@[simp, norm_cast]
theorem affine_map.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] {R : Type u_10} [monoid R] [ V2] [ V2] (c : R) (f : P1 →ᵃ[k] V2) :
(c f) = c f
@[simp]
theorem affine_map.smul_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] {R : Type u_10} [monoid R] [ V2] [ V2] (t : R) (f : P1 →ᵃ[k] V2) :
(t f).linear = t f.linear
@[protected, instance]
def affine_map.is_central_scalar {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] {R : Type u_10} [monoid R] [ V2] [ V2] [ V2] [ V2] :
(P1 →ᵃ[k] V2)
@[protected, instance]
def affine_map.has_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
Equations
@[protected, instance]
def affine_map.has_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
Equations
@[protected, instance]
def affine_map.has_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
has_sub (P1 →ᵃ[k] V2)
Equations
@[protected, instance]
def affine_map.has_neg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] :
has_neg (P1 →ᵃ[k] V2)
Equations
@[simp, norm_cast]
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] [ V1] [ P1] [add_comm_group V2] [ V2] :
0 = 0
@[simp, norm_cast]
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] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f + g) = f + g
@[simp, norm_cast]
theorem affine_map.coe_neg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f : P1 →ᵃ[k] V2) :
@[simp, norm_cast]
theorem affine_map.coe_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f - g) = f - g
@[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] [ V1] [ P1] [add_comm_group V2] [ V2] :
0.linear = 0
@[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] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f + g).linear = f.linear + g.linear
@[simp]
theorem affine_map.sub_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f g : P1 →ᵃ[k] V2) :
(f - g).linear = f.linear - g.linear
@[simp]
theorem affine_map.neg_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [ring k] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] (f : P1 →ᵃ[k] V2) :
@[protected, 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] [ V1] [ P1] [add_comm_group V2] [ V2] :

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

Equations
@[protected, 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
add_torsor (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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] :
def affine_map.id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [ring k] [add_comm_group V1] [ 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] [ V1] [ P1] :
P1) = id

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] [ 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] [ V1] [ P1] (p : P1) :
P1) p = p

The identity affine map acts as the identity.

@[protected, instance]
def affine_map.inhabited {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
f.comp 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] [add_comm_group V3] [ V3] [ P3] [add_comm_group V4] [ V4] [ P4] (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) :
(f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)
@[protected, instance]
def affine_map.monoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ 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] [ 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] [ V1] [ P1] :
def affine_map.linear_hom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] :
(P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1

affine_map.linear on endomorphisms is a monoid_hom.

Equations
@[simp]
theorem affine_map.linear_hom_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (self : P1 →ᵃ[k] P1) :
= self.linear
@[simp]
theorem affine_map.injective_iff_linear_injective {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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
@[simp]
theorem affine_map.surjective_iff_linear_surjective {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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) :
theorem affine_map.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] [add_comm_group V1] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] {s t : set P1} (f : P1 →ᵃ[k] P2) :
f '' s -ᵥ f '' t = (f.linear) '' (s -ᵥ t)

### 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] [ 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] [ V1] [ P1] (p₀ p₁ : P1) :
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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
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] [ V1] (p₀ p₁ : V1) (c : k) :
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] [ V1] (p₀ p₁ : V1) (c : k) :
p₁) c = (1 - c) p₀ + c p₁
theorem affine_map.line_map_apply_ring' {k : Type u_1} [ring k] (a b c : k) :
b) c = c * (b - a) + a
theorem affine_map.line_map_apply_ring {k : Type u_1} [ring k] (a b c : k) :
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] [ V1] [ P1] (p : P1) (v : V1) (c : k) :
(v +ᵥ p)) c = c v +ᵥ p
@[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] [ V1] [ P1] (p₀ p₁ : P1) :
p₁).linear = linear_map.id.smul_right (p₁ -ᵥ p₀)
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] [ V1] [ P1] (p : P1) (c : k) :
p) c = p
@[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] [ V1] [ P1] (p : P1) :
= p
@[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] [ V1] [ P1] (p₀ p₁ : P1) :
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] [ V1] [ P1] (p₀ p₁ : P1) :
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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) :
f ( 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) :
f.comp 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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p₀ p₁ : P1 × P2) (c : k) :
( p₁) c).fst = p₁.fst) c
@[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] [ V1] [ P1] [add_comm_group V2] [ V2] [ P2] (p₀ p₁ : P1 × P2) (c : k) :
( p₁) c).snd = p₁.snd) c
theorem affine_map.line_map_symm {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [ V1] [ P1] (p₀ p₁ : P1) :
p₁ = p₀).comp 0)
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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
p₁) (1 - c) = 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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
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] [ V1] [ P1] (p₀ p₁ : P1) (c : k) :
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] [ V1] [ P1] (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) :
v₂) c +ᵥ 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] [ V1] [ P1] (p₁ p₂ p₃ p₄ : P1) (c : k) :
p₂) c -ᵥ 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] [ V1] [add_comm_group V2] [ 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] [ V1] [add_comm_group V2] [ 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} (f : k →ᵃ[k] k) (a b : k) :
f '' b = set.interval (f a) (f b)
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 : ι), (V i)] [Π (i : ι), add_torsor (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 : ι), (V i)] [Π (i : ι), add_torsor (V i) (P i)] (i : ι) (f : Π (i : ι), P i) :
f = f 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 : ι), (V i)] [Π (i : ι), add_torsor (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 : ι), (V i)] [Π (i : ι), add_torsor (V i) (P i)] (f g : Π (i : ι), P i) (c : k) (i : ι) :
g) c i = (affine_map.line_map (f i) (g i)) c
@[protected, instance]
def affine_map.distrib_mul_action {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [ring k] [add_comm_group V1] [ P1] [add_comm_group V2] [ V1] [ V2] [monoid R] [ V2] [ V2] :
(P1 →ᵃ[k] V2)

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

Equations
@[protected, instance]
def affine_map.module {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [ring k] [add_comm_group V1] [ P1] [add_comm_group V2] [ V1] [ V2] [semiring R] [ V2] [ V2] :
(P1 →ᵃ[k] V2)

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

Equations
def affine_map.to_const_prod_linear_map (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [ring k] [add_comm_group V1] [add_comm_group V2] [ V1] [ V2] [semiring R] [ V2] [ 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.

Equations
@[simp]
theorem affine_map.to_const_prod_linear_map_symm_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [ring k] [add_comm_group V1] [add_comm_group V2] [ V1] [ V2] [semiring R] [ V2] [ V2] (p : V2 × (V1 →ₗ[k] V2)) :
@[simp]
theorem affine_map.to_const_prod_linear_map_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [ring k] [add_comm_group V1] [add_comm_group V2] [ V1] [ V2] [semiring R] [ V2] [ V2] (f : V1 →ᵃ[k] V2) :
= (f 0, f.linear)
def affine_map.homothety {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ 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
theorem affine_map.homothety_def {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r : k) :
= r P1 -ᵥ P1 c) +ᵥ P1 c
theorem affine_map.homothety_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r : k) (p : P1) :
r) p = r (p -ᵥ c) +ᵥ c
theorem affine_map.homothety_eq_line_map {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r : k) (p : P1) :
r) p = p) r
@[simp]
theorem affine_map.homothety_one {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
= P1
@[simp]
theorem affine_map.homothety_apply_same {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r : k) :
r) c = c
theorem affine_map.homothety_mul_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r₁ r₂ : k) (p : P1) :
(r₁ * r₂)) p = r₁) ( r₂) p)
theorem affine_map.homothety_mul {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r₁ r₂ : k) :
(r₁ * r₂) = r₁).comp r₂)
@[simp]
theorem affine_map.homothety_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
= P1 c
@[simp]
theorem affine_map.homothety_add {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) (r₁ r₂ : k) :
(r₁ + r₂) = r₁ P1 -ᵥ P1 c) +ᵥ
def affine_map.homothety_hom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
k →* P1 →ᵃ[k] P1

homothety as a multiplicative monoid homomorphism.

Equations
@[simp]
theorem affine_map.coe_homothety_hom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
def affine_map.homothety_affine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
k →ᵃ[k] P1 →ᵃ[k] P1

homothety as an affine map.

Equations
@[simp]
theorem affine_map.coe_homothety_affine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [ P1] [ V1] (c : P1) :
theorem convex.combo_affine_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ring 𝕜] [ E] [ F] {x 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.