Mathlib.LinearAlgebra.AffineSpace.Basis

AffineBasis structure

 (ι : Type u₁) (k : Type u₂) {V : Type u₃} (P : Type u₄) [AddCommGroup V] [AffineSpace V P] [Ring k] [Module k V]

Full source

/-- An affine basis is a family of affine-independent points whose span is the top subspace. -/
structure AffineBasis (ι : Type u₁) (k : Type u₂) {V : Type u₃} (P : Type u₄) [AddCommGroup V]
  [AffineSpace V P] [Ring k] [Module k V] where
  protected toFun : ι → P
  protected ind' : AffineIndependent k toFun
  protected tot' : affineSpan k (range toFun) = ⊤

Affine Basis

Informal description

An affine basis is a structure representing a family of affine-independent points in an affine space $P$ over a ring $k$ with associated module $V$, such that the affine span of these points is the entire space $P$. Here, $\iota$ is the indexing type for the basis points.

AffineBasis.instInhabitedPUnit instance

: Inhabited (AffineBasis PUnit k PUnit)

Full source

/-- The unique point in a single-point space is the simplest example of an affine basis. -/
instance : Inhabited (AffineBasis PUnit k PUnit) :=
  ⟨⟨id, affineIndependent_of_subsingleton k id, by simp⟩⟩

Canonical Affine Basis of the Single-Point Space

Informal description

The single-point affine space `PUnit` has a canonical affine basis consisting of its unique point.

AffineBasis.instFunLike instance

: FunLike (AffineBasis ι k P) ι P

Full source

instance instFunLike : FunLike (AffineBasis ι k P) ι P where
  coe := AffineBasis.toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure for Affine Bases

Informal description

For any affine basis `b : AffineBasis ι k P`, the structure `AffineBasis ι k P` is equipped with a function-like structure that allows its elements to be treated as functions from the index type `ι` to the affine space `P`.

AffineBasis.ext theorem

{b₁ b₂ : AffineBasis ι k P} (h : (b₁ : ι → P) = b₂) : b₁ = b₂

Full source

@[ext]
theorem ext {b₁ b₂ : AffineBasis ι k P} (h : (b₁ : ι → P) = b₂) : b₁ = b₂ :=
  DFunLike.coe_injective h

Extensionality of Affine Bases: $b₁ = b₂$ if their point families coincide

Informal description

Let $b₁$ and $b₂$ be two affine bases of an affine space $P$ over a ring $k$, indexed by $\iota$. If the underlying point families $b₁$ and $b₂$ are equal as functions from $\iota$ to $P$, then $b₁$ and $b₂$ are equal as affine bases.

AffineBasis.ind theorem

: AffineIndependent k b

Full source

theorem ind : AffineIndependent k b :=
  b.ind'

Affine Independence of Affine Basis Points

Informal description

Given an affine basis $b$ indexed by $\iota$ in an affine space $P$ over a ring $k$ with associated module $V$, the family of points $b_i$ is affine-independent. This means that for any finite subset $S \subseteq \iota$ and any weights $w_i \in k$ such that $\sum_{i \in S} w_i = 0$, the condition $\sum_{i \in S} w_i (b_i - b_j) = 0$ implies $w_i = 0$ for all $i \in S$.

AffineBasis.tot theorem

: affineSpan k (range b) = ⊤

Full source

theorem tot : affineSpan k (range b) = ⊤ :=
  b.tot'

Affine Span of Basis Covers Entire Space

Informal description

Given an affine basis $b : \iota \to P$ of an affine space $P$ over a ring $k$, the affine span of the range of $b$ is equal to the entire space $P$. In other words, the affine subspace generated by the points $\{b_i\}_{i \in \iota}$ is the whole space $P$.

AffineBasis.nonempty theorem

: Nonempty ι

Full source

protected theorem nonempty : Nonempty ι :=
  not_isEmpty_iff.mp fun hι => by
    simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot

Nonemptiness of Affine Basis Index Set

Informal description

The indexing type $\iota$ for an affine basis is nonempty, i.e., there exists at least one index in $\iota$.

AffineBasis.reindex definition

(e : ι ≃ ι') : AffineBasis ι' k P

Full source

/-- Composition of an affine basis and an equivalence of index types. -/
def reindex (e : ι ≃ ι') : AffineBasis ι' k P :=
  ⟨b ∘ e.symm, b.ind.comp_embedding e.symm.toEmbedding, by
    rw [e.symm.surjective.range_comp]
    exact b.3⟩

Reindexing of an affine basis via an equivalence

Informal description

Given an affine basis $b$ indexed by type $\iota$ and an equivalence $e : \iota \simeq \iota'$ between index types, the reindexed affine basis $b \circ e^{-1}$ is an affine basis indexed by $\iota'$. Here, $e^{-1}$ denotes the inverse of the equivalence $e$, and the reindexed basis maps each $i' \in \iota'$ to $b(e^{-1}(i'))$.

AffineBasis.coe_reindex theorem

: ⇑(b.reindex e) = b ∘ e.symm

Full source

@[simp, norm_cast]
theorem coe_reindex : ⇑(b.reindex e) = b ∘ e.symm :=
  rfl

Reindexed Affine Basis as Composition with Inverse Equivalence

Informal description

Let $b$ be an affine basis indexed by $\iota$ for an affine space $P$ over a ring $k$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then the reindexed affine basis $b \circ e^{-1}$ is equal to the composition of $b$ with the inverse of $e$, i.e., $b \circ e^{-1} = b \circ e^{-1}$.

AffineBasis.reindex_apply theorem

(i' : ι') : b.reindex e i' = b (e.symm i')

Full source

@[simp]
theorem reindex_apply (i' : ι') : b.reindex e i' = b (e.symm i') :=
  rfl

Reindexed Affine Basis Evaluation via Equivalence Inverse

Informal description

Let $b$ be an affine basis indexed by $\iota$ for an affine space $P$ over a ring $k$ with associated module $V$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then for any $i' \in \iota'$, the reindexed affine basis satisfies $(b \circ e^{-1})(i') = b(e^{-1}(i'))$.

AffineBasis.reindex_refl theorem

: b.reindex (Equiv.refl _) = b

Full source

@[simp]
theorem reindex_refl : b.reindex (Equiv.refl _) = b :=
  ext rfl

Reindexing an Affine Basis by the Identity Equivalence Preserves the Basis

Informal description

Let $b$ be an affine basis indexed by type $\iota$ for an affine space $P$ over a ring $k$. Then reindexing $b$ with the identity equivalence on $\iota$ yields $b$ itself, i.e., $b \circ \text{id}^{-1} = b$.

AffineBasis.basisOf definition

(i : ι) : Basis { j : ι // j ≠ i } k V

Full source

/-- 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`.) -/
noncomputable def basisOf (i : ι) : Basis { j : ι // j ≠ i } k V :=
  Basis.mk ((affineIndependent_iff_linearIndependent_vsub k b i).mp b.ind)
    (by
      suffices
        Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
        rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
      conv_rhs => rw [← image_univ]
      rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]
      congr
      ext v
      simp)

Linear basis induced by an affine basis at a point

Informal description

Given an affine basis `b : AffineBasis ι k P` and a fixed index `i : ι`, the function `AffineBasis.basisOf` constructs a linear basis for the model space `V` over the ring `k`. The basis vectors are indexed by the subtype `{j : ι // j ≠ i}`, and for each `j` in this subtype, the corresponding basis vector is defined as the difference `b j -ᵥ b i` in the affine space `P`.

AffineBasis.basisOf_apply theorem

(i : ι) (j : { j : ι // j ≠ i }) : b.basisOf i j = b ↑j -ᵥ b i

Full source

@[simp]
theorem basisOf_apply (i : ι) (j : { j : ι // j ≠ i }) : b.basisOf i j = b ↑j -ᵥ b i := by
  simp [basisOf]

Basis Vector as Affine Difference: $\text{basisOf}_i(j) = b(j) - b(i)$

Informal description

Let $b$ be an affine basis for an affine space $P$ over a ring $k$ with associated module $V$. For any index $i \in \iota$ and any index $j \in \{j \in \iota \mid j \neq i\}$, the $j$-th vector of the linear basis $\text{basisOf}_i$ of $V$ is given by the difference $b(j) - b(i)$ in the affine space $P$.

AffineBasis.basisOf_reindex theorem

(i : ι') : (b.reindex e).basisOf i = (b.basisOf <| e.symm i).reindex (e.subtypeEquiv fun _ => e.eq_symm_apply.not)

Full source

@[simp]
theorem basisOf_reindex (i : ι') :
    (b.reindex e).basisOf i =
      (b.basisOf <| e.symm i).reindex (e.subtypeEquiv fun _ => e.eq_symm_apply.not) := by
  ext j
  simp

Reindexed Affine Basis Induces Reindexed Linear Basis: $(b \circ e^{-1}).\text{basisOf}_i = (b.\text{basisOf}_{e^{-1}(i)}).\text{reindex}$

Informal description

Let $b$ be an affine basis for an affine space $P$ over a ring $k$ with associated module $V$, indexed by a type $\iota$. Given an equivalence $e : \iota \simeq \iota'$ between index types and a fixed index $i \in \iota'$, the linear basis $(b \circ e^{-1}).\text{basisOf}_i$ of $V$ is equal to the reindexing of the linear basis $b.\text{basisOf}_{e^{-1}(i)}$ via the equivalence of subtypes induced by $e$. Specifically, the reindexing is given by the equivalence: $$ \{j \in \iota \mid j \neq e^{-1}(i)\} \simeq \{j' \in \iota' \mid j' \neq i\} $$ which maps $j$ to $e(j)$ and has inverse mapping $j'$ to $e^{-1}(j')$.

AffineBasis.coord definition

(i : ι) : P →ᵃ[k] k

Full source

/-- The `i`th barycentric coordinate of a point. -/
noncomputable def coord (i : ι) : P →ᵃ[k] k where
  toFun q := 1 - (b.basisOf i).sumCoords (q -ᵥ b i)
  linear := -(b.basisOf i).sumCoords
  map_vadd' q v := by
    rw [vadd_vsub_assoc, LinearMap.map_add, vadd_eq_add, LinearMap.neg_apply,
      sub_add_eq_sub_sub_swap, add_comm, sub_eq_add_neg]

Barycentric coordinate function for an affine basis

Informal description

For an affine basis `b : AffineBasis ι k P` and a fixed index `i : ι`, the function `AffineBasis.coord i` is the affine map from the affine space `P` to the ring `k` that computes the $i$-th barycentric coordinate of a point `q ∈ P`. Specifically, it is defined by: \[ \text{AffineBasis.coord}_i(q) = 1 - \sum_{j \neq i} f_j(q -ᵥ p_i) \] where `f_j` are the dual basis vectors corresponding to the linear basis `b.basisOf i` of the model space `V`, and `p_i = b i` is the $i$-th point in the affine basis.

AffineBasis.linear_eq_sumCoords theorem

(i : ι) : (b.coord i).linear = -(b.basisOf i).sumCoords

Full source

@[simp]
theorem linear_eq_sumCoords (i : ι) : (b.coord i).linear = -(b.basisOf i).sumCoords :=
  rfl

Linear Part of Barycentric Coordinate Equals Negative Sum of Coordinates

Informal description

For an affine basis `b : AffineBasis ι k P` and a fixed index `i : ι`, the linear part of the barycentric coordinate function `b.coord i` is equal to the negation of the sum of coordinates linear map with respect to the linear basis `b.basisOf i`. That is, the linear map associated with the $i$-th barycentric coordinate function satisfies: \[ \text{linear}(b.\text{coord}_i) = -(\text{basisOf } i).\text{sumCoords} \]

AffineBasis.coord_reindex theorem

(i : ι') : (b.reindex e).coord i = b.coord (e.symm i)

Full source

@[simp]
theorem coord_reindex (i : ι') : (b.reindex e).coord i = b.coord (e.symm i) := by
  ext
  classical simp [AffineBasis.coord]

Reindexing Invariance of Barycentric Coordinates: $(b \circ e^{-1}).\text{coord}_i = b.\text{coord}_{e^{-1}(i)}$

Informal description

Let $b$ be an affine basis for an affine space $P$ over a ring $k$ with associated module $V$, indexed by a type $\iota$. Given an equivalence $e : \iota \simeq \iota'$ between index types and a fixed index $i \in \iota'$, the $i$-th barycentric coordinate function of the reindexed affine basis $b \circ e^{-1}$ is equal to the $(e^{-1}(i))$-th barycentric coordinate function of the original basis $b$. That is, $$(b \circ e^{-1}).\text{coord}_i = b.\text{coord}_{e^{-1}(i)}.$$

AffineBasis.coord_apply_eq theorem

(i : ι) : b.coord i (b i) = 1

Full source

@[simp]
theorem coord_apply_eq (i : ι) : b.coord i (b i) = 1 := by
  simp only [coord, Basis.coe_sumCoords, LinearEquiv.map_zero, LinearEquiv.coe_coe, sub_zero,
    AffineMap.coe_mk, Finsupp.sum_zero_index, vsub_self]

Barycentric Coordinate Identity at Basis Point: $\text{coord}_i(b(i)) = 1$

Informal description

For any affine basis $b$ indexed by $\iota$ and any index $i \in \iota$, the $i$-th barycentric coordinate function evaluated at the basis point $b(i)$ equals $1$, i.e., \[ \text{coord}_i(b(i)) = 1. \]

AffineBasis.coord_apply_ne theorem

(h : i ≠ j) : b.coord i (b j) = 0

Full source

@[simp]
theorem coord_apply_ne (h : i ≠ j) : b.coord i (b j) = 0 := by
  rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]

Barycentric Coordinate Vanishes at Distinct Basis Points: $\text{coord}_i(b(j)) = 0$ for $i \neq j$

Informal description

For any affine basis $b$ indexed by $\iota$ and any distinct indices $i, j \in \iota$, the $i$-th barycentric coordinate function evaluated at the basis point $b(j)$ equals $0$, i.e., \[ \text{coord}_i(b(j)) = 0. \]

AffineBasis.coord_apply theorem

[DecidableEq ι] (i j : ι) : b.coord i (b j) = if i = j then 1 else 0

Full source

theorem coord_apply [DecidableEq ι] (i j : ι) : b.coord i (b j) = if i = j then 1 else 0 := by
  rcases eq_or_ne i j with h | h <;> simp [h]

Barycentric Coordinate Evaluation: $\text{coord}_i(b(j)) = \delta_{ij}$

Informal description

For any affine basis $b$ indexed by $\iota$ and any indices $i, j \in \iota$, the $i$-th barycentric coordinate function evaluated at the basis point $b(j)$ satisfies: \[ \text{coord}_i(b(j)) = \begin{cases} 1 & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases} \]

AffineBasis.coord_apply_combination_of_mem theorem

(hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) : b.coord i (s.affineCombination k b w) = w i

Full source

@[simp]
theorem coord_apply_combination_of_mem (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :
    b.coord i (s.affineCombination k b w) = w i := by
  classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true,
      mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
      s.map_affineCombination b w hw]

Barycentric Coordinate of Affine Combination: $\text{coord}_i(\sum w_j b_j) = w_i$ for $i \in s$

Informal description

Let $b$ be an affine basis indexed by $\iota$ for an affine space $P$ over a ring $k$, and let $s$ be a finite subset of $\iota$. For any index $i \in s$ and any weight function $w : \iota \to k$ such that $\sum_{j \in s} w_j = 1$, the $i$-th barycentric coordinate of the affine combination $\sum_{j \in s} w_j b_j$ is equal to $w_i$, i.e., \[ \text{coord}_i\left(\sum_{j \in s} w_j b_j\right) = w_i. \]

AffineBasis.coord_apply_combination_of_not_mem theorem

(hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) : b.coord i (s.affineCombination k b w) = 0

Full source

@[simp]
theorem coord_apply_combination_of_not_mem (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :
    b.coord i (s.affineCombination k b w) = 0 := by
  classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false,
      mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
      s.map_affineCombination b w hw]

Vanishing of Barycentric Coordinate Outside Support

Informal description

Let $b$ be an affine basis indexed by $\iota$ for an affine space $P$ over a ring $k$ with associated module $V$. For any finite subset $s \subseteq \iota$ and any index $i \notin s$, if $w : \iota \to k$ is a weight function such that $\sum_{j \in s} w_j = 1$, then the $i$-th barycentric coordinate of the affine combination $\sum_{j \in s} w_j b(j)$ is zero, i.e., \[ \text{coord}_i\left(\sum_{j \in s} w_j b(j)\right) = 0. \]

AffineBasis.sum_coord_apply_eq_one theorem

[Fintype ι] (q : P) : ∑ i, b.coord i q = 1

Full source

@[simp]
theorem sum_coord_apply_eq_one [Fintype ι] (q : P) : ∑ i, b.coord i q = 1 := by
  have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q
  obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
  convert hw
  exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw

Sum of Barycentric Coordinates Equals One

Informal description

Let $P$ be an affine space over a ring $k$ with associated module $V$, and let $b$ be an affine basis indexed by a finite type $\iota$. For any point $q \in P$, the sum of its barycentric coordinates with respect to $b$ is equal to $1$, i.e., \[ \sum_{i \in \iota} \text{coord}_i(q) = 1. \]

AffineBasis.affineCombination_coord_eq_self theorem

[Fintype ι] (q : P) : (Finset.univ.affineCombination k b fun i => b.coord i q) = q

Full source

@[simp]
theorem affineCombination_coord_eq_self [Fintype ι] (q : P) :
    (Finset.univ.affineCombination k b fun i => b.coord i q) = q := by
  have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q
  obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
  congr
  ext i
  exact b.coord_apply_combination_of_mem (Finset.mem_univ i) hw

Reconstruction of Point from Barycentric Coordinates

Informal description

Let $P$ be an affine space over a ring $k$ with an affine basis $b$ indexed by a finite type $\iota$. For any point $q \in P$, the affine combination of the basis points $b_i$ with weights given by their barycentric coordinates $\text{coord}_i(q)$ equals $q$ itself, i.e., \[ \sum_{i \in \iota} \text{coord}_i(q) \cdot b_i = q. \]

AffineBasis.linear_combination_coord_eq_self theorem

[Fintype ι] (b : AffineBasis ι k V) (v : V) : ∑ i, b.coord i v • b i = v

Full source

/-- 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. -/
@[simp]
theorem linear_combination_coord_eq_self [Fintype ι] (b : AffineBasis ι k V) (v : V) :
    ∑ i, b.coord i v • b i = v := by
  have hb := b.affineCombination_coord_eq_self v
  rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb

Reconstruction of Vector from Barycentric Coordinates in Module Setting

Informal description

Let $V$ be a module over a ring $k$ with an affine basis $b$ indexed by a finite type $\iota$. For any vector $v \in V$, the linear combination of the basis points $b_i$ with coefficients given by their barycentric coordinates $\text{coord}_i(v)$ equals $v$ itself, i.e., \[ \sum_{i \in \iota} \text{coord}_i(v) \cdot b_i = v. \]

AffineBasis.ext_elem theorem

[Finite ι] {q₁ q₂ : P} (h : ∀ i, b.coord i q₁ = b.coord i q₂) : q₁ = q₂

Full source

theorem ext_elem [Finite ι] {q₁ q₂ : P} (h : ∀ i, b.coord i q₁ = b.coord i q₂) : q₁ = q₂ := by
  cases nonempty_fintype ι
  rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]
  simp only [h]

Uniqueness of Points via Barycentric Coordinates in Finite-Dimensional Affine Spaces

Informal description

Let $P$ be an affine space over a ring $k$ with an affine basis $b$ indexed by a finite type $\iota$. For any two points $q_1, q_2 \in P$, if their barycentric coordinates coincide for all indices $i \in \iota$, then $q_1 = q_2$. In other words, a point in $P$ is uniquely determined by its barycentric coordinates with respect to the affine basis $b$.

AffineBasis.coe_coord_of_subsingleton_eq_one theorem

[Subsingleton ι] (i : ι) : (b.coord i : P → k) = 1

Full source

@[simp]
theorem coe_coord_of_subsingleton_eq_one [Subsingleton ι] (i : ι) : (b.coord i : P → k) = 1 := by
  ext q
  have hp : (range b).Subsingleton := by
    rw [← image_univ]
    apply Subsingleton.image
    apply subsingleton_of_subsingleton
  haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
  let s : Finset ι := {i}
  have hi : i ∈ s := by simp [s]
  have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp [s]
  have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by
    simp [eq_iff_true_of_subsingleton]
  rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]

Barycentric Coordinate is Constant One for Subsingleton Index Sets

Informal description

Let $b$ be an affine basis for an affine space $P$ over a ring $k$, where the indexing set $\iota$ is a subsingleton (i.e., contains at most one element). Then for any index $i \in \iota$, the $i$-th barycentric coordinate function $\text{coord}_i : P \to k$ is identically equal to the constant function $1$.

AffineBasis.surjective_coord theorem

[Nontrivial ι] (i : ι) : Function.Surjective <| b.coord i

Full source

theorem surjective_coord [Nontrivial ι] (i : ι) : Function.Surjective <| b.coord i := by
  classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]

Surjectivity of Barycentric Coordinate Functions in Nontrivial Affine Bases

Informal description

Let $b$ be an affine basis for an affine space $P$ over a ring $k$, with indexing set $\iota$ that is nontrivial (i.e., contains at least two distinct elements). Then for any index $i \in \iota$, the barycentric coordinate function $\text{coord}_i : P \to k$ is surjective. That is, for every $c \in k$, there exists a point $q \in P$ such that $\text{coord}_i(q) = c$.

AffineBasis.coords definition

: P →ᵃ[k] ι → k

Full source

/-- Barycentric coordinates as an affine map. -/
noncomputable def coords : P →ᵃ[k] ι → k where
  toFun q i := b.coord i q
  linear :=
    { toFun := fun v i => -(b.basisOf i).sumCoords v
      map_add' := fun v w => by ext; simp only [LinearMap.map_add, Pi.add_apply, neg_add]
      map_smul' := fun t v => by ext; simp }
  map_vadd' p v := by ext; simp

Barycentric coordinates as an affine map

Informal description

The affine map that sends a point $ q $ in the affine space $ P $ to the function $ \iota \to k $ which assigns to each index $ i $ the $ i $-th barycentric coordinate of $ q $ with respect to the affine basis $ b $. More precisely, for each $ q \in P $, the function $ b.\text{coords}(q) $ is defined by $ b.\text{coords}(q)(i) = b.\text{coord}_i(q) $, where $ b.\text{coord}_i $ is the $ i $-th barycentric coordinate function. The linear part of this affine map is given by $ v \mapsto -\sum_{j \neq i} f_j(v) $ for each $ i $, where $ f_j $ are the dual basis vectors corresponding to the linear basis $ b.\text{basisOf}(i) $.

AffineBasis.coords_apply theorem

(q : P) (i : ι) : b.coords q i = b.coord i q

Full source

@[simp]
theorem coords_apply (q : P) (i : ι) : b.coords q i = b.coord i q :=
  rfl

Equality of Barycentric Coordinate Components and Coordinate Function

Informal description

For any point $q$ in the affine space $P$ and any index $i$ in the indexing set $\iota$, the $i$-th component of the barycentric coordinates map $\text{coords}(q)$ is equal to the $i$-th barycentric coordinate function evaluated at $q$, i.e., \[ \text{coords}(q)(i) = \text{coord}_i(q). \]

AffineBasis.instVAdd instance

: VAdd V (AffineBasis ι k P)

Full source

instance instVAdd : VAdd V (AffineBasis ι k P) where
  vadd x b :=
    { toFun := x +ᵥ ⇑b,
      ind' := b.ind'.vadd,
      tot' := by rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_top] }

Vector Addition on Affine Bases

Informal description

For any affine space $P$ with associated module $V$ over a ring $k$, the type of affine bases $\text{AffineBasis}(\iota, k, P)$ is equipped with a vector addition operation, where adding a vector $v \in V$ to an affine basis $b$ results in a new affine basis obtained by translating each point in $b$ by $v$.

AffineBasis.coe_vadd theorem

(v : V) (b : AffineBasis ι k P) : ⇑(v +ᵥ b) = v +ᵥ ⇑b

Full source

@[simp, norm_cast] lemma coe_vadd (v : V) (b : AffineBasis ι k P) : ⇑(v +ᵥ b) = v +ᵥ ⇑b := rfl

Translation of Affine Basis by Vector Preserves Function Representation

Informal description

For any vector $v \in V$ and any affine basis $b$ of an affine space $P$ over a ring $k$ with associated module $V$, the function representation of the translated affine basis $v +ᵥ b$ is equal to the translation of the function representation of $b$ by $v$. In other words, the evaluation of $v +ᵥ b$ at any index is given by $v +ᵥ (b(i))$.

AffineBasis.basisOf_vadd theorem

(v : V) (b : AffineBasis ι k P) : (v +ᵥ b).basisOf = b.basisOf

Full source

@[simp] lemma basisOf_vadd (v : V) (b : AffineBasis ι k P) : (v +ᵥ b).basisOf = b.basisOf := by
  ext
  simp

Invariance of Induced Linear Basis under Affine Translation: $(v +ᵥ b).\text{basisOf} = b.\text{basisOf}$

Informal description

Let $V$ be a module over a ring $k$, and let $P$ be an affine space with associated module $V$. Given an affine basis $b$ of $P$ indexed by $\iota$ and a vector $v \in V$, the linear basis $(v +ᵥ b).\text{basisOf}$ induced by the translated affine basis $v +ᵥ b$ is equal to the original linear basis $b.\text{basisOf}$.

AffineBasis.instAddAction instance

: AddAction V (AffineBasis ι k P)

Full source

instance instAddAction : AddAction V (AffineBasis ι k P) :=
  DFunLike.coe_injective.addAction _ coe_vadd

Additive Action on Affine Bases by Vectors

Informal description

For any affine space $P$ with associated module $V$ over a ring $k$, the type of affine bases $\text{AffineBasis}(\iota, k, P)$ is equipped with an additive action by $V$. This means that for any vector $v \in V$ and any affine basis $b$, the translation $v +ᵥ b$ is well-defined and satisfies the axioms of an additive action.

AffineBasis.coord_vadd theorem

(v : V) (b : AffineBasis ι k P) : (v +ᵥ b).coord i = (b.coord i).comp (AffineEquiv.constVAdd k P v).symm

Full source

@[simp] lemma coord_vadd (v : V) (b : AffineBasis ι k P) :
    (v +ᵥ b).coord i = (b.coord i).comp (AffineEquiv.constVAdd k P v).symm := by
  ext p
  simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords,
    AffineMap.coe_mk, AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap,
    Function.comp_apply, AffineEquiv.constVAdd_apply, sub_right_inj]
  congr! 1
  rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]

Behavior of Barycentric Coordinates under Affine Translation: $(v +ᵥ b).\text{coord}_i = b.\text{coord}_i \circ (v +ᵥ \cdot)^{-1}$

Informal description

Let $P$ be an affine space with associated vector space $V$ over a ring $k$, and let $b$ be an affine basis for $P$ indexed by $\iota$. For any vector $v \in V$ and any index $i \in \iota$, the $i$-th barycentric coordinate function of the translated affine basis $v +ᵥ b$ is equal to the composition of the original $i$-th barycentric coordinate function $b.\text{coord}_i$ with the inverse of the affine automorphism given by translation by $v$. In other words, for any point $q \in P$, we have: $$(v +ᵥ b).\text{coord}_i(q) = b.\text{coord}_i(v +ᵥ q)$$

AffineBasis.instSMul instance

: SMul G (AffineBasis ι k V)

Full source

/-- 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`. -/
instance instSMul : SMul G (AffineBasis ι k V) where
  smul a b :=
    { toFun := a • ⇑b,
      ind' := b.ind'.smul,
      tot' := by
        rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)] }

Scalar Multiplication on Affine Bases by Group Actions

Informal description

For any group $G$ acting on a vector space $V$ over a ring $k$, there is a corresponding scalar multiplication operation of $G$ on the affine basis $\text{AffineBasis} \, \iota \, k \, V$ of the affine space associated to $V$.

AffineBasis.coe_smul theorem

(a : G) (b : AffineBasis ι k V) : ⇑(a • b) = a • ⇑b

Full source

@[simp, norm_cast] lemma coe_smul (a : G) (b : AffineBasis ι k V) : ⇑(a • b) = a • ⇑b := rfl

Scalar Multiplication Commutes with Affine Basis Evaluation

Informal description

Let $G$ be a group acting on a vector space $V$ over a ring $k$, and let $b$ be an affine basis for the affine space associated to $V$ indexed by $\iota$. For any element $a \in G$, the function associated to the scalar multiple $a \cdot b$ is equal to the pointwise scalar multiplication of $a$ with the function associated to $b$, i.e., $(a \cdot b)(i) = a \cdot b(i)$ for all $i \in \iota$.

AffineBasis.instSMulCommClass instance

[SMulCommClass G G' V] : SMulCommClass G G' (AffineBasis ι k V)

Full source

/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
instance [SMulCommClass G G' V] : SMulCommClass G G' (AffineBasis ι k V) where
  smul_comm _g _g' _b := DFunLike.ext _ _ fun _ => smul_comm _ _ _

Commuting Scalar Actions on Affine Bases

Informal description

For any two groups $G$ and $G'$ acting on a vector space $V$ over a ring $k$ with commuting scalar multiplications (i.e., $a \cdot (b \cdot v) = b \cdot (a \cdot v)$ for all $a \in G$, $b \in G'$, $v \in V$), the scalar multiplications of $G$ and $G'$ on the affine basis $\text{AffineBasis} \, \iota \, k \, V$ also commute.

AffineBasis.instIsScalarTower instance

[SMul G G'] [IsScalarTower G G' V] : IsScalarTower G G' (AffineBasis ι k V)

Full source

/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
instance [SMul G G'] [IsScalarTower G G' V] : IsScalarTower G G' (AffineBasis ι k V) where
  smul_assoc _g _g' _b := DFunLike.ext _ _ fun _ => smul_assoc _ _ _

Scalar Tower Property for Affine Bases

Informal description

For any groups $G$ and $G'$ acting on a vector space $V$ over a ring $k$, if $G$ and $G'$ form a scalar tower on $V$ (i.e., the actions of $G$ and $G'$ on $V$ commute), then they also form a scalar tower on the affine basis $\text{AffineBasis} \, \iota \, k \, V$ of the affine space associated to $V$.

AffineBasis.basisOf_smul theorem

(a : G) (b : AffineBasis ι k V) (i : ι) : (a • b).basisOf i = a • b.basisOf i

Full source

@[simp] lemma basisOf_smul (a : G) (b : AffineBasis ι k V) (i : ι) :
    (a • b).basisOf i = a • b.basisOf i := by ext j; simp [smul_sub]

Scalar Multiplication Commutes with Basis Construction: $(a \cdot b).\text{basisOf}_i = a \cdot (b.\text{basisOf}_i)$

Informal description

Let $G$ be a group acting on a vector space $V$ over a ring $k$, and let $b$ be an affine basis for an affine space $P$ modeled on $V$. For any element $a \in G$ and any index $i \in \iota$, the linear basis of $V$ induced by the scaled affine basis $a \cdot b$ at $i$ is equal to the scaled version of the linear basis induced by $b$ at $i$, i.e., $(a \cdot b).\text{basisOf}_i = a \cdot (b.\text{basisOf}_i)$.

AffineBasis.reindex_smul theorem

(a : G) (b : AffineBasis ι k V) (e : ι ≃ ι') : (a • b).reindex e = a • b.reindex e

Full source

@[simp] lemma reindex_smul (a : G) (b : AffineBasis ι k V) (e : ι ≃ ι') :
    (a • b).reindex e = a • b.reindex e :=
  rfl

Commutativity of Scalar Multiplication and Reindexing for Affine Bases

Informal description

Let $G$ be a group acting on an affine space $P$ with affine basis $b$ indexed by $\iota$, and let $e : \iota \simeq \iota'$ be an equivalence between index types. Then, for any $a \in G$, the reindexed basis $(a \cdot b) \circ e^{-1}$ is equal to $a \cdot (b \circ e^{-1})$. In other words, scalar multiplication by $a$ commutes with reindexing the affine basis $b$ via $e$.

AffineBasis.coord_smul theorem

 (a : G) (b : AffineBasis ι k V) (i : ι) :
  (a • b).coord i = (b.coord i).comp (DistribMulAction.toLinearEquiv _ _ a).symm.toAffineMap

Full source

@[simp] lemma coord_smul (a : G) (b : AffineBasis ι k V) (i : ι) :
    (a • b).coord i = (b.coord i).comp (DistribMulAction.toLinearEquiv _ _ a).symm.toAffineMap := by
  ext v; simp [map_sub, coord]

Behavior of Barycentric Coordinates under Group Action: $(a \cdot b).\text{coord}_i = b.\text{coord}_i \circ \varphi_a^{-1}$

Informal description

Let $G$ be a group acting on a vector space $V$ over a ring $k$, and let $b$ be an affine basis for an affine space $P$ modeled on $V$. For any element $a \in G$ and any index $i \in \iota$, the $i$-th barycentric coordinate function of the scaled affine basis $a \cdot b$ is equal to the composition of the $i$-th barycentric coordinate function of $b$ with the affine map induced by the inverse of the linear equivalence corresponding to the action of $a$ on $V$. In other words, $(a \cdot b).\text{coord}_i = b.\text{coord}_i \circ \varphi_a^{-1}$, where $\varphi_a$ is the linear automorphism of $V$ induced by $a$.

AffineBasis.instMulAction instance

: MulAction G (AffineBasis ι k V)

Full source

/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
instance instMulAction : MulAction G (AffineBasis ι k V) :=
  DFunLike.coe_injective.mulAction _ coe_smul

Multiplicative Action on Affine Bases by Group Actions

Informal description

For any group $G$ acting on a vector space $V$ over a ring $k$, the set of affine bases $\text{AffineBasis} \, \iota \, k \, V$ inherits a multiplicative action structure from $G$. This means that for any $a \in G$ and any affine basis $b \in \text{AffineBasis} \, \iota \, k \, V$, the scalar multiple $a \cdot b$ is again an affine basis, where the action is defined pointwise on the basis vectors.

AffineBasis.coord_apply_centroid theorem

 [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i ∈ s) : b.coord i (s.centroid k b) = (s.card : k)⁻¹

Full source

@[simp]
theorem coord_apply_centroid [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι}
    (hi : i ∈ s) : b.coord i (s.centroid k b) = (s.card : k)⁻¹ := by
  rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]

Barycentric Coordinate of Centroid: $\text{coord}_i(\text{centroid}(s)) = \frac{1}{|s|}$ for $i \in s$

Informal description

Let $k$ be a ring of characteristic zero, $P$ an affine space over $k$, and $b$ an affine basis for $P$ indexed by $\iota$. For any finite subset $s \subseteq \iota$ and any index $i \in s$, the $i$-th barycentric coordinate of the centroid of $s$ with respect to $b$ is equal to the reciprocal of the cardinality of $s$, i.e., \[ \text{coord}_i\left(\text{centroid}_k(b, s)\right) = \frac{1}{|s|}. \]

AffineBasis.exists_affine_subbasis theorem

{t : Set P} (ht : affineSpan k t = ⊤) : ∃ s ⊆ t, ∃ b : AffineBasis s k P, ⇑b = ((↑) : s → P)

Full source

theorem exists_affine_subbasis {t : Set P} (ht : affineSpan k t = ⊤) :
    ∃ s ⊆ t, ∃ b : AffineBasis s k P, ⇑b = ((↑) : s → P) := by
  obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t
  refine ⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩
  rw [Subtype.range_coe, h_tot, ht]

Existence of Affine Subbasis Spanning the Entire Space

Informal description

Given a set $t$ of points in an affine space $P$ over a ring $k$ such that the affine span of $t$ is the entire space $P$, there exists a subset $s \subseteq t$ and an affine basis $b$ indexed by $s$ such that the canonical inclusion map from $s$ to $P$ coincides with the map defined by $b$.

AffineBasis.exists_affineBasis theorem

: ∃ (s : Set P) (b : AffineBasis (↥s) k P), ⇑b = ((↑) : s → P)

Full source

theorem exists_affineBasis : ∃ (s : Set P) (b : AffineBasis (↥s) k P), ⇑b = ((↑) : s → P) :=
  let ⟨s, _, hs⟩ := exists_affine_subbasis (AffineSubspace.span_univ k V P)
  ⟨s, hs⟩

Existence of an Affine Basis for an Affine Space

Informal description

There exists a subset $s$ of an affine space $P$ over a ring $k$ and an affine basis $b$ indexed by $s$ such that the canonical inclusion map from $s$ to $P$ coincides with the map defined by $b$.

Mathlib.LinearAlgebra.AffineSpace.Basis

The construction

Main definitions

TODO