Scalar extension of matrix Lie algebras

The associative matrix-algebra base-change equivalence also identifies Mathlib's scalar extension of the matrix Lie algebra with the matrix Lie algebra over the target ring. The explicit Lie equivalence is needed because the scalar-extension bracket and the associative commutator bracket are propositionally equal but come from different, non-definitionally-equal LieRing instances.

Main definitions

• TauCeti.matrixBaseChangeLieEquiv: the Lie equivalence A ⊗[R] Matrix n n R ≃ Matrix n n A.

noncomputable def TauCeti.matrixBaseChangeLieEquiv (n : Type u_1) (R : Type u_2) (A : Type u_3) [Fintype n] [DecidableEq n] [CommRing R] [CommRing A] [Algebra R A] : TensorProduct R A (Matrix n n R) ≃ₗ⁅A⁆ Matrix n n A

Scalar extension commutes with forming a matrix Lie algebra. The underlying linear equivalence is TauCeti.Algebra.matrixBaseChangeAlgEquiv; the Lie proof bridges Mathlib's scalar-extension bracket with the associative commutator bracket on matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.matrixBaseChangeLieEquiv_tmul (n : Type u_1) (R : Type u_2) (A : Type u_3) [Fintype n] [DecidableEq n] [CommRing R] [CommRing A] [Algebra R A] (a : A) (M : Matrix n n R) : (matrixBaseChangeLieEquiv n R A) (a ⊗ₜ[R] M) = a • M.map ⇑(algebraMap R A)

The scalar-extension equivalence sends a pure tensor to the entrywise scalar extension.