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 #
affine_mapis the type of affine maps between two affine spaces with the same ringk. Various basic examples of affine maps are defined, includingconst,id,line_mapandhomothety.
Notations #
P1 →ᵃ[k] P2is a notation foraffine_map k P1 P2;affine_space V P: a localized notation foradd_torsor V Pdefined inlinear_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]
[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)
- to_fun : P1 → P2
- linear : V1 →ₗ[k] V2
- map_vadd' : ∀ (p : P1) (v : V1), self.to_fun (v +ᵥ p) = ⇑(self.linear) v +ᵥ self.to_fun p
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
- affine_map.has_sizeof_inst
- affine_map.fun_like
- affine_map.has_coe_to_fun
- affine_map.nonempty
- affine_map.mul_action
- affine_map.is_central_scalar
- affine_map.has_zero
- affine_map.has_add
- affine_map.has_sub
- affine_map.has_neg
- affine_map.add_comm_group
- affine_map.add_torsor
- affine_map.inhabited
- affine_map.monoid
- affine_map.distrib_mul_action
- affine_map.module
- affine_equiv.affine_map.has_coe
@[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] :
Equations
- affine_map.fun_like k P1 P2 = {coe := affine_map.to_fun _inst_7, coe_injective' := _}
@[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] :
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₂) :
Reinterpret a linear map as an affine map.
@[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₂) :
⇑(f.to_affine_map) = ⇑f
@[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₂) :
f.to_affine_map.linear = f
@[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) :
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) :
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) :
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} :
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) :
@[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) :
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) :
Constant function as an affine_map.
Equations
- affine_map.const k P1 p = {to_fun := function.const P1 p, linear := 0, map_vadd' := _}
@[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) :
⇑(affine_map.const k P1 p) = function.const P1 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]
[module k V1]
[add_torsor V1 P1]
[add_comm_group V2]
[module k V2]
[add_torsor V2 P2]
(p : P2) :
(affine_map.const k 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]
[module k V1]
[add_torsor V1 P1]
[add_comm_group V2]
[module k V2]
[add_torsor V2 P2]
(f : P1 →ᵃ[k] P2) :
@[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) :
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.
@[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.
@[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) :
@[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) :
@[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] :
is_central_scalar R (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]
[module k V1]
[add_torsor V1 P1]
[add_comm_group V2]
[module k V2] :
@[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] :
@[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] :
@[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] :
@[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] :
@[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) :
@[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) :
@[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] :
@[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) :
@[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) :
@[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] :
add_comm_group (P1 →ᵃ[k] V2)
The set of affine maps to a vector space is an additive commutative group.
Equations
- affine_map.add_comm_group = function.injective.add_comm_group coe_fn affine_map.add_comm_group._proof_3 affine_map.coe_zero affine_map.coe_add affine_map.coe_neg affine_map.coe_sub affine_map.add_comm_group._proof_4 affine_map.add_comm_group._proof_5
@[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
- affine_map.add_torsor = {to_add_action := {to_has_vadd := {vadd := λ (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2), {to_fun := λ (p : P1), ⇑f p +ᵥ ⇑g p, linear := f.linear + g.linear, map_vadd' := _}}, zero_vadd := _, add_vadd := _}, to_has_vsub := {vsub := λ (f g : P1 →ᵃ[k] P2), {to_fun := λ (p : P1), ⇑f p -ᵥ ⇑g p, linear := f.linear - g.linear, map_vadd' := _}}, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}
@[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) :
@[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) :
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] :
prod.fst as an affine_map.
Equations
- affine_map.fst = {to_fun := prod.fst P2, linear := linear_map.fst k V1 V2 _inst_6, map_vadd' := _}
@[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] :
affine_map.fst.linear = linear_map.fst k V1 V2
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] :
prod.snd as an affine_map.
Equations
- affine_map.snd = {to_fun := prod.snd P2, linear := linear_map.snd k V1 V2 _inst_6, map_vadd' := _}
@[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] :
affine_map.snd.linear = linear_map.snd k V1 V2
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] :
Identity map as an affine map.
Equations
- affine_map.id k P1 = {to_fun := id P1, linear := linear_map.id _inst_3, map_vadd' := _}
@[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] :
⇑(affine_map.id k 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]
[module k V1]
[add_torsor V1 P1] :
(affine_map.id k P1).linear = linear_map.id
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
- affine_map.inhabited = {default := affine_map.id k P1 _inst_4}
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) :
Composition of affine maps.
@[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) :
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) :
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) :
@[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] :
Equations
- affine_map.monoid = {mul := affine_map.comp _inst_4, mul_assoc := _, one := affine_map.id k P1 _inst_4, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (P1 →ᵃ[k] P1)), npow_zero' := _, npow_succ' := _}
@[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] :
affine_map.linear on endomorphisms is a monoid_hom.
Equations
- affine_map.linear_hom = {to_fun := affine_map.linear _inst_4, map_one' := _, map_mul' := _}
@[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) :
⇑affine_map.linear_hom self = self.linear
@[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) :
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) :
The affine map from k to P1 sending 0 to p₀ and 1 to p₁.
Equations
- affine_map.line_map p₀ p₁ = (linear_map.id.smul_right (p₁ -ᵥ p₀)).to_affine_map +ᵥ affine_map.const k k p₀
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) :
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) :
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) :
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) :
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) :
(affine_map.line_map p₀ 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]
[module k V1]
[add_torsor V1 P1]
(p : P1)
(c : k) :
⇑(affine_map.line_map p 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]
[module k V1]
[add_torsor V1 P1]
(p : P1) :
affine_map.line_map p p = affine_map.const k k 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]
[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} :
@[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} :
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) :
(⇑(affine_map.line_map p₀ p₁) c).fst = ⇑(affine_map.line_map p₀.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]
[module k V1]
[add_torsor V1 P1]
[add_comm_group V2]
[module k V2]
[add_torsor V2 P2]
(p₀ p₁ : P1 × P2)
(c : k) :
(⇑(affine_map.line_map p₀ p₁) c).snd = ⇑(affine_map.line_map p₀.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]
[module k V1]
[add_torsor V1 P1]
(p₀ p₁ : P1) :
affine_map.line_map p₀ p₁ = (affine_map.line_map p₁ p₀).comp (affine_map.line_map 1 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]
[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) :
@[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) :
@[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) :
@[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) :
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) :
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) :
Decomposition of an affine map in the special case when the point space and vector space are the same.
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 : ι) :
Evaluation at a point as an affine map.
Equations
- affine_map.proj i = {to_fun := λ (f : Π (i : ι), P i), f i, linear := linear_map.proj i, map_vadd' := _}
@[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) :
⇑(affine_map.proj 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 : ι), 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 : ι) :
⇑(affine_map.line_map f 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]
[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] :
distrib_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
- affine_map.distrib_mul_action = {to_mul_action := affine_map.mul_action _inst_9, smul_zero := _, smul_add := _}
@[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] :
The space of affine maps taking values in an R-module is an R-module.
Equations
- affine_map.module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
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] :
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.
@[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)) :
⇑((affine_map.to_const_prod_linear_map R).symm) p = p.snd.to_affine_map + affine_map.const k V1 p.fst
@[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) :
⇑(affine_map.to_const_prod_linear_map R) f = (⇑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]
[add_torsor V1 P1]
[module k V1]
(c : P1)
(r : k) :
homothety c r is the homothety (also known as dilation) about c with scale factor r.
Equations
- affine_map.homothety c r = r • (affine_map.id k P1 -ᵥ affine_map.const k P1 c) +ᵥ affine_map.const k P1 c
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) :
affine_map.homothety c r = r • (affine_map.id k P1 -ᵥ affine_map.const k P1 c) +ᵥ affine_map.const k 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]
[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) :
⇑(affine_map.homothety c r) p = ⇑(affine_map.line_map c 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]
[add_torsor V1 P1]
[module k V1]
(c : P1) :
affine_map.homothety c 1 = affine_map.id k 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) :
⇑(affine_map.homothety c 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]
[add_torsor V1 P1]
[module k V1]
(c : P1)
(r₁ r₂ : k)
(p : P1) :
⇑(affine_map.homothety c (r₁ * r₂)) p = ⇑(affine_map.homothety c r₁) (⇑(affine_map.homothety c 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]
[add_torsor V1 P1]
[module k V1]
(c : P1)
(r₁ r₂ : k) :
affine_map.homothety c (r₁ * r₂) = (affine_map.homothety c r₁).comp (affine_map.homothety c 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]
[add_torsor V1 P1]
[module k V1]
(c : P1) :
affine_map.homothety c 0 = affine_map.const k 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]
[add_torsor V1 P1]
[module k V1]
(c : P1)
(r₁ r₂ : k) :
affine_map.homothety c (r₁ + r₂) = r₁ • (affine_map.id k P1 -ᵥ affine_map.const k P1 c) +ᵥ affine_map.homothety c r₂
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) :
homothety as a multiplicative monoid homomorphism.
Equations
- affine_map.homothety_hom c = {to_fun := affine_map.homothety c, map_one' := _, map_mul' := _}
@[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) :
homothety as an affine map.
Equations
- affine_map.homothety_affine c = {to_fun := affine_map.homothety c, linear := ⇑((linear_map.lsmul k (P1 →ᵃ[k] V1)).flip) (affine_map.id k P1 -ᵥ affine_map.const k P1 c), map_vadd' := _}
@[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) :
Applying an affine map to an affine combination of two points yields an affine combination of the images.