basis for linear maps/endomorphisms

Stream: mathlib4

[Johan Commelin]

Do we have a basis for linear maps/endomorphisms? I came up with

-- move to Mathlib.LinearAlgebra.Matrix.ToLin
@[simps! repr_apply repr_symm_apply]
noncomputable
def Basis.end (b : Basis ι R M) : Basis (ι × ι) R (Module.End R M) :=
  (Matrix.stdBasis R ι ι).map (LinearMap.toMatrix b b).symm

-- move to Mathlib.LinearAlgebra.Matrix.ToLin
lemma Basis.end_apply (b : Basis ι R M) (ij : ι × ι) :
    (b.end ij) = (Matrix.toLin b b) (Matrix.stdBasis R ι ι ij) := by
  erw [end_repr_symm_apply, Finsupp.total_single, one_smul]

-- move to Mathlib.LinearAlgebra.Matrix.ToLin
lemma Basis.end_apply_apply (b : Basis ι R M) (ij : ι × ι) (k : ι) :
    (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0 := by
  rcases ij with ⟨i, j⟩
  rw [end_apply, Matrix.stdBasis_eq_stdBasisMatrix, Matrix.toLin_self]
  dsimp only [Matrix.stdBasisMatrix]
  simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]


open Algebra.TensorProduct LinearMap in
lemma Basis.baseChange_end (A : Type*) [CommRing A] [Algebra R A] (b : Basis ι R M) (ij : ι × ι) :
    baseChange A (b.end ij) = (basis A b).end ij := by
  apply (basis A b).ext
  intro k
  conv_lhs => simp only [basis_apply, baseChange_tmul]
  simp_rw [end_apply_apply, basis_apply]
  split <;> simp only [TensorProduct.tmul_zero]

[Eric Wieser]

docs#Basis.dualBasis is all I can find, which I assume is a special case?

[Johan Commelin]

Yes, exactly