Documentation

TauCeti.RepresentationTheory.Lie.Ado.PositiveCharacteristic

Faithful Lie representations in positive characteristic #

Every finite-dimensional Lie algebra over a field of prime characteristic admits a faithful finite-dimensional representation that sends adjoint-nilpotent elements to nilpotent endomorphisms. This is Hochschild's strengthening of the positive-characteristic Ado theorem.

The representation comes from left multiplication on a finite-dimensional quotient of the universal enveloping algebra by a power of its central augmentation ideal. The quotient construction preserves adjoint nilpotence and has the same kernel on the Lie algebra as the canonical map into its enveloping algebra. The Poincaré--Birkhoff--Witt theorem makes that canonical map injective and supplies the domain property needed by the quotient construction. The resulting existence statements involve no chosen basis or central generating family.

References #

theorem TauCeti.exists_faithful_preserving_ad_nilpotence_charP (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] :
∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ ∧ ∀ (x_3 : L), IsNilpotent ((LieAlgebra.ad K L) x_3) → IsNilpotent (ρ x_3)

Hochschild's strengthening in prime characteristic. A finite-dimensional Lie algebra has a faithful finite-dimensional representation that preserves nilpotence of the adjoint action. There is no restriction on the prime, including in characteristics two and three.

theorem TauCeti.adoCharP (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] :
∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ

Ado's theorem in prime characteristic. Every finite-dimensional Lie algebra over a field of prime characteristic admits a faithful finite-dimensional representation.