beginner project: linear algebra lemma

Stream: new members

[Paul Nelson]

I formalized a result from one of my papers: https://github.com/ultronozm/LinearAlgebraLemma. It's a "linear algebra lemma" that shows up at the end of a longer analytic argument. This is my first attempt at doing anything with Lean, so any feedback or criticism would be welcome. Some of the intermediary results might be useful in Mathlib in some form, but I suspect my proofs are clumsy, and I'm not very familiar with Mathlib, so any suggestions there would also be welcome.

Here's the mathematical statement:

Let $M_{n}$ denote the space of complex n × n matrices, included in the space $M_{n+1}$ of (n+1) × (n+1) matrices as the upper-left block. Let τ be an element of $M_{n+1}$ with the property that no eigenvalue of τ is also an eigenvalue of the upper-left n × n submatrix of τ. Let x be an element of $M_{n+1}$ with [x,τ] = 0. Let z denote the image in $M_{n+1}$ of the identity element of $M_{n}$, thus z is a diagonal matrix with entries (1, ..., 1, 0). Suppose that [x,[z,τ]] = [y, τ] for some y in $M_{n}$. Then x is a scalar matrix.

Here's the Lean statement:

import Mathlib

abbrev Mat (R : Type) [Ring R] (n : ℕ) := Matrix (Fin n) (Fin n) R

def matrixIncl {R : Type} [Ring R] {n : ℕ}
  (x : Mat R n) : Mat R (n+1) :=
  fun i j ↦ if h : i  ≠ Fin.last n ∧ j ≠ Fin.last n
    then x ⟨i, Fin.val_lt_last h.1⟩ ⟨j, Fin.val_lt_last h.2⟩
    else 0

example (n : ℕ)
  (τ : Mat ℂ (n+1)) (hτ : τ.charpoly.roots ⊓ (Matrix.subUpLeft τ).charpoly.roots = ⊥)
  (x : Mat ℂ (n+1)) (hx : ⁅x, τ⁆ = 0) (y : Mat ℂ n)
  (h : ⁅x, ⁅matrixIncl (1 : Mat ℂ n), τ⁆⁆ = ⁅matrixIncl y, τ⁆)
  : ∃ (r : ℂ), x = r • (1 : Mat ℂ (n+1)) := by sorry

[Ruben Van de Velde]

Congratulations!