Continues from https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/lie.20algebra/near/516211291

slbasis.lean

import Mathlib

namespace LieAlgebra.SpecialLinear

variable {n R M} [CommRing R] [DecidableEq n] [AddCommGroup M] [Module R M]

theorem ext_linear [Fintype n] ⦃f g : sl n R →ₗ[R] M⦄ (i₀ : n)
    (hf : ∀ i j h, f ∘ₗ single i j h = g ∘ₗ single i j h)
    (hf : ∀ i, f ∘ₗ singleSubSingle i i₀ = g ∘ₗ singleSubSingle i i₀) :
    f = g := by
  ext


#exit

def basisEquiv (i₀ : n) [Fintype n] :
    (({ x : n × n // x.1 ≠ x.2 } → R) × ({y // y ≠ i₀} → R)) ≃ₗ[R] sl n R :=
  .ofLinear
    (LinearMap.coprod
      (∑ i, single _ _ i.prop ∘ₗ .proj i)
      (∑ i, singleSubSingle i.val i₀ ∘ₗ .proj i))
    (LinearMap.prod
      (LinearMap.pi fun ij =>
        (Matrix.entryLinearMap R _ ij.val.1 ij.val.2) ∘ₗ (sl n R).toSubmodule.subtype)
      (LinearMap.pi fun i =>
        (Matrix.entryLinearMap R _ i.val i.val -Matrix.entryLinearMap R _ i₀ i₀)
          ∘ₗ (sl n R).toSubmodule.subtype))
    _
    (by
      rw [← LinearMap.lsum_apply R (fun _ : { x : n × n // x.1 ≠ x.2 } => sl n R) R]
      -- ext <;> dsimp <;> simp
      sorry)



noncomputable def basis (i₀ : n) [Fintype n] :
    Module.Basis ({ x : n × n // x.1 ≠ x.2 } ⊕ {y // y ≠ i₀}) R (sl n R) :=
  .ofEquivFun <| {
    toFun M := (fun ij : { x : n × n // x.1 ≠ x.2 } => M.val ij.1.1 ij.1.2, fun i : {y // y ≠ i₀} => M.val i i - M.val i₀ i₀)
    map_add' _ _ := by ext <;> dsimp; simp [sub_add_sub_comm]
    map_smul' _ _ := by ext <;> dsimp; simp [mul_sub]
    invFun c :=
      ∑ ij, single _ _ ij.prop (c.1 ij) + ∑ i, singleSubSingle i.1 i₀ (c.2 i)
    left_inv M := by
      ext : 1
      dsimp
      simp
      sorry
    right_inv
    | ⟨x, x'⟩ => by
      ext ⟨⟨i, j⟩, hij : i ≠ j⟩
      dsimp
      simp
      sorry
  } ≪≫ₗ (LinearEquiv.sumArrowLequivProdArrow _ _ R R |>.symm)