Documentation

LeanPool.Ado.RepresentationTheory.Lie.Abelian

A faithful square-zero representation of an abelian Lie algebra #

For an abelian Lie algebra L over a commutative ring R, let L act on R × L by

x • (a, y) = (0, a • x).

Every two operators in this representation have zero composite, while evaluation at (1, 0) recovers the acting element. The representation is therefore faithful and square-zero.

Over a field, this gives an explicit faithful representation of an n-dimensional abelian Lie algebra by square-zero endomorphisms of an (n + 1)-dimensional vector space. It is the basic abelian model for faithful nilrepresentations.

Main definition #

source
def Ado.abelianSquareZeroRepresentation (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] :
L →ₗ⁅R⁆ Module.End R (R × L)

The canonical representation of an abelian Lie algebra by square-zero operators on R × L. The first coordinate records the scalar that the acting element transfers to the second coordinate.

Equations
Instances For
    source
    @[simp]
    theorem Ado.abelianSquareZeroRepresentation_apply_apply (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) (z : R × L) :
    ((abelianSquareZeroRepresentation R L) x) z = (0, z.1 • x)

    The canonical representation acts by the square-zero operator construction.

    source
    @[simp]
    theorem Ado.abelianSquareZeroRepresentation_mul_eq_zero (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x y : L) :
    (abelianSquareZeroRepresentation R L) x * (abelianSquareZeroRepresentation R L) y = 0

    Any two operators in the canonical abelian representation have zero product.

    source
    @[simp]
    theorem Ado.abelianSquareZeroRepresentation_sq_eq_zero (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) :
    (abelianSquareZeroRepresentation R L) x ^ 2 = 0

    Every operator in the canonical abelian representation is square-zero.

    source
    theorem Ado.isNilpotent_abelianSquareZeroRepresentation (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] (x : L) :
    IsNilpotent ((abelianSquareZeroRepresentation R L) x)

    Every operator in the canonical abelian representation is nilpotent, uniformly with exponent two.

    source
    theorem Ado.abelianSquareZeroRepresentation_injective (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] [IsLieAbelian L] :
    Function.Injective ⇑(abelianSquareZeroRepresentation R L)

    The canonical square-zero representation of an abelian Lie algebra is injective (faithful).

    source
    theorem Ado.exists_faithful_squareZeroRepresentation (K : Type u) [Field K] (A : Type v) [LieRing A] [LieAlgebra K A] [IsLieAbelian A] [FiniteDimensional K A] :
    ∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : A →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ ∧ (∀ (x_3 y : A), ρ x_3 * ρ y = 0) ∧ Module.finrank K V = Module.finrank K A + 1

    Every finite-dimensional abelian Lie algebra A has an explicit faithful representation whose operators have pairwise-zero products, on a carrier of dimension finrank K A + 1.