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 i
th
barycentric coordinate of q : P
is 1 - fᵢ (q -ᵥ p i)
.
Main definitions #
AffineBasis
: a structure representing an affine basis of an affine space.AffineBasis.coord
: the mapP →ᵃ[k] k
corresponding toi : ι
.AffineBasis.coord_apply_eq
: the behaviour ofAffineBasis.coord i
onp i
.AffineBasis.coord_apply_ne
: the behaviour ofAffineBasis.coord i
onp j
whenj ≠ i
.AffineBasis.coord_apply
: the behaviour ofAffineBasis.coord i
onp j
for generalj
.AffineBasis.coord_apply_combination
: the characterisation ofAffineBasis.coord i
in terms of affine combinations, i.e.,AffineBasis.coord i (w₀ p₀ + w₁ p₁ + ⋯) = wᵢ
.
TODO #
- Construct the affine equivalence between
P
and{ f : ι →₀ k | f.sum = 1 }
.
- toFun : ι → P
- ind' : AffineIndependent k s.toFun
- tot' : affineSpan k (Set.range s.toFun) = ⊤
An affine basis is a family of affine-independent points whose span is the top subspace.
Instances For
The unique point in a single-point space is the simplest example of an affine basis.
Composition of an affine basis and an equivalence of index types.
Instances For
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 j
th element is b j -ᵥ b i
. (See basisOf_apply
.)
Instances For
The i
th barycentric coordinate of a point.
Instances For
A variant of AffineBasis.affineCombination_coord_eq_self
for the special case when the
affine space is a module so we can talk about linear combinations.
Barycentric coordinates as an affine map.