mathlib documentation

linear_algebra.affine_space.basis

Affine bases and barycentric coordinates #

Suppose P is an affine space modelled on the module V over the ring k, and p : ι → P is an affine-independent family of points spanning P. Given this data, each point q : P may be written uniquely as an affine combination: q = w₀ p₀ + w₁ p₁ + ⋯ for some (finitely-supported) weights wᵢ. For each i : ι, we thus have an affine map P →ᵃ[k] k, namely q ↦ wᵢ. This family of maps is known as the family of barycentric coordinates. It is defined in this file.

The construction #

Fixing i : ι, and allowing j : ι to range over the values j ≠ i, we obtain a basis bᵢ of V defined by bᵢ j = p j -ᵥ p i. Let fᵢ j : V →ₗ[k] k be the corresponding dual basis and let fᵢ = ∑ j, fᵢ j : V →ₗ[k] k be the corresponding "sum of all coordinates" form. Then the ith barycentric coordinate of q : P is 1 - fᵢ (q -ᵥ p i).

Main definitions #

affine_basis: a structure representing an affine basis of an affine space.
affine_basis.coord: the map P →ᵃ[k] k corresponding to i : ι.
affine_basis.coord_apply_eq: the behaviour of affine_basis.coord i on p i.
affine_basis.coord_apply_neq: the behaviour of affine_basis.coord i on p j when j ≠ i.
affine_basis.coord_apply: the behaviour of affine_basis.coord i on p j for general j.
affine_basis.coord_apply_combination: the characterisation of affine_basis.coord i in terms of affine combinations, i.e., affine_basis.coord i (w₀ p₀ + w₁ p₁ + ⋯) = wᵢ.

TODO #

Construct the affine equivalence between P and { f : ι →₀ k | f.sum = 1 }.

structure affine_basis (ι : Type u₁) (k : Type u₂) {V : Type u₃} (P : Type u₄) [add_comm_group V] [add_torsor V P] [ring k] [module k V] :

Type (max u₁ u₄)

points : ι → P
ind : affine_independent k self.points
tot : affine_span k (set.range self.points) = ⊤

An affine basis is a family of affine-independent points whose span is the top subspace.

Instances for affine_basis

affine_basis.has_sizeof_inst
affine_basis.inhabited

@[protected, instance]

def affine_basis.inhabited {k : Type u₂} [ring k] :

inhabited (affine_basis punit k punit)

The unique point in a single-point space is the simplest example of an affine basis.

Equations

affine_basis.inhabited = {default := {points := id punit, ind := _, tot := _}}

noncomputable def affine_basis.basis_of {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :

basis {j // j ≠ i} k V

Given an affine basis for an affine space P, if we single out one member of the family, we obtain a linear basis for the model space V.

The linear basis correpsonding to the singled-out member i : ι is indexed by {j : ι // j ≠ i} and its jth element is points j -ᵥ points i. (See basis_of_apply.)

Equations

b.basis_of i = basis.mk _ _

@[simp]

theorem affine_basis.basis_of_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) (j : {j // j ≠ i}) :

⇑(b.basis_of i) j = b.points ↑j -ᵥ b.points i

noncomputable def affine_basis.coord {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :

The ith barycentric coordinate of a point.

Equations

b.coord i = {to_fun := λ (q : P), 1 - ⇑((b.basis_of i).sum_coords) (q -ᵥ b.points i), linear := -(b.basis_of i).sum_coords, map_vadd' := _}

@[simp]

theorem affine_basis.linear_eq_sum_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :

(b.coord i).linear = -(b.basis_of i).sum_coords

@[simp]

theorem affine_basis.coord_apply_eq {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :

⇑(b.coord i) (b.points i) = 1

@[simp]

theorem affine_basis.coord_apply_neq {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i j : ι) (h : j ≠ i) :

⇑(b.coord i) (b.points j) = 0

theorem affine_basis.coord_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [decidable_eq ι] (i j : ι) :

⇑(b.coord i) (b.points j) = ite (i = j) 1 0

@[simp]

theorem affine_basis.coord_apply_combination_of_mem {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {s : finset ι} {i : ι} (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :

⇑(b.coord i) (⇑(s.affine_combination b.points) w) = w i

@[simp]

theorem affine_basis.coord_apply_combination_of_not_mem {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {s : finset ι} {i : ι} (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :

⇑(b.coord i) (⇑(s.affine_combination b.points) w) = 0

@[simp]

theorem affine_basis.sum_coord_apply_eq_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (q : P) :

finset.univ.sum (λ (i : ι), ⇑(b.coord i) q) = 1

@[simp]

theorem affine_basis.affine_combination_coord_eq_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (q : P) :

⇑(finset.univ.affine_combination b.points) (λ (i : ι), ⇑(b.coord i) q) = q

@[simp]

theorem affine_basis.linear_combination_coord_eq_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} [add_comm_group V] [ring k] [module k V] [fintype ι] (b : affine_basis ι k V) (v : V) :

finset.univ.sum (λ (i : ι), ⇑(b.coord i) v • b.points i) = v

A variant of affine_basis.affine_combination_coord_eq_self for the special case when the affine space is a module so we can talk about linear combinations.

theorem affine_basis.ext_elem {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] {q₁ q₂ : P} (h : ∀ (i : ι), ⇑(b.coord i) q₁ = ⇑(b.coord i) q₂) :

q₁ = q₂

@[simp]

theorem affine_basis.coe_coord_of_subsingleton_eq_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [subsingleton ι] (i : ι) :

⇑(b.coord i) = 1

theorem affine_basis.surjective_coord {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [nontrivial ι] (i : ι) :

function.surjective ⇑(b.coord i)

noncomputable def affine_basis.coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) :

P →ᵃ[k] ι → k

Barycentric coordinates as an affine map.

Equations

b.coords = {to_fun := λ (q : P) (i : ι), ⇑(b.coord i) q, linear := {to_fun := λ (v : V) (i : ι), -⇑((b.basis_of i).sum_coords) v, map_add' := _, map_smul' := _}, map_vadd' := _}

@[simp]

theorem affine_basis.coords_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (q : P) (i : ι) :

⇑(b.coords) q i = ⇑(b.coord i) q

noncomputable def affine_basis.to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} (q : ι' → P) :

matrix ι' ι k

Given an affine basis p, and a family of points q : ι' → P, this is the matrix whose rows are the barycentric coordinates of q with respect to p.

It is an affine equivalent of basis.to_matrix.

Equations

b.to_matrix q = λ (i : ι') (j : ι), ⇑(b.coord j) (q i)

@[simp]

theorem affine_basis.to_matrix_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} (q : ι' → P) (i : ι') (j : ι) :

b.to_matrix q i j = ⇑(b.coord j) (q i)

@[simp]

theorem affine_basis.to_matrix_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [decidable_eq ι] :

b.to_matrix b.points = 1

theorem affine_basis.to_matrix_row_sum_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] {ι' : Type u_1} (q : ι' → P) (i : ι') :

finset.univ.sum (λ (j : ι), b.to_matrix q i j) = 1

theorem affine_basis.affine_independent_of_to_matrix_right_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} [fintype ι'] [fintype ι] [decidable_eq ι'] (p : ι' → P) {A : matrix ι ι' k} (hA : (b.to_matrix p).mul A = 1) :

affine_independent k p

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a right inverse, then p is affine independent.

theorem affine_basis.affine_span_eq_top_of_to_matrix_left_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} [fintype ι'] [fintype ι] [decidable_eq ι] [nontrivial k] (p : ι' → P) {A : matrix ι ι' k} (hA : A.mul (b.to_matrix p) = 1) :

affine_span k (set.range p) = ⊤

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a left inverse, then p spans the entire space.

@[simp]

theorem affine_basis.to_matrix_vec_mul_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) (x : P) :

matrix.vec_mul (⇑(b₂.coords) x) (b.to_matrix b₂.points) = ⇑(b.coords) x

A change of basis formula for barycentric coordinates.

See also affine_basis.to_matrix_inv_mul_affine_basis_to_matrix.

theorem affine_basis.to_matrix_mul_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) [decidable_eq ι] :

(b.to_matrix b₂.points).mul (b₂.to_matrix b.points) = 1

theorem affine_basis.is_unit_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) [decidable_eq ι] :

is_unit (b.to_matrix b₂.points)

theorem affine_basis.is_unit_to_matrix_iff {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] [decidable_eq ι] [nontrivial k] (p : ι → P) :

is_unit (b.to_matrix p) ↔ affine_independent k p ∧ affine_span k (set.range p) = ⊤

@[simp]

theorem affine_basis.to_matrix_inv_vec_mul_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [comm_ring k] [module k V] [decidable_eq ι] [fintype ι] (b b₂ : affine_basis ι k P) (x : P) :

matrix.vec_mul (⇑(b.coords) x) (b.to_matrix b₂.points)⁻¹ = ⇑(b₂.coords) x

A change of basis formula for barycentric coordinates.

See also affine_basis.to_matrix_vec_mul_coords.

theorem affine_basis.det_smul_coords_eq_cramer_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [comm_ring k] [module k V] [decidable_eq ι] [fintype ι] (b b₂ : affine_basis ι k P) (x : P) :

(b.to_matrix b₂.points).det • ⇑(b₂.coords) x = ⇑((b.to_matrix b₂.points).transpose.cramer) (⇑(b.coords) x)

If we fix a background affine basis b, then for any other basis b₂, we can characterise the barycentric coordinates provided by b₂ in terms of determinants relative to b.

theorem affine_basis.exists_affine_basis (k : Type u₂) (V : Type u₃) (P : Type u₄) [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] :

∃ (s : set P), nonempty (affine_basis ↥s k P)

theorem affine_basis.exists_affine_basis_of_finite_dimensional {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] {ι : Type u_1} [fintype ι] [finite_dimensional k V] (h : fintype.card ι = finite_dimensional.finrank k V + 1) :

nonempty (affine_basis ι k P)