Matrix targets for Lie representations

A faithful representation ρ : L →ₗ⁅K⁆ Module.End K V on a finite free module becomes an injective Lie homomorphism L →ₗ⁅K⁆ Matrix (Fin n) (Fin n) K once a basis of V is chosen, and conversely a matrix algebra acts faithfully on its coordinate space. So the endomorphism and matrix formulations of faithfulness are interchangeable. Over a field the freeness of V is automatic, so this compares finite-dimensional faithful representations with matrix embeddings.

The dictionary is a statement about two existentials and needs no finiteness of L, so it is independent of any construction of a faithful representation; a construction supplying one formulation reads off the other by rewriting.

Main result

• TauCeti.faithfulRepresentation_iff_exists_injective_lieHom_matrix: the endomorphism and matrix formulations of a faithful representation on a finite free module agree.

theorem TauCeti.faithfulRepresentation_iff_exists_injective_lieHom_matrix (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] : (∃ (V : Type (max u w)) (x : AddCommGroup V) (x_1 : Module K V) (_ : Module.Free K V) (_ : Module.Finite K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ) ↔ ∃ (n : ℕ) (f : L →ₗ⁅K⁆ Matrix (Fin n) (Fin n) K), Function.Injective ⇑f

The matrix and endomorphism formulations of faithfulness agree. A faithful representation on a finite free module becomes an injective Lie homomorphism into a matrix algebra once a basis of the carrier is chosen, and conversely a matrix algebra acts faithfully on the coordinate space, lifted to any universe containing K. No finiteness of L is needed: this is a dictionary between two existential statements.