mathlib3 documentation

linear_algebra.affine_space.affine_map

Affine maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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.fun_like (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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] :
fun_like (P1 →ᵃ[k] P2) P1 (λ (_x : P1), P2)
Equations
@[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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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₁] [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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] (p : P2) :
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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] (f : P1 →ᵃ[k] P2) :
f.linear = 0 (q : P2), f = affine_map.const k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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'
@[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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] {R : Type u_10} [monoid R] [distrib_mul_action R V2] [smul_comm_class k R V2] :
mul_action R (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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] {R : Type u_10} [monoid R] [distrib_mul_action R V2] [smul_comm_class k R 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] {R : Type u_10} [monoid R] [distrib_mul_action R V2] [smul_comm_class k R 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] {R : Type u_10} [monoid R] [distrib_mul_action R V2] [smul_comm_class k R V2] [distrib_mul_action Rᵐᵒᵖ V2] [is_central_scalar R 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] :
has_add (P1 →ᵃ[k] 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor V1 P1] (p : P1) :
(affine_map.id k 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] [module k V1] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] [add_comm_group V3] [module k V3] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] [add_comm_group V3] [module k V3] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] [add_comm_group V3] [module k V3] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] [add_comm_group V3] [module k V3] [add_torsor V3 P3] [add_comm_group V4] [module k V4] [add_torsor 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] [module k V1] [add_torsor 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] [add_torsor 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] [add_torsor 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] [module k V1] [add_torsor 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] [module k V1] [add_torsor V1 P1] (self : P1 →ᵃ[k] P1) :
@[simp]
theorem affine_map.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] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] (f : P1 →ᵃ[k] P2) :
@[simp]
theorem affine_map.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] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor V2 P2] (f : P1 →ᵃ[k] P2) :
@[simp]
theorem affine_map.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] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [module k V1] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor V1 P1] (p₀ p₁ : P1) :
(affine_map.line_map p₀ p₁) 1 = p₁
@[simp]
theorem affine_map.line_map_eq_line_map_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [no_zero_smul_divisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} :
(affine_map.line_map p₀ p₁) c₁ = (affine_map.line_map p₀ p₁) c₂ p₀ = p₁ c₁ = c₂
@[simp]
theorem affine_map.line_map_eq_left_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [no_zero_smul_divisors k V1] {p₀ p₁ : P1} {c : k} :
(affine_map.line_map p₀ p₁) c = p₀ p₀ = p₁ c = 0
@[simp]
theorem affine_map.line_map_eq_right_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [no_zero_smul_divisors k V1] {p₀ p₁ : P1} {c : k} :
(affine_map.line_map p₀ p₁) c = p₁ p₀ = p₁ c = 1
theorem affine_map.line_map_injective (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [ring k] [add_comm_group V1] [module k V1] [add_torsor V1 P1] [no_zero_smul_divisors k V1] {p₀ p₁ : P1} (h : p₀ 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor V1 P1] [add_comm_group V2] [module k V2] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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] [add_torsor 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_uIcc {k : Type u_1} [linear_ordered_field k] (f : k →ᵃ[k] k) (a b : k) :
f '' set.uIcc a b = set.uIcc (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 : ι), module k (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 : ι), module k (V i)] [Π (i : ι), add_torsor (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 : ι), module k (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 : ι), module k (V i)] [Π (i : ι), add_torsor (V i) (P i)] (f g : Π (i : ι), P i) (c : k) (i : ι) :
@[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] [add_torsor V1 P1] [add_comm_group V2] [module k V1] [module k V2] [monoid R] [distrib_mul_action R V2] [smul_comm_class k R 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] [add_torsor V1 P1] [add_comm_group V2] [module k V1] [module k V2] [semiring R] [module R V2] [smul_comm_class k R V2] :
module R (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] [module k V1] [module k V2] [semiring R] [module R V2] [smul_comm_class 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
@[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] [module k V1] [module k V2] [semiring R] [module R V2] [smul_comm_class k R 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] [module k V1] [module k V2] [semiring R] [module R V2] [smul_comm_class k R V2] (f : V1 →ᵃ[k] V2) :
def affine_map.homothety {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [add_torsor 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
theorem affine_map.homothety_def {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [add_torsor V1 P1] [module k V1] (c : P1) (r : k) :
theorem affine_map.homothety_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [add_torsor V1 P1] [module k V1] (c : P1) (r : k) (p : P1) :
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] [add_torsor V1 P1] [module k V1] (c : P1) (r : k) (p : P1) :
@[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] [add_torsor V1 P1] [module k V1] (c : 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] [add_torsor V1 P1] [module k V1] (c : P1) (r : k) :
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] [add_torsor V1 P1] [module k V1] (c : P1) (r₁ r₂ : k) (p : P1) :
theorem affine_map.homothety_mul {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [add_torsor V1 P1] [module k V1] (c : P1) (r₁ r₂ : k) :
@[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] [add_torsor V1 P1] [module k V1] (c : P1) :
@[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] [add_torsor V1 P1] [module k V1] (c : P1) (r₁ r₂ : k) :
def affine_map.homothety_hom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [comm_ring k] [add_comm_group V1] [add_torsor V1 P1] [module k 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] [add_torsor V1 P1] [module k 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] [add_torsor V1 P1] [module k 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] [add_torsor V1 P1] [module k V1] (c : P1) :
theorem convex.combo_affine_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 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.