mathlib3 documentation

linear_algebra.affine_space.matrix

Matrix results for barycentric co-ordinates #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Results about the matrix of barycentric co-ordinates for a family of points in an affine space, with respect to some affine basis.

source
noncomputable def affine_basis.to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} (q : ι' → P) :
matrix ι' ι k

Given an affine basis p, and a family of points q : ι' → P, this is the matrix whose rows are the barycentric coordinates of q with respect to p.

It is an affine equivalent of basis.to_matrix.

Equations
source
@[simp]
theorem affine_basis.to_matrix_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} (q : ι' → P) (i : ι') (j : ι) :
b.to_matrix q i j = ⇑(b.coord j) (q i)
source
@[simp]
theorem affine_basis.to_matrix_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [decidable_eq ι] :
b.to_matrix ⇑b = 1
source
theorem affine_basis.to_matrix_row_sum_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] {ι' : Type u_1} (q : ι' → P) (i : ι') :
finset.univ.sum (λ (j : ι), b.to_matrix q i j) = 1
source
theorem affine_basis.affine_independent_of_to_matrix_right_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} [fintype ι'] [fintype ι] [decidable_eq ι'] (p : ι' → P) {A : matrix ι ι' k} (hA : (b.to_matrix p).mul A = 1) :
affine_independent k p

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a right inverse, then p is affine independent.

source
theorem affine_basis.affine_span_eq_top_of_to_matrix_left_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) {ι' : Type u_1} [fintype ι'] [fintype ι] [decidable_eq ι] [nontrivial k] (p : ι' → P) {A : matrix ι ι' k} (hA : A.mul (b.to_matrix p) = 1) :
affine_span k (set.range p) = ⊤

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a left inverse, then p spans the entire space.

source
@[simp]
theorem affine_basis.to_matrix_vec_mul_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) (x : P) :
matrix.vec_mul (⇑(b₂.coords) x) (b.to_matrix ⇑b₂) = ⇑(b.coords) x

A change of basis formula for barycentric coordinates.

See also affine_basis.to_matrix_inv_mul_affine_basis_to_matrix.

source
theorem affine_basis.to_matrix_mul_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) [decidable_eq ι] :
(b.to_matrix ⇑b₂).mul (b₂.to_matrix ⇑b) = 1
source
theorem affine_basis.is_unit_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] (b₂ : affine_basis ι k P) [decidable_eq ι] :
is_unit (b.to_matrix ⇑b₂)
source
theorem affine_basis.is_unit_to_matrix_iff {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [ring k] [module k V] (b : affine_basis ι k P) [fintype ι] [decidable_eq ι] [nontrivial k] (p : ι → P) :
is_unit (b.to_matrix p) ↔ affine_independent k p ∧ affine_span k (set.range p) = ⊤
source
@[simp]
theorem affine_basis.to_matrix_inv_vec_mul_to_matrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [comm_ring k] [module k V] [decidable_eq ι] [fintype ι] (b b₂ : affine_basis ι k P) (x : P) :
matrix.vec_mul (⇑(b.coords) x) (b.to_matrix ⇑b₂)⁻¹ = ⇑(b₂.coords) x

A change of basis formula for barycentric coordinates.

See also affine_basis.to_matrix_vec_mul_coords.

source
theorem affine_basis.det_smul_coords_eq_cramer_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [comm_ring k] [module k V] [decidable_eq ι] [fintype ι] (b b₂ : affine_basis ι k P) (x : P) :
(b.to_matrix ⇑b₂).det • ⇑(b₂.coords) x = ⇑((b.to_matrix ⇑b₂).transpose.cramer) (⇑(b.coords) x)

If we fix a background affine basis b, then for any other basis b₂, we can characterise the barycentric coordinates provided by b₂ in terms of determinants relative to b.