Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Augmentation

The augmentation ideal of a universal enveloping algebra #

The augmentation of U(L) is the counit ε : U(L) →ₐ[R] R of its Hopf algebra structure, the algebra homomorphism induced by the zero Lie homomorphism L → R. Its kernel U⁺(L), the augmentation Hopf ideal TauCeti.HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L), is the two-sided ideal generated by the canonical Lie generators, and every algebra homomorphism out of U(L) that kills those generators is the augmentation followed by the structure map of its target. The powers of U⁺(L) are generated by products of Lie generators, and the lower central series of L maps into them: an element of the n-th term of the lower central series, where the 0-th term is L itself, lands in the (n + 1)-st power of the augmentation ideal.

The augmentation ideal and its powers are the filtration along which finite-dimensional quotients of U(L) separating L are cut out: the weighted truncations that give a finite-dimensional nilpotent Lie algebra over a field a faithful finite-dimensional nilpotent representation, and the central p-polynomials of positive characteristic, both live inside U⁺(L).

Main results #

References #

The augmentation ideal and its role in the Birkhoff embedding of a nilpotent Lie algebra follow W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §17. The proof that the augmentation ideal is generated by the Lie generators is the argument of TauCeti.SymmetricAlgebra.augmentation_toIdeal_eq_span_range_ι, adapted to a noncommutative algebra.

source
theorem TauCeti.UniversalEnvelopingAlgebra.counitAlgHom_eq_lift_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
Bialgebra.counitAlgHom R (UniversalEnvelopingAlgebra R L) = (UniversalEnvelopingAlgebra.lift R) 0

The augmentation of U(L) is the algebra homomorphism induced by the zero Lie homomorphism L → R.

source
theorem TauCeti.UniversalEnvelopingAlgebra.ι_mem_augmentation (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
(UniversalEnvelopingAlgebra.ι R) x ∈ HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)

The canonical Lie generators lie in the augmentation ideal.

source
theorem TauCeti.UniversalEnvelopingAlgebra.pow_ι_mem_augmentation_toIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) {n : ℕ} (hn : n ≠ 0) :
(UniversalEnvelopingAlgebra.ι R) x ^ n ∈ (HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)).toIdeal

Every positive power of a canonical Lie generator lies in the augmentation ideal. This is what makes a linearized polynomial in ι x with zero constant term an element of U⁺(L).

source
theorem TauCeti.UniversalEnvelopingAlgebra.eq_ofId_comp_counitAlgHom_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] (f : UniversalEnvelopingAlgebra R L →ₐ[R] A) :
f = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R (UniversalEnvelopingAlgebra R L)) ↔ ∀ (x : L), f ((UniversalEnvelopingAlgebra.ι R) x) = 0

The universal property of the augmentation. An algebra homomorphism out of U(L) kills the canonical Lie generators exactly when it is the augmentation followed by the structure map of its target.

source
theorem TauCeti.UniversalEnvelopingAlgebra.apply_eq_algebraMap_counit_of_ι_eq_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] (f : UniversalEnvelopingAlgebra R L →ₐ[R] A) (hf : ∀ (x : L), f ((UniversalEnvelopingAlgebra.ι R) x) = 0) (u : UniversalEnvelopingAlgebra R L) :
f u = (algebraMap R A) (CoalgebraStruct.counit u)

An algebra homomorphism out of U(L) that kills the canonical Lie generators evaluates every element to its augmentation, viewed as a scalar in the target.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.augmentation_toIdeal_eq_span_range_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
(HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)).toIdeal = Ideal.span (Set.range ⇑(UniversalEnvelopingAlgebra.ι R))

The augmentation ideal is generated by the Lie generators. The underlying ideal of the augmentation Hopf ideal of U(L) is the left ideal generated by the canonical Lie generators; being two-sided, it is also the two-sided ideal they generate.

source
instance TauCeti.UniversalEnvelopingAlgebra.isTwoSided_span_range_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
(Ideal.span (Set.range ⇑(UniversalEnvelopingAlgebra.ι R))).IsTwoSided

The left ideal generated by the canonical Lie generators is two-sided, being the augmentation ideal.

source
theorem TauCeti.UniversalEnvelopingAlgebra.augmentation_toIdeal_pow_eq_span_range_ι_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) :
(HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)).toIdeal ^ n = Ideal.span (Set.range ⇑(UniversalEnvelopingAlgebra.ι R) ^ n)

The n-th power of the augmentation ideal is the left ideal generated by the products of n canonical Lie generators.

source
theorem TauCeti.UniversalEnvelopingAlgebra.ι_mem_augmentation_toIdeal_pow_of_mem_lowerCentralSeries (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} {x : L} (hx : x ∈ LieModule.lowerCentralSeries R L L n) :
(UniversalEnvelopingAlgebra.ι R) x ∈ (HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)).toIdeal ^ (n + 1)

Iterated brackets lie in powers of the augmentation ideal. An element of the n-th term of the lower central series of L, whose 0-th term is L itself and whose 1-st term is ⁅L, L⁆, maps into the (n + 1)-st power of the augmentation ideal.

source
theorem TauCeti.UniversalEnvelopingAlgebra.ι_lie_mem_augmentation_toIdeal_sq (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) :
(UniversalEnvelopingAlgebra.ι R) ⁅x, y⁆ ∈ (HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R L)).toIdeal ^ 2

The bracket of two elements of L maps into the square of the augmentation ideal.