Skip to content

Commit

Permalink
refactor(linear_algebra/affine_space/*): make affine_basis more ele…
Browse files Browse the repository at this point in the history 
…mentary (#18141)

In the linear algebra development of mathlib, `basis` is more elementary than `finite_dimension`, and matrix results are not imported to the main theory until determinants.  This PR changes the structure of the affine linear algebra development to match that.

I think this is worth doing in any case, but my motivation is to decrease the length of the [current longest chain in mathlib](https://tqft.net/mathlib4/2023-01-12/all) and particularly the length of the chain to `analysis.convex.specific_functions`, which is imported by measure theory.  This actually only reduces those chains in length slightly, since there is a second nearly-as-long path from `data.set.finite` to `analysis.convex.specific_functions` which passes through topology, metric spaces, and normed spaces, rather than through linear algebra, noetherian rings, free modules, and matrix theory.  But that one can be studied later.
  • Loading branch information
@hrmacbeth
hrmacbeth committed Jan 12, 2023
1 parent ec322de commit 579cdfe
Show file tree
Hide file tree
Showing 4 changed files with 221 additions and 176 deletions.
2 changes: 1 addition & 1 deletion src/analysis/normed_space/add_torsor_bases.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Authors: Oliver Nash
import analysis.normed_space.finite_dimension
import analysis.calculus.affine_map
import analysis.convex.combination
import linear_algebra.affine_space.basis
import linear_algebra.affine_space.finite_dimensional

/-!
# Bases in normed affine spaces.
Expand Down
176 changes: 2 additions & 174 deletions src/linear_algebra/affine_space/basis.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import linear_algebra.affine_space.independent
import linear_algebra.affine_space.finite_dimensional
import linear_algebra.determinant
import linear_algebra.basis

/-!
# Affine bases and barycentric coordinates
Expand Down Expand Up @@ -39,7 +38,7 @@ barycentric coordinate of `q : P` is `1 - fᵢ (q -ᵥ p i)`.
-/

open_locale affine big_operators matrix
open_locale affine big_operators
open set

universes u₁ u₂ u₃ u₄
Expand Down Expand Up @@ -223,178 +222,19 @@ noncomputable def coords : P →ᵃ[k] ι → k :=
b.coords q i = b.coord i q :=
rfl

/-- 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`. -/
noncomputable def to_matrix {ι' : Type*} (q : ι' → P) : matrix ι' ι k :=
λ i j, b.coord j (q i)

@[simp] lemma to_matrix_apply {ι' : Type*} (q : ι' → P) (i : ι') (j : ι) :
b.to_matrix q i j = b.coord j (q i) :=
rfl

@[simp] lemma to_matrix_self [decidable_eq ι] :
b.to_matrix b.points = (1 : matrix ι ι k) :=
begin
ext i j,
rw [to_matrix_apply, coord_apply, matrix.one_eq_pi_single, pi.single_apply],
end

variables {ι' : Type*} [fintype ι'] [fintype ι] (b₂ : affine_basis ι k P)

lemma to_matrix_row_sum_one {ι' : Type*} (q : ι' → P) (i : ι') :
∑ j, b.to_matrix q i j = 1 :=
by simp

/-- 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. -/
lemma affine_independent_of_to_matrix_right_inv [decidable_eq ι']
(p : ι' → P) {A : matrix ι ι' k} (hA : (b.to_matrix p) ⬝ A = 1) : affine_independent k p :=
begin
rw affine_independent_iff_eq_of_fintype_affine_combination_eq,
intros w₁ w₂ hw₁ hw₂ hweq,
have hweq' : (b.to_matrix p).vec_mul w₁ = (b.to_matrix p).vec_mul w₂,
{ ext j,
change ∑ i, (w₁ i) • (b.coord j (p i)) = ∑ i, (w₂ i) • (b.coord j (p i)),
rw [← finset.univ.affine_combination_eq_linear_combination _ _ hw₁,
← finset.univ.affine_combination_eq_linear_combination _ _ hw₂,
← finset.univ.map_affine_combination p w₁ hw₁,
← finset.univ.map_affine_combination p w₂ hw₂, hweq], },
replace hweq' := congr_arg (λ w, A.vec_mul w) hweq',
simpa only [matrix.vec_mul_vec_mul, ← matrix.mul_eq_mul, hA, matrix.vec_mul_one] using hweq',
end

/-- 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. -/
lemma affine_span_eq_top_of_to_matrix_left_inv [decidable_eq ι] [nontrivial k]
(p : ι' → P) {A : matrix ι ι' k} (hA : A ⬝ b.to_matrix p = 1) : affine_span k (range p) = ⊤ :=
begin
suffices : ∀ i, b.points i ∈ affine_span k (range p),
{ rw [eq_top_iff, ← b.tot, affine_span_le],
rintros q ⟨i, rfl⟩,
exact this i, },
intros i,
have hAi : ∑ j, A i j = 1,
{ calc ∑ j, A i j = ∑ j, (A i j) * ∑ l, b.to_matrix p j l : by simp
... = ∑ j, ∑ l, (A i j) * b.to_matrix p j l : by simp_rw finset.mul_sum
... = ∑ l, ∑ j, (A i j) * b.to_matrix p j l : by rw finset.sum_comm
... = ∑ l, (A ⬝ b.to_matrix p) i l : rfl
... = 1 : by simp [hA, matrix.one_apply, finset.filter_eq], },
have hbi : b.points i = finset.univ.affine_combination p (A i),
{ apply b.ext_elem,
intros j,
rw [b.coord_apply, finset.univ.map_affine_combination _ _ hAi,
finset.univ.affine_combination_eq_linear_combination _ _ hAi],
change _ = (A ⬝ b.to_matrix p) i j,
simp_rw [hA, matrix.one_apply, @eq_comm _ i j] },
rw hbi,
exact affine_combination_mem_affine_span hAi p,
end

/-- A change of basis formula for barycentric coordinates.
See also `affine_basis.to_matrix_inv_mul_affine_basis_to_matrix`. -/
@[simp] lemma to_matrix_vec_mul_coords (x : P) :
(b.to_matrix b₂.points).vec_mul (b₂.coords x) = b.coords x :=
begin
ext j,
change _ = b.coord j x,
conv_rhs { rw ← b₂.affine_combination_coord_eq_self x, },
rw finset.map_affine_combination _ _ _ (b₂.sum_coord_apply_eq_one x),
simp [matrix.vec_mul, matrix.dot_product, to_matrix_apply, coords],
end

variables [decidable_eq ι]

lemma to_matrix_mul_to_matrix :
(b.to_matrix b₂.points) ⬝ (b₂.to_matrix b.points) = 1 :=
begin
ext l m,
change (b₂.to_matrix b.points).vec_mul (b.coords (b₂.points l)) m = _,
rw [to_matrix_vec_mul_coords, coords_apply, ← to_matrix_apply, to_matrix_self],
end

lemma is_unit_to_matrix :
is_unit (b.to_matrix b₂.points) :=
⟨{ val := b.to_matrix b₂.points,
inv := b₂.to_matrix b.points,
val_inv := b.to_matrix_mul_to_matrix b₂,
inv_val := b₂.to_matrix_mul_to_matrix b, }, rfl⟩

lemma is_unit_to_matrix_iff [nontrivial k] (p : ι → P) :
is_unit (b.to_matrix p) ↔ affine_independent k p ∧ affine_span k (range p) = ⊤ :=
begin
split,
{ rintros ⟨⟨B, A, hA, hA'⟩, (rfl : B = b.to_matrix p)⟩,
rw matrix.mul_eq_mul at hA hA',
exact ⟨b.affine_independent_of_to_matrix_right_inv p hA,
b.affine_span_eq_top_of_to_matrix_left_inv p hA'⟩, },
{ rintros ⟨h_tot, h_ind⟩,
let b' : affine_basis ι k P := ⟨p, h_tot, h_ind⟩,
change is_unit (b.to_matrix b'.points),
exact b.is_unit_to_matrix b', },
end

end ring

section comm_ring

variables [comm_ring k] [module k V] [decidable_eq ι] [fintype ι]
variables (b b₂ : affine_basis ι k P)

/-- A change of basis formula for barycentric coordinates.
See also `affine_basis.to_matrix_vec_mul_coords`. -/
@[simp] lemma to_matrix_inv_vec_mul_to_matrix (x : P) :
(b.to_matrix b₂.points)⁻¹.vec_mul (b.coords x) = b₂.coords x :=
begin
have hu := b.is_unit_to_matrix b₂,
rw matrix.is_unit_iff_is_unit_det at hu,
rw [← b.to_matrix_vec_mul_coords b₂, matrix.vec_mul_vec_mul, matrix.mul_nonsing_inv _ hu,
matrix.vec_mul_one],
end

/-- 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`. -/
lemma det_smul_coords_eq_cramer_coords (x : P) :
(b.to_matrix b₂.points).det • b₂.coords x = (b.to_matrix b₂.points)ᵀ.cramer (b.coords x) :=
begin
have hu := b.is_unit_to_matrix b₂,
rw matrix.is_unit_iff_is_unit_det at hu,
rw [← b.to_matrix_inv_vec_mul_to_matrix, matrix.det_smul_inv_vec_mul_eq_cramer_transpose _ _ hu],
end

end comm_ring

section division_ring

variables [division_ring k] [module k V]
include V

protected lemma finite_dimensional [finite ι] (b : affine_basis ι k P) : finite_dimensional k V :=
let ⟨i⟩ := b.nonempty in finite_dimensional.of_fintype_basis (b.basis_of i)

protected lemma finite [finite_dimensional k V] (b : affine_basis ι k P) : finite ι :=
finite_of_fin_dim_affine_independent k b.ind

protected lemma finite_set [finite_dimensional k V] {s : set ι} (b : affine_basis s k P) :
s.finite :=
finite_set_of_fin_dim_affine_independent k b.ind

@[simp] lemma coord_apply_centroid [char_zero k] (b : affine_basis ι k P) {s : finset ι} {i : ι}
(hi : i ∈ s) :
b.coord i (s.centroid k b.points) = (s.card : k) ⁻¹ :=
by rw [finset.centroid, b.coord_apply_combination_of_mem hi
(s.sum_centroid_weights_eq_one_of_nonempty _ ⟨i, hi⟩), finset.centroid_weights]

lemma card_eq_finrank_add_one [fintype ι] (b : affine_basis ι k P) :
fintype.card ι = finite_dimensional.finrank k V + 1 :=
begin
haveI := b.finite_dimensional,
exact b.ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mp b.tot
end

lemma exists_affine_subbasis {t : set P} (ht : affine_span k t = ⊤) :
∃ (s ⊆ t) (b : affine_basis ↥s k P), b.points = coe :=
begin
Expand All @@ -408,18 +248,6 @@ variables (k V P)
lemma exists_affine_basis : ∃ (s : set P) (b : affine_basis ↥s k P), b.points = coe :=
let ⟨s, _, hs⟩ := exists_affine_subbasis (affine_subspace.span_univ k V P) in ⟨s, hs⟩

variables {k V P}

lemma exists_affine_basis_of_finite_dimensional [fintype ι] [finite_dimensional k V]
(h : fintype.card ι = finite_dimensional.finrank k V + 1) :
nonempty (affine_basis ι k P) :=
begin
obtain ⟨s, b, hb⟩ := affine_basis.exists_affine_basis k V P,
lift s to finset P using b.finite_set,
refine ⟨b.comp_equiv $ fintype.equiv_of_card_eq _⟩,
rw [h, ← b.card_eq_finrank_add_one]
end

end division_ring

end affine_basis
47 changes: 46 additions & 1 deletion src/linear_algebra/affine_space/finite_dimensional.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers
-/
import linear_algebra.affine_space.independent
import linear_algebra.affine_space.basis
import linear_algebra.finite_dimensional

/-!
Expand Down Expand Up @@ -727,3 +727,48 @@ lemma coplanar_triple (p₁ p₂ p₃ : P) : coplanar k ({p₁, p₂, p₃} : se
(collinear_pair k p₂ p₃).coplanar_insert p₁

end division_ring

namespace affine_basis

universes u₁ u₂ u₃ u₄

variables {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄}
variables [add_comm_group V] [affine_space V P]

section division_ring

variables [division_ring k] [module k V]
include V

protected lemma finite_dimensional [finite ι] (b : affine_basis ι k P) : finite_dimensional k V :=
let ⟨i⟩ := b.nonempty in finite_dimensional.of_fintype_basis (b.basis_of i)

protected lemma finite [finite_dimensional k V] (b : affine_basis ι k P) : finite ι :=
finite_of_fin_dim_affine_independent k b.ind

protected lemma finite_set [finite_dimensional k V] {s : set ι} (b : affine_basis s k P) :
s.finite :=
finite_set_of_fin_dim_affine_independent k b.ind

lemma card_eq_finrank_add_one [fintype ι] (b : affine_basis ι k P) :
fintype.card ι = finite_dimensional.finrank k V + 1 :=
begin
haveI := b.finite_dimensional,
exact b.ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mp b.tot
end

variables {k V P}

lemma exists_affine_basis_of_finite_dimensional [fintype ι] [finite_dimensional k V]
(h : fintype.card ι = finite_dimensional.finrank k V + 1) :
nonempty (affine_basis ι k P) :=
begin
obtain ⟨s, b, hb⟩ := affine_basis.exists_affine_basis k V P,
lift s to finset P using b.finite_set,
refine ⟨b.comp_equiv $ fintype.equiv_of_card_eq _⟩,
rw [h, ← b.card_eq_finrank_add_one]
end

end division_ring

end affine_basis
Loading

0 comments on commit 579cdfe

Please sign in to comment.