English
For a basis b and another basis b2, the product of their matrices equals the identity on the left.
Русский
Для базиса b и другого базиса b2 произведение их матриц слева равно тождественной матрице.
LaTeX
$$$b.toMatrix b_2 \\cdot b_2.toMatrix b = 1.$$$
Lean4
/-- 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. -/
theorem affineSpan_eq_top_of_toMatrix_left_inv [Finite ι] [Fintype ι'] [DecidableEq ι] [Nontrivial k] (p : ι' → P)
{A : Matrix ι ι' k} (hA : A * b.toMatrix p = 1) : affineSpan k (range p) = ⊤ :=
by
cases nonempty_fintype ι
suffices ∀ i, b i ∈ affineSpan k (range p)
by
rw [eq_top_iff, ← b.tot, affineSpan_le]
rintro q ⟨i, rfl⟩
exact this i
intro i
have hAi : ∑ j, A i j = 1 := by
calc
∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
_ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
_ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
_ = ∑ l, (A * b.toMatrix p) i l := rfl
_ = 1 := by simp [hA, Matrix.one_apply]
have hbi : b i = Finset.univ.affineCombination k p (A i) :=
by
apply b.ext_elem
intro j
rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
change _ = (A * b.toMatrix p) i j
simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
rw [hbi]
exact affineCombination_mem_affineSpan hAi p
