Affine maps

This file defines affine maps.

Main definitions

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

Notations

• P1 →ᵃ[k] P2 is a notation for AffineMap k P1 P2;
• AffineSpace V P: a localized notation for AddTorsor V P defined in LinearAlgebra.AffineSpace.Basic.

Implementation notes

outParam is used in the definition of [AddTorsor V P] to make V an implicit argument (deduced from P) in most cases. As for modules, k is an explicit argument rather than implied by P or V.

This file only provides purely algebraic definitions and results. Those depending on analysis or topology are defined elsewhere; see Analysis.Normed.Affine.AddTorsor and Topology.Algebra.Affine.

References

• https://en.wikipedia.org/wiki/Affine_space
• https://en.wikipedia.org/wiki/Principal_homogeneous_space

structure AffineMap (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : Type (max (max (max u_2 u_3) u_4) u_5)

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

• toFun : P1 → P2
• linear : V1 →ₗ[k] V2
• map_vadd' (p : P1) (v : V1) : self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p

def «term_→ᵃ[_]_» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

instance AffineMap.instFunLike (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} (P2 : Type u_5) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : FunLike (P1 →ᵃ[k] P2) P1 P2

Equations

• AffineMap.instFunLike k P1 P2 = { coe := AffineMap.toFun, coe_injective' := ⋯ }

def LinearMap.toAffineMap {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) : V₁ →ᵃ[k] V₂

Reinterpret a linear map as an affine map.

Equations

• f.toAffineMap = { toFun := ⇑f, linear := f, map_vadd' := ⋯ }

@[simp]

theorem LinearMap.coe_toAffineMap {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) : ⇑f.toAffineMap = ⇑f

@[simp]

theorem LinearMap.toAffineMap_linear {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (f : V₁ →ₗ[k] V₂) : f.toAffineMap.linear = f

@[simp]

theorem AffineMap.coe_mk {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2) (add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p) : ⇑{ toFun := f, linear := linear, map_vadd' := add } = f

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

@[simp]

theorem AffineMap.toFun_eq_coe {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : f.toFun = ⇑f

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

@[simp]

theorem AffineMap.map_vadd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1) : f (v +ᵥ p) = f.linear v +ᵥ f p

An affine map on the result of adding a vector to a point produces the same result as the linear map applied to that vector, added to the affine map applied to that point.

@[simp]

theorem AffineMap.linearMap_vsub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor 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.

theorem AffineMap.ext {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor 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 AffineMap.ext_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2} : f = g ↔ ∀ (p : P1), f p = g p

theorem AffineMap.coeFn_injective {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : Function.Injective DFunLike.coe

theorem AffineMap.congr_arg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y

theorem AffineMap.congr_fun {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2} (h : f = g) (x : P1) : f x = g x

theorem AffineMap.ext_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2} (h₁ : f.linear = g.linear) {p : P1} (h₂ : f p = g p) : f = g

Two affine maps are equal if they have equal linear maps and are equal at some point.

theorem AffineMap.ext_linear_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2} : f = g ↔ f.linear = g.linear ∧ ∃ (p : P1), f p = g p

Two affine maps are equal if they have equal linear maps and are equal at some point.

def AffineMap.const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) : P1 →ᵃ[k] P2

The constant function as an AffineMap.

Equations

• AffineMap.const k P1 p = { toFun := Function.const P1 p, linear := 0, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_const (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) : ⇑(const k P1 p) = Function.const P1 p

@[simp]

theorem AffineMap.const_apply (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) (q : P1) : (const k P1 p) q = p

@[simp]

theorem AffineMap.const_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p : P2) : (const k P1 p).linear = 0

theorem AffineMap.linear_eq_zero_iff_exists_const {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : f.linear = 0 ↔ ∃ (q : P2), f = const k P1 q

instance AffineMap.nonempty {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : Nonempty (P1 →ᵃ[k] P2)

def AffineMap.mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor 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

• AffineMap.mk' f f' p h = { toFun := f, linear := f', map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_mk' {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) : ⇑(mk' f f' p h) = f

@[simp]

theorem AffineMap.mk'_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1) (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) : (mk' f f' p h).linear = f'

instance AffineMap.mulAction {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] : MulAction R (P1 →ᵃ[k] V2)

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

Equations

• AffineMap.mulAction = { smul := fun (c : R) (f : P1 →ᵃ[k] V2) => { toFun := c • ⇑f, linear := c • f.linear, map_vadd' := ⋯ }, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem AffineMap.coe_smul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] (c : R) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • ⇑f

@[simp]

theorem AffineMap.smul_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] (t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear

instance AffineMap.isCentralScalar {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] {R : Type u_10} [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] : IsCentralScalar R (P1 →ᵃ[k] V2)

instance AffineMap.instZero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : Zero (P1 →ᵃ[k] V2)

Equations

• AffineMap.instZero = { zero := { toFun := 0, linear := 0, map_vadd' := ⋯ } }

instance AffineMap.instAdd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : Add (P1 →ᵃ[k] V2)

Equations

• AffineMap.instAdd = { add := fun (f g : P1 →ᵃ[k] V2) => { toFun := ⇑f + ⇑g, linear := f.linear + g.linear, map_vadd' := ⋯ } }

instance AffineMap.instSub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : Sub (P1 →ᵃ[k] V2)

Equations

• AffineMap.instSub = { sub := fun (f g : P1 →ᵃ[k] V2) => { toFun := ⇑f - ⇑g, linear := f.linear - g.linear, map_vadd' := ⋯ } }

instance AffineMap.instNeg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : Neg (P1 →ᵃ[k] V2)

Equations

• AffineMap.instNeg = { neg := fun (f : P1 →ᵃ[k] V2) => { toFun := -⇑f, linear := -f.linear, map_vadd' := ⋯ } }

@[simp]

theorem AffineMap.coe_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : ⇑0 = 0

@[simp]

theorem AffineMap.coe_add {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f g : P1 →ᵃ[k] V2) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem AffineMap.coe_neg {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) : ⇑(-f) = -⇑f

@[simp]

theorem AffineMap.coe_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f g : P1 →ᵃ[k] V2) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem AffineMap.zero_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : linear 0 = 0

@[simp]

theorem AffineMap.add_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f g : P1 →ᵃ[k] V2) : (f + g).linear = f.linear + g.linear

@[simp]

theorem AffineMap.sub_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f g : P1 →ᵃ[k] V2) : (f - g).linear = f.linear - g.linear

@[simp]

theorem AffineMap.neg_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] (f : P1 →ᵃ[k] V2) : (-f).linear = -f.linear

instance AffineMap.instAddCommGroup {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] : AddCommGroup (P1 →ᵃ[k] V2)

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

Equations

• AffineMap.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AffineMap.instAddTorsor {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : AddTorsor (P1 →ᵃ[k] V2) (P1 →ᵃ[k] P2)

The space of affine maps from P1 to P2 is an affine space over the space of affine maps from P1 to the vector space V2 corresponding to P2.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AffineMap.vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) : (f +ᵥ g) p = f p +ᵥ g p

@[simp]

theorem AffineMap.vsub_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f g : P1 →ᵃ[k] P2) (p : P1) : (f -ᵥ g) p = f p -ᵥ g p

def AffineMap.fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : P1 × P2 →ᵃ[k] P1

Prod.fst as an AffineMap.

Equations

• AffineMap.fst = { toFun := Prod.fst, linear := LinearMap.fst k V1 V2, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_fst {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : ⇑fst = Prod.fst

@[simp]

theorem AffineMap.fst_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : fst.linear = LinearMap.fst k V1 V2

def AffineMap.snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : P1 × P2 →ᵃ[k] P2

Prod.snd as an AffineMap.

Equations

• AffineMap.snd = { toFun := Prod.snd, linear := LinearMap.snd k V1 V2, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_snd {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : ⇑snd = Prod.snd

@[simp]

theorem AffineMap.snd_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] : snd.linear = LinearMap.snd k V1 V2

def AffineMap.id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : P1 →ᵃ[k] P1

Identity map as an affine map.

Equations

• AffineMap.id k P1 = { toFun := id, linear := LinearMap.id, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_id (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : ⇑(id k P1) = _root_.id

The identity affine map acts as the identity.

@[simp]

theorem AffineMap.id_linear (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : (id k P1).linear = LinearMap.id

theorem AffineMap.id_apply (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) : (id k P1) p = p

The identity affine map acts as the identity.

instance AffineMap.instInhabited {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : Inhabited (P1 →ᵃ[k] P1)

Equations

• AffineMap.instInhabited = { default := AffineMap.id k P1 }

def AffineMap.comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : P1 →ᵃ[k] P3

Composition of affine maps.

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, linear := f.linear ∘ₗ g.linear, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) : ⇑(f.comp g) = ⇑f ∘ ⇑g

Composition of affine maps acts as applying the two functions.

theorem AffineMap.comp_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) : (f.comp g) p = f (g p)

Composition of affine maps acts as applying the two functions.

@[simp]

theorem AffineMap.comp_id {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : f.comp (id k P1) = f

@[simp]

theorem AffineMap.id_comp {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : (id k P2).comp f = f

theorem AffineMap.comp_assoc {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7} {V4 : Type u_8} {P4 : Type u_9} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] [AddCommGroup V3] [Module k V3] [AddTorsor V3 P3] [AddCommGroup V4] [Module k V4] [AddTorsor V4 P4] (f₃₄ : P3 →ᵃ[k] P4) (f₂₃ : P2 →ᵃ[k] P3) (f₁₂ : P1 →ᵃ[k] P2) : (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)

instance AffineMap.instMonoid {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : Monoid (P1 →ᵃ[k] P1)

Equations

• AffineMap.instMonoid = { mul := AffineMap.comp, mul_assoc := ⋯, one := AffineMap.id k P1, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem AffineMap.coe_mul {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (f g : P1 →ᵃ[k] P1) : ⇑(f * g) = ⇑f ∘ ⇑g

@[simp]

theorem AffineMap.coe_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : ⇑1 = _root_.id

def AffineMap.linearHom {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] : (P1 →ᵃ[k] P1) →* V1 →ₗ[k] V1

AffineMap.linear on endomorphisms is a MonoidHom.

Equations

• AffineMap.linearHom = { toFun := AffineMap.linear, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AffineMap.linearHom_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (self : P1 →ᵃ[k] P1) : linearHom self = self.linear

@[simp]

theorem AffineMap.linear_injective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : Function.Injective ⇑f.linear ↔ Function.Injective ⇑f

@[simp]

theorem AffineMap.linear_surjective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑f

@[simp]

theorem AffineMap.linear_bijective_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) : Function.Bijective ⇑f.linear ↔ Function.Bijective ⇑f

theorem AffineMap.image_vsub_image {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] {s t : Set P1} (f : P1 →ᵃ[k] P2) : ⇑f '' s -ᵥ ⇑f '' t = ⇑f.linear '' (s -ᵥ t)

Definition of AffineMap.lineMap and lemmas about it

def AffineMap.lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : k →ᵃ[k] P1

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

Equations

• AffineMap.lineMap p₀ p₁ = (LinearMap.id.smulRight (p₁ -ᵥ p₀)).toAffineMap +ᵥ AffineMap.const k k p₀

theorem AffineMap.coe_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : ⇑(lineMap p₀ p₁) = fun (c : k) => c • (p₁ -ᵥ p₀) +ᵥ p₀

theorem AffineMap.lineMap_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : (lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀

theorem AffineMap.lineMap_apply_module' {k : Type u_1} {V1 : Type u_2} [Ring k] [AddCommGroup V1] [Module k V1] (p₀ p₁ : V1) (c : k) : (lineMap p₀ p₁) c = c • (p₁ - p₀) + p₀

theorem AffineMap.lineMap_apply_module {k : Type u_1} {V1 : Type u_2} [Ring k] [AddCommGroup V1] [Module k V1] (p₀ p₁ : V1) (c : k) : (lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁

theorem AffineMap.lineMap_apply_ring' {k : Type u_1} [Ring k] (a b c : k) : (lineMap a b) c = c * (b - a) + a

theorem AffineMap.lineMap_apply_ring {k : Type u_1} [Ring k] (a b c : k) : (lineMap a b) c = (1 - c) * a + c * b

theorem AffineMap.lineMap_vadd_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) (v : V1) (c : k) : (lineMap p (v +ᵥ p)) c = c • v +ᵥ p

@[simp]

theorem AffineMap.lineMap_linear {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : (lineMap p₀ p₁).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀)

theorem AffineMap.lineMap_same_apply {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) (c : k) : (lineMap p p) c = p

@[simp]

theorem AffineMap.lineMap_same {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p : P1) : lineMap p p = const k k p

@[simp]

theorem AffineMap.lineMap_apply_zero {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : (lineMap p₀ p₁) 0 = p₀

@[simp]

theorem AffineMap.lineMap_apply_one {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : (lineMap p₀ p₁) 1 = p₁

@[simp]

theorem AffineMap.lineMap_eq_lineMap_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} : (lineMap p₀ p₁) c₁ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

@[simp]

theorem AffineMap.lineMap_eq_left_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} : (lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0

@[simp]

theorem AffineMap.lineMap_eq_right_iff {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} : (lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1

theorem AffineMap.lineMap_injective (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} (h : p₀ ≠ p₁) : Function.Injective ⇑(lineMap p₀ p₁)

@[simp]

theorem AffineMap.apply_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) : f ((lineMap p₀ p₁) c) = (lineMap (f p₀) (f p₁)) c

@[simp]

theorem AffineMap.comp_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) : f.comp (lineMap p₀ p₁) = lineMap (f p₀) (f p₁)

@[simp]

theorem AffineMap.fst_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p₀ p₁ : P1 × P2) (c : k) : ((lineMap p₀ p₁) c).1 = (lineMap p₀.1 p₁.1) c

@[simp]

theorem AffineMap.snd_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p₀ p₁ : P1 × P2) (c : k) : ((lineMap p₀ p₁) c).2 = (lineMap p₀.2 p₁.2) c

theorem AffineMap.lineMap_symm {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) : lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap 1 0)

@[simp]

theorem AffineMap.lineMap_apply_one_sub {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : (lineMap p₀ p₁) (1 - c) = (lineMap p₁ p₀) c

@[simp]

theorem AffineMap.lineMap_vsub_left {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : (lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)

@[simp]

theorem AffineMap.left_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)

@[simp]

theorem AffineMap.lineMap_vsub_right {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : (lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)

@[simp]

theorem AffineMap.right_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c : k) : p₁ -ᵥ (lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)

theorem AffineMap.lineMap_vadd_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) : (lineMap v₁ v₂) c +ᵥ (lineMap p₁ p₂) c = (lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c

theorem AffineMap.lineMap_vsub_lineMap {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₁ p₂ p₃ p₄ : P1) (c : k) : (lineMap p₁ p₂) c -ᵥ (lineMap p₃ p₄) c = (lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c

@[simp]

theorem AffineMap.lineMap_lineMap_right {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c d : k) : (lineMap p₀ ((lineMap p₀ p₁) c)) d = (lineMap p₀ p₁) (d * c)

@[simp]

theorem AffineMap.lineMap_lineMap_left {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] (p₀ p₁ : P1) (c d : k) : (lineMap ((lineMap p₀ p₁) c) p₁) d = (lineMap p₀ p₁) (1 - (1 - d) * (1 - c))

theorem AffineMap.decomp {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddCommGroup V2] [Module k V2] (f : V1 →ᵃ[k] V2) : ⇑f = ⇑f.linear + fun (x : V1) => f 0

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

theorem AffineMap.decomp' {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [Ring k] [AddCommGroup V1] [Module k V1] [AddCommGroup V2] [Module k V2] (f : V1 →ᵃ[k] V2) : ⇑f.linear = ⇑f - fun (x : V1) => f 0

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

theorem AffineMap.image_uIcc {k : Type u_10} [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : k →ᵃ[k] k) (a b : k) : ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

def AffineMap.proj {k : Type u_1} [Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) : ((i : ι) → P i) →ᵃ[k] P i

Evaluation at a point as an affine map.

Equations

• AffineMap.proj i = { toFun := fun (f : (i : ι) → P i) => f i, linear := LinearMap.proj i, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.proj_apply {k : Type u_1} [Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) (f : (i : ι) → P i) : (proj i) f = f i

@[simp]

theorem AffineMap.proj_linear {k : Type u_1} [Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (i : ι) : (proj i).linear = LinearMap.proj i

theorem AffineMap.pi_lineMap_apply {k : Type u_1} [Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (f g : (i : ι) → P i) (c : k) (i : ι) : (lineMap f g) c i = (lineMap (f i) (g i)) c

instance AffineMap.distribMulAction {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V1] [Module k V2] [Monoid R] [DistribMulAction R V2] [SMulCommClass k R V2] : DistribMulAction R (P1 →ᵃ[k] V2)

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

Equations

• AffineMap.distribMulAction = { toMulAction := AffineMap.mulAction, smul_zero := ⋯, smul_add := ⋯ }

instance AffineMap.instModule {R : Type u_1} {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] : Module R (P1 →ᵃ[k] V2)

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

Equations

• AffineMap.instModule = { toDistribMulAction := AffineMap.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

def AffineMap.toConstProdLinearMap (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] : (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2)

The space of affine maps between two modules is linearly equivalent to the product of the domain with the space of linear maps, by taking the value of the affine map at (0 : V1) and the linear part.

See note [bundled maps over different rings]

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AffineMap.toConstProdLinearMap_symm_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] (p : V2 × (V1 →ₗ[k] V2)) : (toConstProdLinearMap R).symm p = p.2.toAffineMap + const k V1 p.1

@[simp]

theorem AffineMap.toConstProdLinearMap_apply (R : Type u_1) {k : Type u_2} {V1 : Type u_3} {V2 : Type u_5} [Ring k] [AddCommGroup V1] [AddCommGroup V2] [Module k V1] [Module k V2] [Semiring R] [Module R V2] [SMulCommClass k R V2] (f : V1 →ᵃ[k] V2) : (toConstProdLinearMap R) f = (f 0, f.linear)

def AffineMap.pi {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (f : (i : ι) → P1 →ᵃ[k] φp i) : P1 →ᵃ[k] (i : ι) → φp i

pi construction for affine maps. From a family of affine maps it produces an affine map into a family of affine spaces.

This is the affine version of LinearMap.pi.

Equations

• AffineMap.pi f = { toFun := fun (m : P1) (a : ι) => (f a) m, linear := LinearMap.pi fun (a : ι) => (f a).linear, map_vadd' := ⋯ }

@[simp]

theorem AffineMap.pi_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (c : P1) (i : ι) : (pi fp) c i = (fp i) c

theorem AffineMap.pi_comp {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V3 : Type u_7} {P3 : Type u_8} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [AddCommGroup V3] [AddTorsor V3 P3] [Module k V1] [Module k V3] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (g : P3 →ᵃ[k] P1) : (pi fp).comp g = pi fun (i : ι) => (fp i).comp g

theorem AffineMap.pi_eq_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ι → Type u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] (fv : (i : ι) → P1 →ᵃ[k] φv i) : pi fv = 0 ↔ ∀ (i : ι), fv i = 0

theorem AffineMap.pi_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ι → Type u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] : (pi fun (x : ι) => 0) = 0

theorem AffineMap.proj_pi {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [Ring k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [(i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (i : ι) : (proj i).comp (pi fp) = fp i

theorem AffineMap.pi_ext_zero {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2} (h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) (h₂ : f 0 = g 0) : f = g

Two affine maps from a Pi-type of modules (i : ι) → φv i are equal if they are equal in their operation on Pi.single and at zero. Analogous to LinearMap.pi_ext. See also pi_ext_nonempty, which instead of agreement at zero requires Nonempty ι.

theorem AffineMap.pi_ext_nonempty {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2} [Nonempty ι] (h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)) : f = g

Two affine maps from a Pi-type of modules (i : ι) → φv i are equal if they are equal in their operation on Pi.single and ι is nonempty. Analogous to LinearMap.pi_ext. See also pi_ext_zero, which instead of Nonempty ι requires agreement at 0.

theorem AffineMap.pi_ext_nonempty' {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [Ring k] [AddCommGroup V2] [AddTorsor V2 P2] [Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [(i : ι) → AddCommGroup (φv i)] [(i : ι) → Module k (φv i)] [Finite ι] [DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2} [Nonempty ι] (h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap) : f = g

This is used as the ext lemma instead of AffineMap.pi_ext_nonempty for reasons explained in note [partially-applied ext lemmas]. Analogous to LinearMap.pi_ext'

def AffineMap.homothety {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) : P1 →ᵃ[k] P1

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

Equations

• AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c

theorem AffineMap.homothety_def {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) : homothety c r = r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c

theorem AffineMap.homothety_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) : (homothety c r) p = r • (p -ᵥ c) +ᵥ c

theorem AffineMap.homothety_eq_lineMap {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) (p : P1) : (homothety c r) p = (lineMap c p) r

@[simp]

theorem AffineMap.homothety_one {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : homothety c 1 = id k P1

@[simp]

theorem AffineMap.homothety_apply_same {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r : k) : (homothety c r) c = c

theorem AffineMap.homothety_mul_apply {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ r₂ : k) (p : P1) : (homothety c (r₁ * r₂)) p = (homothety c r₁) ((homothety c r₂) p)

theorem AffineMap.homothety_mul {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ r₂ : k) : homothety c (r₁ * r₂) = (homothety c r₁).comp (homothety c r₂)

@[simp]

theorem AffineMap.homothety_zero {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : homothety c 0 = const k P1 c

@[simp]

theorem AffineMap.homothety_add {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) (r₁ r₂ : k) : homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂

def AffineMap.homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : k →* P1 →ᵃ[k] P1

homothety as a multiplicative monoid homomorphism.

Equations

• AffineMap.homothetyHom c = { toFun := AffineMap.homothety c, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AffineMap.coe_homothetyHom {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : ⇑(homothetyHom c) = homothety c

def AffineMap.homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : k →ᵃ[k] P1 →ᵃ[k] P1

homothety as an affine map.

Equations

• AffineMap.homothetyAffine c = { toFun := AffineMap.homothety c, linear := (LinearMap.lsmul k (P1 →ᵃ[k] V1)).flip (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c), map_vadd' := ⋯ }

@[simp]

theorem AffineMap.coe_homothetyAffine {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [CommRing k] [AddCommGroup V1] [AddTorsor V1 P1] [Module k V1] (c : P1) : ⇑(homothetyAffine c) = homothety c

theorem Convex.combo_affine_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [AddCommGroup E] [AddCommGroup 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.