Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.AffineLine

Central p-polynomials for the two-dimensional nonabelian Lie algebra #

TauCeti.LieAlgebra.AffineLine K is the Lie algebra of the affine line, spanned by a dilation x and a translation y with ⁅x, y⁆ = y. This file computes, explicitly and for every element, the central p-polynomial in U(L) whose existence TauCeti.UniversalEnvelopingAlgebra.exists_pCentralPolynomial asserts abstractly.

The computation is driven by one identity at the Lie-algebra level: the adjoint action of u : AffineLine K satisfies T ^ n = u.1 ^ (n - 1) • T for n ≠ 0 (TauCeti.LieAlgebra.AffineLine.ad_pow), because T kills the dilation direction into the translation line and scales that line by the dilation coordinate u.1. Taking n = p turns it into a monic linearized relation of degree p, so

ι u ^ p - u.1 ^ (p - 1) • ι u

is central in U(L); having zero constant term it also lies in the augmentation ideal, by TauCeti.UniversalEnvelopingAlgebra.pPolynomial_ι_mem_augmentation_toIdeal, so it belongs to Hochschild's Z(U(L)) ∩ U⁺(L). At the two generators this reads ι x ^ p - ι x and ι y ^ p, the two shapes a linearized polynomial can take: the adjoint action of the dilation is idempotent, and that of the translation squares to zero.

The polynomial statements assume positive characteristic, that is p ≠ 1: in characteristic zero the displayed polynomial is ι u - ι u = 0 and would say nothing.

The exponent is genuinely needed. No nonzero element of AffineLine K becomes central in U(L) (TauCeti.LieAlgebra.AffineLine.ι_mem_center_iff_eq_zero), so the polynomials above are not central for the trivial reason that their linear parts already are.

For contrast, in the one-dimensional abelian Lie algebra the exponent may be taken to be p ^ 0 = 1: U(L) is commutative there (TauCeti.UniversalEnvelopingAlgebra.instCommRing), so Subalgebra.center_eq_top makes every element central and ι x is itself a central p-polynomial.

Main statements #

References #

source
theorem TauCeti.LieAlgebra.AffineLine.ι_pow_sub_smul_ι_mem_center {K : Type u_1} [CommRing K] (p : ℕ) [ExpChar K p] (hp : p ≠ 1) (u : AffineLine K) :
(UniversalEnvelopingAlgebra.ι K) u ^ p - u.1 ^ (p - 1) • (UniversalEnvelopingAlgebra.ι K) u ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (AffineLine K))

The explicit central p-polynomial of an element of the affine line. For every u : AffineLine K the linearized polynomial ι u ^ p - u.1 ^ (p - 1) • ι u is central in U(L), where u.1 is the dilation coordinate of u. It is monic of degree p and has zero constant term, so it is a central p-polynomial in the sense of TauCeti.UniversalEnvelopingAlgebra.exists_pCentralPolynomial, exhibited here with no Noetherian search. The characteristic is positive: for p = 1 the polynomial T ^ p - T is the zero polynomial and the statement would be empty.

source
theorem TauCeti.LieAlgebra.AffineLine.ι_dilation_pow_sub_ι_dilation_mem_center (K : Type u_1) [CommRing K] (p : ℕ) [ExpChar K p] (hp : p ≠ 1) :
(UniversalEnvelopingAlgebra.ι K) (dilation K) ^ p - (UniversalEnvelopingAlgebra.ι K) (dilation K) ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (AffineLine K))

The central p-polynomial of the dilation x is ι x ^ p - ι x: the adjoint action of x is the projection onto the translation line, hence idempotent, so the linearized relation it satisfies is T ^ p = T.

source
theorem TauCeti.LieAlgebra.AffineLine.ι_translation_pow_mem_center (K : Type u_1) [CommRing K] (p : ℕ) [ExpChar K p] (hp : p ≠ 1) :
(UniversalEnvelopingAlgebra.ι K) (translation K) ^ p ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (AffineLine K))

The central p-polynomial of the translation y is the single Frobenius power ι y ^ p: the adjoint action of y squares to zero, so already T ^ p = 0 in positive characteristic. This is the shape TauCeti.UniversalEnvelopingAlgebra.exists_pow_ι_mem_center_of_isNilpotent_ad predicts for an adjoint-nilpotent element, here with the exponent p ^ 1.

source
theorem TauCeti.LieAlgebra.AffineLine.ι_translation_ne_zero (K : Type u_1) [CommRing K] [Nontrivial K] :
(UniversalEnvelopingAlgebra.ι K) (translation K) ≠ 0

The canonical Lie generator attached to the translation y is nonzero: the adjoint representation of U(L) sends it to LieAlgebra.ad K (AffineLine K) y, which moves the dilation.

source
@[simp]
theorem TauCeti.LieAlgebra.AffineLine.ι_mem_center_iff_eq_zero (K : Type u_1) [CommRing K] {u : AffineLine K} :
(UniversalEnvelopingAlgebra.ι K) u ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K (AffineLine K)) ↔ u = 0

The canonical copy of the affine line meets the centre of U(L) only in 0. Hence the passage to p-th powers in TauCeti.LieAlgebra.AffineLine.ι_pow_sub_smul_ι_mem_center is not an artifact: apart from 0, no element of the Lie algebra is already central in its enveloping algebra.

Examples in characteristics 2 and 3 #

The two smallest positive characteristics, over the prime fields, with the two central p-polynomials made completely explicit.