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 map P →ᵃ[k] k corresponding to i : ι.
• AffineBasis.coord_apply_eq: the behaviour of AffineBasis.coord i on p i.
• AffineBasis.coord_apply_ne: the behaviour of AffineBasis.coord i on p j when j ≠ i.
• AffineBasis.coord_apply: the behaviour of AffineBasis.coord i on p j for general j.
• AffineBasis.coord_apply_combination: the characterisation of AffineBasis.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 }.

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

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) = ⊤

instance AffineBasis.instInhabitedPUnit {k : Type u_5} [Ring k] : Inhabited (AffineBasis PUnit.{u_8 + 1} k PUnit.{u_8 + 1})

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

Equations

• AffineBasis.instInhabitedPUnit = { default := { toFun := id, ind' := ⋯, tot' := ⋯ } }

instance AffineBasis.instFunLike {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] : FunLike (AffineBasis ι k P) ι P

Equations

• AffineBasis.instFunLike = { coe := AffineBasis.toFun, coe_injective' := ⋯ }

theorem AffineBasis.ext {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] {b₁ b₂ : AffineBasis ι k P} (h : ⇑b₁ = ⇑b₂) : b₁ = b₂

theorem AffineBasis.ind {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [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_5} {V : Type u_6} {P : Type u_7} [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_5} {V : Type u_6} {P : Type u_7} [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_5} {V : Type u_6} {P : Type u_7} [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.

Equations

• b.reindex e = { toFun := ⇑b ∘ ⇑e.symm, ind' := ⋯, tot' := ⋯ }

@[simp]

theorem AffineBasis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') : ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm

@[simp]

theorem AffineBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i' : ι') : (b.reindex e) i' = b (e.symm i')

@[simp]

theorem AffineBasis.reindex_refl {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) : b.reindex (Equiv.refl ι) = b

noncomputable def AffineBasis.basisOf {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι 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 basisOf_apply.)

Equations

• b.basisOf i = Basis.mk ⋯ ⋯

@[simp]

theorem AffineBasis.basisOf_apply {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) (j : { j : ι // j ≠ i }) : (b.basisOf i) j = b ↑j -ᵥ b i

@[simp]

theorem AffineBasis.basisOf_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i : ι') : (b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)

noncomputable def AffineBasis.coord {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) : P →ᵃ[k] k

The ith barycentric coordinate of a point.

Equations

• b.coord i = { toFun := fun (q : P) => 1 - (b.basisOf i).sumCoords (q -ᵥ b i), linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ }

@[simp]

theorem AffineBasis.linear_eq_sumCoords {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) : (b.coord i).linear = -(b.basisOf i).sumCoords

@[simp]

theorem AffineBasis.coord_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i : ι') : (b.reindex e).coord i = b.coord (e.symm i)

@[simp]

theorem AffineBasis.coord_apply_eq {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) : (b.coord i) (b i) = 1

@[simp]

theorem AffineBasis.coord_apply_ne {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {i j : ι} (h : i ≠ j) : (b.coord i) (b j) = 0

theorem AffineBasis.coord_apply {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [DecidableEq ι] (i j : ι) : (b.coord i) (b j) = if i = j then 1 else 0

@[simp]

theorem AffineBasis.coord_apply_combination_of_mem {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) : (b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i

@[simp]

theorem AffineBasis.coord_apply_combination_of_not_mem {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) : (b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0

@[simp]

theorem AffineBasis.sum_coord_apply_eq_one {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (q : P) : ∑ i : ι, (b.coord i) q = 1

@[simp]

theorem AffineBasis.affineCombination_coord_eq_self {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [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 : ι) => (b.coord i) q) = q

@[simp]

theorem AffineBasis.linear_combination_coord_eq_self {ι : Type u_1} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Fintype ι] (b : AffineBasis ι k V) (v : V) : ∑ i : ι, (b.coord 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_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Finite ι] {q₁ q₂ : P} (h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂) : q₁ = q₂

@[simp]

theorem AffineBasis.coe_coord_of_subsingleton_eq_one {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Subsingleton ι] (i : ι) : ⇑(b.coord i) = 1

theorem AffineBasis.surjective_coord {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Nontrivial ι] (i : ι) : Function.Surjective ⇑(b.coord i)

noncomputable def AffineBasis.coords {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) : P →ᵃ[k] ι → k

Barycentric coordinates as an affine map.

Equations

• b.coords = { toFun := fun (q : P) (i : ι) => (b.coord i) q, linear := { toFun := fun (v : V) (i : ι) => -(b.basisOf i).sumCoords v, map_add' := ⋯, map_smul' := ⋯ }, map_vadd' := ⋯ }

@[simp]

theorem AffineBasis.coords_apply {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (q : P) (i : ι) : b.coords q i = (b.coord i) q

instance AffineBasis.instVAdd {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] : VAdd V (AffineBasis ι k P)

Equations

• AffineBasis.instVAdd = { vadd := fun (x : V) (b : AffineBasis ι k P) => { toFun := x +ᵥ ⇑b, ind' := ⋯, tot' := ⋯ } }

@[simp]

theorem AffineBasis.coe_vadd {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (v : V) (b : AffineBasis ι k P) : ⇑(v +ᵥ b) = v +ᵥ ⇑b

@[simp]

theorem AffineBasis.basisOf_vadd {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (v : V) (b : AffineBasis ι k P) : (v +ᵥ b).basisOf = b.basisOf

instance AffineBasis.instAddAction {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] : AddAction V (AffineBasis ι k P)

Equations

• AffineBasis.instAddAction = Function.Injective.addAction (fun (f : AffineBasis ι k P) => ⇑f) ⋯ ⋯

@[simp]

theorem AffineBasis.coord_vadd {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] {i : ι} (v : V) (b : AffineBasis ι k P) : (v +ᵥ b).coord i = (b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm

instance AffineBasis.instSMul {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] : SMul G (AffineBasis ι k V)

In an affine space that is also a vector space, an AffineBasis can be scaled.

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineBasis ι k P), which acts on P with a VAdd version of a DistribMulAction.

Equations

• AffineBasis.instSMul = { smul := fun (a : G) (b : AffineBasis ι k V) => { toFun := a • ⇑b, ind' := ⋯, tot' := ⋯ } }

@[simp]

theorem AffineBasis.coe_smul {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] (a : G) (b : AffineBasis ι k V) : ⇑(a • b) = a • ⇑b

instance AffineBasis.instSMulCommClass {ι : Type u_1} {G : Type u_3} {G' : Type u_4} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [Group G'] [DistribMulAction G V] [DistribMulAction G' V] [SMulCommClass G k V] [SMulCommClass G' k V] [SMulCommClass G G' V] : SMulCommClass G G' (AffineBasis ι k V)

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineBasis ι k P), which acts on P with a VAdd version of a DistribMulAction.

instance AffineBasis.instIsScalarTower {ι : Type u_1} {G : Type u_3} {G' : Type u_4} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [Group G'] [DistribMulAction G V] [DistribMulAction G' V] [SMulCommClass G k V] [SMulCommClass G' k V] [SMul G G'] [IsScalarTower G G' V] : IsScalarTower G G' (AffineBasis ι k V)

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineBasis ι k P), which acts on P with a VAdd version of a DistribMulAction.

@[simp]

theorem AffineBasis.basisOf_smul {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] (a : G) (b : AffineBasis ι k V) (i : ι) : (a • b).basisOf i = a • b.basisOf i

@[simp]

theorem AffineBasis.reindex_smul {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] (a : G) (b : AffineBasis ι k V) (e : ι ≃ ι') : (a • b).reindex e = a • b.reindex e

@[simp]

theorem AffineBasis.coord_smul {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] (a : G) (b : AffineBasis ι k V) (i : ι) : (a • b).coord i = (b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap

instance AffineBasis.instMulAction {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [AddCommGroup V] [Ring k] [Module k V] [Group G] [DistribMulAction G V] [SMulCommClass G k V] : MulAction G (AffineBasis ι k V)

TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineBasis ι k P), which acts on P with a VAdd version of a DistribMulAction.

Equations

• AffineBasis.instMulAction = Function.Injective.mulAction (fun (f : AffineBasis ι k V) => ⇑f) ⋯ ⋯

@[simp]

theorem AffineBasis.coord_apply_centroid {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i ∈ s) : (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹

theorem AffineBasis.exists_affine_subbasis {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] {t : Set P} (ht : affineSpan k t = ⊤) : ∃ s ⊆ t, ∃ (b : AffineBasis (↑s) k P), ⇑b = Subtype.val

theorem AffineBasis.exists_affineBasis (k : Type u_5) (V : Type u_6) (P : Type u_7) [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] : ∃ (s : Set P) (b : AffineBasis (↑s) k P), ⇑b = Subtype.val