AffineBasis.det_smul_coords_eq_cramer_coords
theorem AffineBasis.det_smul_coords_eq_cramer_coords :
∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : CommRing k] [inst_3 : Module k V] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
(b b₂ : AffineBasis ι k P) (x : P),
(b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂).transpose.cramer (b.coords x)
This theorem, named `AffineBasis.det_smul_coords_eq_cramer_coords`, states that given a fixed affine basis `b`, for any other basis `b₂`, the barycentric coordinates provided by `b₂` can be characterized in terms of determinants relative to `b`. In more precise terms, for all types `ι`, `k`, `V`, `P`, where `V` is an additive commutative group, `P` is an additive torsor over `V`, `k` is a commutative ring, and `V` is a `k`-module, and under the conditions that equality in `ι` is decidable and `ι` is finite, for any two affine bases `b` and `b₂` of type `AffineBasis ι k P` and any point `x` of type `P`, the determinant of the matrix representation of basis `b` with respect to `b₂`, scaled by the coordinates of `x` in `b₂`, is equal to the result of applying the Cramer's rule to the coordinates of `x` in `b` using the transpose of the matrix representation of `b` with respect to `b₂`.
More concisely: For any affine bases `b` and `b₂` and point `x` in a finite-dimensional vector space over a commutative ring, the determinant of the matrix representing `b` with respect to `b₂`, multiplied by the coordinates of `x` in `b₂`, is equal to the product of the coordinates of `x` in `b` and the determinant of the transpose of the matrix representing `b` with respect to `b₂`.
|
AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv
theorem AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv :
∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [inst_4 : Finite ι]
[inst_5 : Fintype ι'] [inst_6 : DecidableEq ι] [inst_7 : Nontrivial k] (p : ι' → P) {A : Matrix ι ι' k},
A * b.toMatrix p = 1 → affineSpan k (Set.range p) = ⊤
The theorem `AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv` states that given an affine basis `b` and a family of points `p` mapping from the type `ι'` to `P`, if the matrix `A` whose rows are the coordinates of `p` with respect to `b` has a left inverse (i.e., `A * b.toMatrix p = 1`), then the set of points `p` spans the entire space. Here, the type `ι'` has a finite type and a decidable equality. The matrix `A` is defined in a field `k`, which is nontrivial and forms a ring structure, where `V` is an additive commutative group and `P` is an additive torsor over `V`.
More concisely: Given an affine basis `b` and a family of points `p : ι' -> P` such that the matrix `A` of coordinates of `p` with respect to `b` has a left inverse `1 = A * b.toMatrix p`, then the points `p` span the entire affine space.
|
AffineBasis.toMatrix_vecMul_coords
theorem AffineBasis.toMatrix_vecMul_coords :
∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (b₂ : AffineBasis ι k P)
(x : P), Matrix.vecMul (b₂.coords x) (b.toMatrix ⇑b₂) = b.coords x
This theorem specifies a change of basis formula for barycentric coordinates. In the context of affine spaces, given two affine bases `b` and `b₂` of the same finite type `ι` over a field `k`, for any point `x` in the affine space, the vector of barycentric coordinates of `x` with respect to `b₂`, when multiplied by the change of basis matrix from `b` to `b₂`, equals the barycentric coordinates of `x` with respect to `b`. This theorem thus links the change of basis process with the computation of barycentric coordinates in different bases.
More concisely: Given affine bases `b` and `b₂` of the same type over a field `k`, and any point `x` in the affine space, the matrix of barycentric coordinates of `x` with respect to `b₂` times the change of basis matrix from `b` to `b₂` equals the matrix of barycentric coordinates of `x` with respect to `b`.
|
AffineBasis.toMatrix_inv_vecMul_toMatrix
theorem AffineBasis.toMatrix_inv_vecMul_toMatrix :
∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : CommRing k] [inst_3 : Module k V] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
(b b₂ : AffineBasis ι k P) (x : P), Matrix.vecMul (b.coords x) (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
This theorem, `AffineBasis.toMatrix_inv_vecMul_toMatrix`, provides a change of basis formula for barycentric coordinates. For any types ι, k, V, and P, given an addition commutative group structure on V, an add-torsor structure on P with respect to V, a commutative ring structure on k, a module structure of k on V, a decision procedure for equality on ι, and a finite type structure on ι, and for any two affine bases `b` and `b₂` for the affine space P over the field k indexed by ι, and for any point `x` in P, the barycentric coordinates of `x` with respect to `b₂` can be computed by multiplying the vector of barycentric coordinates of `x` with respect to `b` by the inverse of the matrix representing `b` with respect to `b₂`.
More concisely: Given affine bases `b` and `b₂` for an affine space P over a field k, the barycentric coordinates of a point `x` in P with respect to `b₂` are equal to the product of the barycentric coordinates of `x` with respect to `b` and the inverse of the matrix representing the change of basis from `b` to `b₂`.
|
AffineBasis.affineIndependent_of_toMatrix_right_inv
theorem AffineBasis.affineIndependent_of_toMatrix_right_inv :
∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [inst_4 : Fintype ι]
[inst_5 : Finite ι'] [inst_6 : DecidableEq ι'] (p : ι' → P) {A : Matrix ι ι' k},
b.toMatrix p * A = 1 → AffineIndependent k p
This theorem states that, given a set of points `p` and an affine basis `b`, if the matrix whose rows are the coordinates of `p` with respect to `b` has a right inverse (i.e., the multiplication of the matrix with its right inverse equals the identity matrix), then the set of points `p` is affinely independent. In mathematical terms, affinely independent points imply that no point in the set can be expressed as a linear combination of the other points. This theorem is applicable under the conditions that the vector space `V` forms an additive commutative group, `P` is an affine torsor over `V`, and `k` is a ring that is also a module over `V`. The indices `ι` and `ι'` must be finite and have decidable equality.
More concisely: If the matrix of coordinates of a finite set of points with respect to an affine basis has a right inverse, then the points are affinely independent.
|