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 #
AffineBasis: a structure representing an affine basis of an affine space.AffineBasis.coord: the mapP →ᵃ[k] kcorresponding toi : ι.AffineBasis.coord_apply_eq: the behaviour ofAffineBasis.coord ionp i.AffineBasis.coord_apply_ne: the behaviour ofAffineBasis.coord ionp jwhenj ≠ i.AffineBasis.coord_apply: the behaviour ofAffineBasis.coord ionp jfor generalj.AffineBasis.coord_apply_combination: the characterisation ofAffineBasis.coord iin terms of affine combinations, i.e.,AffineBasis.coord i (w₀ p₀ + w₁ p₁ + ⋯) = wᵢ.
TODO #
- Construct the affine equivalence between
Pand{ f : ι →₀ k | f.sum = 1 }.
structure
AffineBasis
(ι : Type u₁)
(k : Type u₂)
{V : Type u₃}
(P : Type u₄)
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
:
Type (max u₁ u₄)
- 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
instance
AffineBasis.instInhabitedAffineBasisPUnitPUnitAddCommGroupAddGroupIsAddTorsorToAddGroupToAddGroupWithOneToRingCommRingModuleToSemiring
{k : Type u_3}
[Ring k]
:
The unique point in a single-point space is the simplest example of an affine basis.
instance
AffineBasis.funLike
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
:
FunLike (AffineBasis ι k P) ι fun x => P
theorem
AffineBasis.ext
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
{b₁ : AffineBasis ι k P}
{b₂ : AffineBasis ι k P}
(h : ↑b₁ = ↑b₂)
:
b₁ = b₂
theorem
AffineBasis.ind
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
:
AffineIndependent k ↑b
theorem
AffineBasis.tot
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
:
affineSpan k (Set.range ↑b) = ⊤
theorem
AffineBasis.nonempty
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
:
Nonempty ι
def
AffineBasis.reindex
{ι : Type u_1}
{ι' : Type u_2}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(e : ι ≃ ι')
:
AffineBasis ι' k P
Composition of an affine basis and an equivalence of index types.
Instances For
@[simp]
theorem
AffineBasis.coe_reindex
{ι : Type u_1}
{ι' : Type u_2}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(e : ι ≃ ι')
:
↑(AffineBasis.reindex b e) = ↑b ∘ ↑e.symm
@[simp]
theorem
AffineBasis.reindex_apply
{ι : Type u_1}
{ι' : Type u_2}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(e : ι ≃ ι')
(i' : ι')
:
↑(AffineBasis.reindex b e) i' = ↑b (↑e.symm i')
@[simp]
theorem
AffineBasis.reindex_refl
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
:
AffineBasis.reindex b (Equiv.refl ι) = b
noncomputable def
AffineBasis.basisOf
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(i : ι)
:
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 basisOf_apply.)
Instances For
@[simp]
theorem
AffineBasis.basisOf_apply
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(i : ι)
(j : { j // j ≠ i })
:
↑(AffineBasis.basisOf b i) j = ↑b ↑j -ᵥ ↑b i
@[simp]
theorem
AffineBasis.basisOf_reindex
{ι : Type u_1}
{ι' : Type u_2}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(e : ι ≃ ι')
(i : ι')
:
AffineBasis.basisOf (AffineBasis.reindex b e) i = Basis.reindex (AffineBasis.basisOf b (↑e.symm i)) (Equiv.subtypeEquiv e (_ : ∀ (x : ι), ¬x = ↑e.symm i ↔ ¬↑e x = i))
noncomputable def
AffineBasis.coord
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(i : ι)
:
The ith barycentric coordinate of a point.
Instances For
@[simp]
theorem
AffineBasis.linear_eq_sumCoords
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(i : ι)
:
(AffineBasis.coord b i).linear = -Basis.sumCoords (AffineBasis.basisOf b i)
@[simp]
theorem
AffineBasis.coord_reindex
{ι : Type u_1}
{ι' : Type u_2}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(e : ι ≃ ι')
(i : ι')
:
AffineBasis.coord (AffineBasis.reindex b e) i = AffineBasis.coord b (↑e.symm i)
@[simp]
theorem
AffineBasis.coord_apply_eq
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(i : ι)
:
↑(AffineBasis.coord b i) (↑b i) = 1
@[simp]
theorem
AffineBasis.coord_apply_ne
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
{i : ι}
{j : ι}
(h : i ≠ j)
:
↑(AffineBasis.coord b i) (↑b j) = 0
theorem
AffineBasis.coord_apply
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[DecidableEq ι]
(i : ι)
(j : ι)
:
↑(AffineBasis.coord b i) (↑b j) = if i = j then 1 else 0
@[simp]
theorem
AffineBasis.coord_apply_combination_of_mem
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
{s : Finset ι}
{i : ι}
(hi : i ∈ s)
{w : ι → k}
(hw : Finset.sum s w = 1)
:
↑(AffineBasis.coord b i) (↑(Finset.affineCombination k s ↑b) w) = w i
@[simp]
theorem
AffineBasis.coord_apply_combination_of_not_mem
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
{s : Finset ι}
{i : ι}
(hi : ¬i ∈ s)
{w : ι → k}
(hw : Finset.sum s w = 1)
:
↑(AffineBasis.coord b i) (↑(Finset.affineCombination k s ↑b) w) = 0
@[simp]
theorem
AffineBasis.sum_coord_apply_eq_one
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[Fintype ι]
(q : P)
:
(Finset.sum Finset.univ fun i => ↑(AffineBasis.coord b i) q) = 1
@[simp]
theorem
AffineBasis.affineCombination_coord_eq_self
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[Fintype ι]
(q : P)
:
(↑(Finset.affineCombination k Finset.univ ↑b) fun i => ↑(AffineBasis.coord b i) q) = q
@[simp]
theorem
AffineBasis.linear_combination_coord_eq_self
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
[AddCommGroup V]
[Ring k]
[Module k V]
[Fintype ι]
(b : AffineBasis ι k V)
(v : V)
:
(Finset.sum Finset.univ fun i => ↑(AffineBasis.coord b i) v • ↑b i) = v
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.
theorem
AffineBasis.ext_elem
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[Finite ι]
{q₁ : P}
{q₂ : P}
(h : ∀ (i : ι), ↑(AffineBasis.coord b i) q₁ = ↑(AffineBasis.coord b i) q₂)
:
q₁ = q₂
@[simp]
theorem
AffineBasis.coe_coord_of_subsingleton_eq_one
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[Subsingleton ι]
(i : ι)
:
↑(AffineBasis.coord b i) = 1
theorem
AffineBasis.surjective_coord
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
[Nontrivial ι]
(i : ι)
:
noncomputable def
AffineBasis.coords
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
:
Barycentric coordinates as an affine map.
Instances For
@[simp]
theorem
AffineBasis.coords_apply
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[Ring k]
[Module k V]
(b : AffineBasis ι k P)
(q : P)
(i : ι)
:
↑(AffineBasis.coords b) q i = ↑(AffineBasis.coord b i) q
@[simp]
theorem
AffineBasis.coord_apply_centroid
{ι : Type u_1}
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[DivisionRing k]
[Module k V]
[CharZero k]
(b : AffineBasis ι k P)
{s : Finset ι}
{i : ι}
(hi : i ∈ s)
:
↑(AffineBasis.coord b i) (Finset.centroid k s ↑b) = (↑(Finset.card s))⁻¹
theorem
AffineBasis.exists_affine_subbasis
{k : Type u_3}
{V : Type u_4}
{P : Type u_5}
[AddCommGroup V]
[AddTorsor V P]
[DivisionRing k]
[Module k V]
{t : Set P}
(ht : affineSpan k t = ⊤)
:
∃ s x b, ↑b = Subtype.val
theorem
AffineBasis.exists_affineBasis
(k : Type u_3)
(V : Type u_4)
(P : Type u_5)
[AddCommGroup V]
[AddTorsor V P]
[DivisionRing k]
[Module k V]
:
∃ s b, ↑b = Subtype.val