The two-dimensional nonabelian Lie algebra #
TauCeti.LieAlgebra.AffineLine K is the Lie algebra of the group of affine transformations
t ↦ a * t + b of the line: the free K-module on a dilation x and a translation y, with
⁅x, y⁆ = y. Over a field it is, up to isomorphism, the only nonabelian two-dimensional Lie
algebra (a classification not carried out here), and it is the standard witness that the nilradical
is strictly larger than Mathlib's LieAlgebra.maxNilpotentIdeal. Over any nontrivial commutative
ring, its nonzero abelian ideal of translations is contained in the nilradical, while
maxNilpotentIdeal is ⊥. Over a reduced commutative ring, the nilradical is exactly the ideal
of translations.
The adjoint action of an element u is computed here too: it sends the dilation direction into
the translation line and scales that line by the dilation coordinate u.1, so all of its positive
powers are scalar multiples of it. Over a field of positive characteristic that monic relation is
what produces the explicit central p-polynomials of
TauCeti.Algebra.Lie.UniversalEnveloping.AffineLine.
Main definitions #
TauCeti.LieAlgebra.AffineLine: the two-dimensional nonabelian Lie algebra, with itsdilationx, itstranslationy, and its idealtranslationIdealof translations.
Main statements #
TauCeti.LieAlgebra.AffineLine.ad_pow: every positive power of the adjoint action of an element is a scalar multiple of it, the scalar being a power of the dilation coordinate.TauCeti.LieAlgebra.AffineLine.nilradical_eq_translationIdeal: the nilradical is the ideal of translations, the span ofy.TauCeti.LieAlgebra.AffineLine.maxNilpotentIdeal_eq_bot: Mathlib'smaxNilpotentIdealis⊥.TauCeti.LieAlgebra.AffineLine.maxNilpotentIdeal_lt_nilradical: hence the containmentTauCeti.LieAlgebra.maxNilpotentIdeal_le_nilradicalis strict in general.
References #
- [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1-3][bourbaki1975], Chapter I, §4.
The two-dimensional nonabelian Lie algebra over K, the Lie algebra of the group of
affine transformations t ↦ a * t + b of the line: the K-module K × K, whose first coordinate
is the dilation coordinate and whose second is the translation coordinate, with the bracket
determined by ⁅x, y⁆ = y for the basis x = (1, 0), y = (0, 1).
Equations
- TauCeti.LieAlgebra.AffineLine K = (K × K)
Instances For
Equations
- TauCeti.LieAlgebra.AffineLine.instAddCommGroup = { toAddGroup := Prod.instAddGroup, add_comm := ⋯ }
Equations
- TauCeti.LieAlgebra.AffineLine.instModule = { toDistribMulAction := Prod.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- TauCeti.LieAlgebra.AffineLine.instLieAlgebra = { toModule := TauCeti.LieAlgebra.AffineLine.instModule, lie_smul := ⋯ }
The defining relation ⁅x, y⁆ = y.
The ideal of translations, the span of y: the elements whose dilation coordinate vanishes.
Equations
- TauCeti.LieAlgebra.AffineLine.translationIdeal K = { carrier := {u : TauCeti.LieAlgebra.AffineLine K | u.1 = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }
Instances For
The ideal of translations is the span of the translation y.
The translation y is nonzero.
The ideal of translations is nonzero.
The ideal of translations is abelian.
The ideal of translations is abelian, hence nilpotent as a Lie algebra, so it is contained in the nilradical.
The adjoint action of any element squares to its dilation coordinate times itself. The
operator LieAlgebra.ad K (AffineLine K) u sends the dilation direction into the translation
line and scales that line by u.1, so composing it with itself only multiplies it by u.1. In
particular it is idempotent at the dilation x, where u.1 = 1, and squares to zero at the
translation y, where u.1 = 0.
The monic relation satisfied by the adjoint action: T ^ n = u.1 ^ (n - 1) • T for every
n ≠ 0, where T = LieAlgebra.ad K (AffineLine K) u. Every positive power of T is therefore a
scalar multiple of it, the scalar being a power of the dilation coordinate. Taking n to be a
power of the characteristic turns this into a linearized relation, which is what produces a
central p-polynomial in the universal enveloping algebra.
The adjoint action of the translation y is nonzero: it sends the dilation x to -y.
The translation y survives in every term of the series ⁅N, ⁅N, … ⁆⁆ attached to an ideal
N containing an element of dilation coordinate 1, because ⁅x, y⁆ = y.
Every nonzero ideal contains the translation y.
The translation y survives in every term of the lower central series of a nonzero ideal for
the adjoint action of the whole algebra, because ⁅x, y⁆ = y.
No nonzero ideal is acted on nilpotently by the whole algebra.
Over a reduced commutative ring, an ideal that is nilpotent as a Lie algebra consists of translations.
The nilradical of the two-dimensional nonabelian Lie algebra is its ideal of translations,
the span of y (translationIdeal_toSubmodule), over any reduced commutative ring.
Mathlib's LieAlgebra.maxNilpotentIdeal of the two-dimensional nonabelian Lie algebra is
⊥ over any commutative ring: dilation acts idempotently, and every nonzero ideal
contains a translation on which it acts nontrivially.
The containment TauCeti.LieAlgebra.maxNilpotentIdeal_le_nilradical is strict in general:
over any nontrivial commutative ring, the nilradical contains the nonzero ideal of translations,
while Mathlib's LieAlgebra.maxNilpotentIdeal is ⊥.