English
For a type equivalence e : n ≃ m, reindexing rows and columns gives a Lie algebra equivalence between Matrix n n R and Matrix m m R.
Русский
Для эквивалента типа e : n ≃ m перестановка строк и столбцов задаёт тождество Ли‑алгебр между Matrix n n R и Matrix m m R.
LaTeX
$$$\\text{reindexLieEquiv} e: \\mathrm{Matrix}_{n}(R) \\to \\mathrm{Matrix}_{m}(R)$ is a LieEquiv with $\\mathrm{reindexLieEquiv} e\,M = \\mathrm{reindex}\,e\,e\,M$.$$
Lean4
/-- For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent
types, `Matrix.reindex`, is an equivalence of Lie algebras. -/
def reindexLieEquiv : Matrix n n R ≃ₗ⁅R⁆ Matrix m m R :=
{ Matrix.reindexLinearEquiv R R e e with
toFun := Matrix.reindex e e
map_lie' := fun {_ _} => by
simp only [LieRing.of_associative_ring_bracket, Matrix.reindex_apply, Matrix.submatrix_mul_equiv,
Matrix.submatrix_sub, Pi.sub_apply] }
