mathlib3 documentation

linear_algebra.affine_space.basis

Affine bases and barycentric coordinates #

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

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 #

TODO #

source
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₄)

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

Instances for affine_basis
source
@[protected, instance]
def affine_basis.inhabited {k : Type u_3} [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
source
@[protected, instance]
def affine_basis.fun_like {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] :
fun_like (affine_basis ι k P) ι (λ (_x : ι), P)
Equations
source
@[ext]
theorem affine_basis.ext {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] {b₁ b₂ : affine_basis ι k P} (h : ⇑b₁ = ⇑b₂) :
b₁ = b₂
source
theorem affine_basis.ind {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) :
affine_independent k ⇑b
source
theorem affine_basis.tot {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) :
affine_span k (set.range ⇑b) = ⊤
source
@[protected]
theorem affine_basis.nonempty {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) :
nonempty ι
source
def affine_basis.reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (e : ι ≃ ι') :
affine_basis ι' k P

Composition of an affine basis and an equivalence of index types.

Equations
source
@[simp, norm_cast]
theorem affine_basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (e : ι ≃ ι') :
⇑(b.reindex e) = ⇑b ∘ ⇑(e.symm)
source
@[simp]
theorem affine_basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (e : ι ≃ ι') (i' : ι') :
⇑(b.reindex e) i' = ⇑b (⇑(e.symm) i')
source
@[simp]
theorem affine_basis.reindex_refl {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) :
b.reindex (equiv.refl ι) = b
source
noncomputable def affine_basis.basis_of {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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 corresponding to the singled-out member i : ι is indexed by {j : ι // j ≠ i} and its jth element is b j -ᵥ b i. (See basis_of_apply.)

Equations
source
@[simp]
theorem affine_basis.basis_of_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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 ↑j -ᵥ ⇑b i
source
@[simp]
theorem affine_basis.basis_of_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (e : ι ≃ ι') (i : ι') :
(b.reindex e).basis_of i = (b.basis_of (⇑(e.symm) i)).reindex (e.subtype_equiv _)
source
noncomputable def affine_basis.coord {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :
P →ᵃ[k] k

The ith barycentric coordinate of a point.

Equations
source
@[simp]
theorem affine_basis.linear_eq_sum_coords {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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
source
@[simp]
theorem affine_basis.coord_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (e : ι ≃ ι') (i : ι') :
(b.reindex e).coord i = b.coord (⇑(e.symm) i)
source
@[simp]
theorem affine_basis.coord_apply_eq {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) (i : ι) :
⇑(b.coord i) (⇑b i) = 1
source
@[simp]
theorem affine_basis.coord_apply_ne {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {i j : ι} (h : i ≠ j) :
⇑(b.coord i) (⇑b j) = 0
source
theorem affine_basis.coord_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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 j) = ite (i = j) 1 0
source
@[simp]
theorem affine_basis.coord_apply_combination_of_mem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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) (⇑(finset.affine_combination k s ⇑b) w) = w i
source
@[simp]
theorem affine_basis.coord_apply_combination_of_not_mem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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) (⇑(finset.affine_combination k s ⇑b) w) = 0
source
@[simp]
theorem affine_basis.sum_coord_apply_eq_one {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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
source
@[simp]
theorem affine_basis.affine_combination_coord_eq_self {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (q : P) :
⇑(finset.affine_combination k finset.univ ⇑b) (λ (i : ι), ⇑(b.coord i) q) = q
source
@[simp]
theorem affine_basis.linear_combination_coord_eq_self {ι : Type u_1} {k : Type u_3} {V : Type u_4} [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 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.

source
theorem affine_basis.ext_elem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [finite ι] {q₁ q₂ : P} (h : ∀ (i : ι), ⇑(b.coord i) q₁ = ⇑(b.coord i) q₂) :
q₁ = q₂
source
@[simp]
theorem affine_basis.coe_coord_of_subsingleton_eq_one {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [subsingleton ι] (i : ι) :
⇑(b.coord i) = 1
source
theorem affine_basis.surjective_coord {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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)
source
noncomputable def affine_basis.coords {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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
source
@[simp]
theorem affine_basis.coords_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [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
source
@[simp]
theorem affine_basis.coord_apply_centroid {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [char_zero k] (b : affine_basis ι k P) {s : finset ι} {i : ι} (hi : i ∈ s) :
⇑(b.coord i) (finset.centroid k s ⇑b) = (↑(s.card))⁻¹
source
theorem affine_basis.exists_affine_subbasis {k : Type u_3} {V : Type u_4} {P : Type u_5} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] {t : set P} (ht : affine_span k t = ⊤) :
∃ (s : set P) (H : s ⊆ t) (b : affine_basis ↥s k P), ⇑b = coe
source
theorem affine_basis.exists_affine_basis (k : Type u_3) (V : Type u_4) (P : Type u_5) [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] :
∃ (s : set P) (b : affine_basis ↥s k P), ⇑b = coe