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 }
.
An affine basis is a family of affine-independent points whose span is the top subspace.
- toFun : ι → P
- ind' : AffineIndependent k self.toFun
- tot' : affineSpan k (Set.range self.toFun) = ⊤
Instances For
The unique point in a single-point space is the simplest example of an affine basis.
Equations
- AffineBasis.instInhabitedAffineBasisPUnitPUnitAddCommGroupAddGroupIsAddTorsorToAddGroupToAddGroupWithOneToRingCommRingModuleToSemiring = { default := { toFun := id, ind' := ⋯, tot' := ⋯ } }
Equations
- AffineBasis.instFunLike = { coe := AffineBasis.toFun, coe_injective' := ⋯ }
Composition of an affine basis and an equivalence of index types.
Equations
- AffineBasis.reindex b e = { toFun := ⇑b ∘ ⇑e.symm, ind' := ⋯, tot' := ⋯ }
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
.)
Equations
- AffineBasis.basisOf b i = Basis.mk ⋯ ⋯
Instances For
The i
th barycentric coordinate of a point.
Equations
- AffineBasis.coord b i = { toFun := fun (q : P) => 1 - (Basis.sumCoords (AffineBasis.basisOf b i)) (q -ᵥ b i), linear := -Basis.sumCoords (AffineBasis.basisOf b i), map_vadd' := ⋯ }
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.
Equations
- One or more equations did not get rendered due to their size.