AffineBasis.ind
theorem AffineBasis.ind :
∀ {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), AffineIndependent k ⇑b
The theorem `AffineBasis.ind` states that for any affine basis `b` - which is a function from some type `ι` of indices to points in an affine space `P` over a ring `k` with an associated vector space `V` - the indexed family defined by `b` is affinely independent. In other words, there is no nontrivial linear combination of the points of the basis, where the coefficients sum to zero, which gives the zero vector. The condition of affine independence is crucial in many results in affine geometry and linear algebra.
More concisely: Given an affine basis `b : ι → P` from an index type `ι` to an affine space `P` over a ring `k` with associated vector space `V`, the family `{b i | i ∈ ι}` is affinely independent.
|
AffineBasis.linear_combination_coord_eq_self
theorem AffineBasis.linear_combination_coord_eq_self :
∀ {ι : Type u_1} {k : Type u_3} {V : Type u_4} [inst : AddCommGroup V] [inst_1 : Ring k] [inst_2 : Module k V]
[inst_3 : Fintype ι] (b : AffineBasis ι k V) (v : V), (Finset.univ.sum fun i => (b.coord i) v • b i) = v
This theorem, `AffineBasis.linear_combination_coord_eq_self`, is a variation of `AffineBasis.affineCombination_coord_eq_self` and specifically applies to the case where the affine space is a module, allowing us to discuss linear combinations. Given any type `ι`, a ring `k`, an additive commutative group `V` along with a module structure on `V` over `k`, a finite set of type `ι`, an affine basis `b` for a vector space `V`, and a vector `v` in `V`, the theorem states that the sum over all elements of the universal finite set (meaning all elements in the finite set), of the scalar multiplication of the coordinate function of `b` at `i` evaluated at `v` with `b` at `i`, is equal to `v`. In mathematical terms, this can be written as $\sum_{i \in \text{univ}} (b.\text{coord}\ i)(v) \cdot b(i) = v$.
More concisely: Given an affine space `V` as a `k`-module, for any affine basis `b` and vector `v` in `V`, the sum of the scalar multiplication of the coordinate function of `b` at each index `i` by the corresponding basis vector `b(i)` equals `v`. That is, $\sum\_{i \in \text{univ}} (b.\text{coord}\ i)(v) \cdot b(i) = v$.
|