feat: port LinearAlgebra.Matrix.Basis (#3691)

Co-authored-by: Parcly Taxel <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Komyyy <[email protected]> Co-authored-by: Johan Commelin <[email protected]>
leanprover-community · Apr 28, 2023 · 88894f5 · 88894f5
1 parent fabd023
commit 88894f5
Show file tree

Hide file tree

Showing 3 changed files with 306 additions and 21 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1421,6 +1421,7 @@ import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.LinearAlgebra.LinearPMap
 import Mathlib.LinearAlgebra.Matrix.AbsoluteValue
 import Mathlib.LinearAlgebra.Matrix.Adjugate
+import Mathlib.LinearAlgebra.Matrix.Basis
 import Mathlib.LinearAlgebra.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Circulant
 import Mathlib.LinearAlgebra.Matrix.Determinant

diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
@@ -1245,47 +1245,47 @@ theorem units_smul_span_eq_top {v : ι → M} (hv : Submodule.span R (Set.range
 
 /-- Given a basis `v` and a map `w` such that for all `i`, `w i` is a unit, `smul_of_is_unit`
 provides the basis corresponding to `w • v`. -/
-def unitsSmul (v : Basis ι R M) (w : ι → Rˣ) : Basis ι R M :=
+def unitsSMul (v : Basis ι R M) (w : ι → Rˣ) : Basis ι R M :=
   Basis.mk (LinearIndependent.units_smul v.linearIndependent w)
     (units_smul_span_eq_top v.span_eq).ge
-#align basis.units_smul Basis.unitsSmul
+#align basis.units_smul Basis.unitsSMul
 
-theorem unitsSmul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSmul v w i = w i • v i :=
+theorem unitsSMul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSMul v w i = w i • v i :=
   mk_apply (LinearIndependent.units_smul v.linearIndependent w)
     (units_smul_span_eq_top v.span_eq).ge i
-#align basis.units_smul_apply Basis.unitsSmul_apply
+#align basis.units_smul_apply Basis.unitsSMul_apply
 
 set_option synthInstance.etaExperiment true in
 @[simp]
-theorem coord_unitsSmul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
-    (unitsSmul e w).coord i = (w i)⁻¹ • e.coord i := by
+theorem coord_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
+    (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i := by
   classical
     apply e.ext
     intro j
-    trans ((unitsSmul e w).coord i) ((w j)⁻¹ • (unitsSmul e w) j)
+    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
     · congr
-      simp [Basis.unitsSmul, ← mul_smul]
+      simp [Basis.unitsSMul, ← mul_smul]
     simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
       SMulHomClass.map_smul, Finsupp.single_apply]
     split_ifs with h <;> simp [h]
-#align basis.coord_units_smul Basis.coord_unitsSmul
+#align basis.coord_units_smul Basis.coord_unitsSMul
 
 set_option synthInstance.etaExperiment true in
 @[simp]
-theorem repr_unitsSmul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
-    (e.unitsSmul w).repr v i = (w i)⁻¹ • e.repr v i :=
-  congr_arg (fun f : M →ₗ[R₂] R₂ => f v) (e.coord_unitsSmul w i)
-#align basis.repr_units_smul Basis.repr_unitsSmul
+theorem repr_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
+    (e.unitsSMul w).repr v i = (w i)⁻¹ • e.repr v i :=
+  congr_arg (fun f : M →ₗ[R₂] R₂ => f v) (e.coord_unitsSMul w i)
+#align basis.repr_units_smul Basis.repr_unitsSMul
 
 /-- A version of `smul_of_units` that uses `IsUnit`. -/
-def isUnitSmul (v : Basis ι R M) {w : ι → R} (hw : ∀ i, IsUnit (w i)) : Basis ι R M :=
-  unitsSmul v fun i => (hw i).unit
-#align basis.is_unit_smul Basis.isUnitSmul
-
-theorem isUnitSmul_apply {v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit (w i)) (i : ι) :
-    v.isUnitSmul hw i = w i • v i :=
-  unitsSmul_apply i
-#align basis.is_unit_smul_apply Basis.isUnitSmul_apply
+def isUnitSMul (v : Basis ι R M) {w : ι → R} (hw : ∀ i, IsUnit (w i)) : Basis ι R M :=
+  unitsSMul v fun i => (hw i).unit
+#align basis.is_unit_smul Basis.isUnitSMul
+
+theorem isUnitSMul_apply {v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit (w i)) (i : ι) :
+    v.isUnitSMul hw i = w i • v i :=
+  unitsSMul_apply i
+#align basis.is_unit_smul_apply Basis.isUnitSMul_apply
 
 section Fin
 

diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean
@@ -0,0 +1,284 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
+
+! This file was ported from Lean 3 source module linear_algebra.matrix.basis
+! leanprover-community/mathlib commit 6c263e4bfc2e6714de30f22178b4d0ca4d149a76
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.LinearAlgebra.Matrix.Reindex
+import Mathlib.LinearAlgebra.Matrix.ToLin
+
+/-!
+# Bases and matrices
+
+This file defines the map `Basis.toMatrix` that sends a family of vectors to
+the matrix of their coordinates with respect to some basis.
+
+## Main definitions
+
+ * `Basis.toMatrix e v` is the matrix whose `i, j`th entry is `e.repr (v j) i`
+ * `basis.toMatrixEquiv` is `Basis.toMatrix` bundled as a linear equiv
+
+## Main results
+
+ * `LinearMap.toMatrix_id_eq_basis_toMatrix`: `LinearMap.toMatrix b c id`
+   is equal to `Basis.toMatrix b c`
+ * `Basis.toMatrix_mul_toMatrix`: multiplying `Basis.toMatrix` with another
+   `Basis.toMatrix` gives a `Basis.toMatrix`
+
+## Tags
+
+matrix, basis
+-/
+
+
+noncomputable section
+
+open LinearMap Matrix Set Submodule
+
+open BigOperators
+
+open Matrix
+
+section BasisToMatrix
+
+variable {ι ι' κ κ' : Type _}
+
+variable {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+variable {R₂ M₂ : Type _} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂]
+
+open Function Matrix
+
+/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
+are the vectors `v i` written in the basis `e`. -/
+def Basis.toMatrix (e : Basis ι R M) (v : ι' → M) : Matrix ι ι' R := fun i j => e.repr (v j) i
+#align basis.to_matrix Basis.toMatrix
+
+variable (e : Basis ι R M) (v : ι' → M) (i : ι) (j : ι')
+
+namespace Basis
+
+theorem toMatrix_apply : e.toMatrix v i j = e.repr (v j) i :=
+  rfl
+#align basis.to_matrix_apply Basis.toMatrix_apply
+
+theorem toMatrix_transpose_apply : (e.toMatrix v)ᵀ j = e.repr (v j) :=
+  funext fun _ => rfl
+#align basis.to_matrix_transpose_apply Basis.toMatrix_transpose_apply
+
+theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) :
+    e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v) := by
+  ext
+  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
+#align basis.to_matrix_eq_to_matrix_constr Basis.toMatrix_eq_toMatrix_constr
+
+-- TODO (maybe) Adjust the definition of `Basis.toMatrix` to eliminate the transpose.
+theorem coePiBasisFun.toMatrix_eq_transpose [Fintype ι] :
+    ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose := by
+  ext (M i j)
+  rfl
+#align basis.coe_pi_basis_fun.to_matrix_eq_transpose Basis.coePiBasisFun.toMatrix_eq_transpose
+
+@[simp]
+theorem toMatrix_self [DecidableEq ι] : e.toMatrix e = 1 := by
+  unfold Basis.toMatrix
+  ext (i j)
+  simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm]
+#align basis.to_matrix_self Basis.toMatrix_self
+
+theorem toMatrix_update [DecidableEq ι'] (x : M) :
+    e.toMatrix (Function.update v j x) = Matrix.updateColumn (e.toMatrix v) j (e.repr x) := by
+  ext (i' k)
+  rw [Basis.toMatrix, Matrix.updateColumn_apply, e.toMatrix_apply]
+  split_ifs with h
+  · rw [h, update_same j x v]
+  · rw [update_noteq h]
+#align basis.to_matrix_update Basis.toMatrix_update
+
+/-- The basis constructed by `unitsSMul` has vectors given by a diagonal matrix. -/
+@[simp]
+theorem toMatrix_unitsSMul [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) :
+    e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w) := by
+  ext (i j)
+  by_cases h : i = j
+  · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]
+  · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h]
+#align basis.to_matrix_units_smul Basis.toMatrix_unitsSMul
+
+/-- The basis constructed by `isUnitSMul` has vectors given by a diagonal matrix. -/
+@[simp]
+theorem toMatrix_isUnitSMul [DecidableEq ι] (e : Basis ι R₂ M₂) {w : ι → R₂}
+    (hw : ∀ i, IsUnit (w i)) : e.toMatrix (e.isUnitSMul hw) = diagonal w :=
+  e.toMatrix_unitsSMul _
+#align basis.to_matrix_is_unit_smul Basis.toMatrix_isUnitSMul
+
+@[simp]
+theorem sum_toMatrix_smul_self [Fintype ι] : (∑ i : ι, e.toMatrix v i j • e i) = v j := by
+  simp_rw [e.toMatrix_apply, e.sum_repr]
+#align basis.sum_to_matrix_smul_self Basis.sum_toMatrix_smul_self
+
+set_option synthInstance.etaExperiment true in
+theorem toMatrix_map_vecMul {S : Type _} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S)
+    (v : ι' → S) : ((b.toMatrix v).map <| algebraMap R S).vecMul b = v := by
+  ext i
+  simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
+    sum_toMatrix_smul_self]
+#align basis.to_matrix_map_vec_mul Basis.toMatrix_map_vecMul
+
+@[simp]
+theorem toLin_toMatrix [Fintype ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
+    Matrix.toLin v e (e.toMatrix v) = LinearMap.id :=
+  v.ext fun i => by rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]
+#align basis.to_lin_to_matrix Basis.toLin_toMatrix
+
+/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
+and matrices, making the matrix whose columns are the vectors `v i` written in the basis `e`. -/
+def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix ι ι R where
+  toFun := e.toMatrix
+  map_add' v w := by
+    ext (i j)
+    change _ = _ + _
+    rw [e.toMatrix_apply, Pi.add_apply, LinearEquiv.map_add]
+    rfl
+  map_smul' := by
+    intro c v
+    ext (i j)
+    dsimp only []
+    rw [e.toMatrix_apply, Pi.smul_apply, LinearEquiv.map_smul]
+    rfl
+  invFun m j := ∑ i, m i j • e i
+  left_inv := by
+    intro v
+    ext j
+    exact e.sum_toMatrix_smul_self v j
+  right_inv := by
+    intro m
+    ext (k l)
+    simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply,
+      LinearEquiv.apply_symm_apply]
+#align basis.to_matrix_equiv Basis.toMatrixEquiv
+
+end Basis
+
+section MulLinearMapToMatrix
+
+variable {N : Type _} [AddCommMonoid N] [Module R N]
+
+variable (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N)
+
+variable (f : M →ₗ[R] N)
+
+open LinearMap
+
+section Fintype
+
+variable [Fintype ι'] [Fintype κ] [Fintype κ']
+
+@[simp]
+theorem basis_toMatrix_mul_linearMap_toMatrix [DecidableEq ι'] :
+    c.toMatrix c' ⬝ LinearMap.toMatrix b' c' f = LinearMap.toMatrix b' c f :=
+  (Matrix.toLin b' c).injective
+    (by
+      haveI := Classical.decEq κ'
+      rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, id_comp])
+#align basis_to_matrix_mul_linear_map_to_matrix basis_toMatrix_mul_linearMap_toMatrix
+
+variable [Fintype ι]
+
+@[simp]
+theorem linearMap_toMatrix_mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] :
+    LinearMap.toMatrix b' c' f ⬝ b'.toMatrix b = LinearMap.toMatrix b c' f :=
+  (Matrix.toLin b c').injective
+    (by rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, comp_id])
+#align linear_map_to_matrix_mul_basis_to_matrix linearMap_toMatrix_mul_basis_toMatrix
+
+theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] :
+    c.toMatrix c' ⬝ LinearMap.toMatrix b' c' f ⬝ b'.toMatrix b = LinearMap.toMatrix b c f := by
+  rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]
+#align basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix
+
+theorem basis_toMatrix_mul [DecidableEq κ] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N)
+    (A : Matrix ι' κ R) : b₁.toMatrix b₂ ⬝ A = LinearMap.toMatrix b₃ b₁ (toLin b₃ b₂ A) := by
+  have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
+  rwa [LinearMap.toMatrix_toLin] at this
+#align basis_to_matrix_mul basis_toMatrix_mul
+
+theorem mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M)
+    (b₃ : Basis κ R N) (A : Matrix κ ι R) :
+    A ⬝ b₁.toMatrix b₂ = LinearMap.toMatrix b₂ b₃ (toLin b₁ b₃ A) := by
+  have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
+  rwa [LinearMap.toMatrix_toLin] at this
+#align mul_basis_to_matrix mul_basis_toMatrix
+
+theorem basis_toMatrix_basisFun_mul (b : Basis ι R (ι → R)) (A : Matrix ι ι R) :
+    b.toMatrix (Pi.basisFun R ι) ⬝ A = of fun i j => b.repr (Aᵀ j) i := by
+  classical
+    simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
+    ext (i j)
+    rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
+      Matrix.mulVec_stdBasis_apply, Matrix.of_apply]
+#align basis_to_matrix_basis_fun_mul basis_toMatrix_basisFun_mul
+
+/-- A generalization of `LinearMap.toMatrix_id`. -/
+@[simp]
+theorem LinearMap.toMatrix_id_eq_basis_toMatrix [DecidableEq ι] :
+    LinearMap.toMatrix b b' id = b'.toMatrix b := by
+  haveI := Classical.decEq ι'
+  rw [← @basis_toMatrix_mul_linearMap_toMatrix _ _ ι, toMatrix_id, Matrix.mul_one]
+#align linear_map.to_matrix_id_eq_basis_to_matrix LinearMap.toMatrix_id_eq_basis_toMatrix
+
+/-- See also `Basis.toMatrix_reindex` which gives the `simp` normal form of this result. -/
+theorem Basis.toMatrix_reindex' [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M)
+    (e : ι ≃ ι') : (b.reindex e).toMatrix v = Matrix.reindexAlgEquiv _ e (b.toMatrix (v ∘ e)) := by
+  ext
+  simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply,
+    Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
+    Finsupp.mapDomain_equiv_apply]
+#align basis.to_matrix_reindex' Basis.toMatrix_reindex'
+
+end Fintype
+
+/-- A generalization of `Basis.toMatrix_self`, in the opposite direction. -/
+@[simp]
+theorem Basis.toMatrix_mul_toMatrix {ι'' : Type _} [Fintype ι'] (b'' : ι'' → M) :
+    b.toMatrix b' ⬝ b'.toMatrix b'' = b.toMatrix b'' := by
+  haveI := Classical.decEq ι
+  haveI := Classical.decEq ι'
+  haveI := Classical.decEq ι''
+  ext (i j)
+  simp only [Matrix.mul_apply, Basis.toMatrix_apply, Basis.sum_repr_mul_repr]
+#align basis.to_matrix_mul_to_matrix Basis.toMatrix_mul_toMatrix
+
+/-- `b.toMatrix b'` and `b'.toMatrix b` are inverses. -/
+theorem Basis.toMatrix_mul_toMatrix_flip [DecidableEq ι] [Fintype ι'] :
+    b.toMatrix b' ⬝ b'.toMatrix b = 1 := by rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
+#align basis.to_matrix_mul_to_matrix_flip Basis.toMatrix_mul_toMatrix_flip
+
+/-- A matrix whose columns form a basis `b'`, expressed w.r.t. a basis `b`, is invertible. -/
+def Basis.invertibleToMatrix [DecidableEq ι] [Fintype ι] (b b' : Basis ι R₂ M₂) :
+    Invertible (b.toMatrix b') :=
+  ⟨b'.toMatrix b, Basis.toMatrix_mul_toMatrix_flip _ _, Basis.toMatrix_mul_toMatrix_flip _ _⟩
+#align basis.invertible_to_matrix Basis.invertibleToMatrix
+
+@[simp]
+theorem Basis.toMatrix_reindex (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
+    (b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id := by
+  ext
+  simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.submatrix_apply, id.def,
+    Finsupp.mapDomain_equiv_apply]
+#align basis.to_matrix_reindex Basis.toMatrix_reindex
+
+@[simp]
+theorem Basis.toMatrix_map (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) :
+    (b.map f).toMatrix v = b.toMatrix (f.symm ∘ v) := by
+  ext
+  simp only [Basis.toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]
+#align basis.to_matrix_map Basis.toMatrix_map
+
+end MulLinearMapToMatrix
+
+end BasisToMatrix