Presenting a Lie algebra by generators and relations

A Lie algebra presented by generators X and relations S ⊆ FreeLieAlgebra R X is the quotient of FreeLieAlgebra R X by the Lie ideal generated by S. Mathlib builds both halves of that construction — the free Lie algebra with its universal property, and the LieRing/LieAlgebra structure on a quotient by a Lie ideal — but not the bridge between them, which is what a presentation is used for: a homomorphism out of the presented algebra is the same thing as a family of images satisfying the relations. The quotient universal property is provided by TauCeti/Algebra/Lie/Quotient.lean; this file supplies two further facts needed to apply it, and leans on a third imported from TauCeti/Algebra/Lie/Basic.lean.

Relations of a presentation are frequently written as the vanishing of (ad x) ^ n y — Serre's relations for a Cartan matrix are the standard example — and such a relation says nothing about the presented algebra until it is known to be carried along by the map that checks it. That transport is LieHom.map_ad_pow, which lives in TauCeti/Algebra/Lie/Basic.lean and is imported here. The first fact supplied by this file is its companion TauCeti.ad_neg_pow_apply_eq_zero, which carries such a vanishing result from x to -x.

The second is that a free Lie algebra is generated, as a Lie subalgebra, by its generators: TauCeti.FreeLieAlgebra.lieSpan_range_of_eq_top. This is what makes the images of the generators generate the presented algebra, rather than merely determine maps out of it.

Main results

• TauCeti.ad_neg_pow_apply_eq_zero: negating the element acting by ad preserves the vanishing of an iterated adjoint action.
• TauCeti.FreeLieAlgebra.lieSpan_range_of_eq_top: the generators of a free Lie algebra generate it as a Lie subalgebra.

Roadmap

These are the general steps behind the universal property of the Serre presentation in TauCeti/Algebra/Lie/Presentation/Serre.lean, which names the generators of Matrix.ToLieAlgebra R CM and maps out of it, as required by the Chevalley--Demazure construction of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

theorem TauCeti.ad_neg_pow_apply_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {x y : L} {n : ℕ} (h : ((LieAlgebra.ad R L) x ^ n) y = 0) : ((LieAlgebra.ad R L) (-x) ^ n) y = 0

If the n-fold adjoint action of x annihilates y, then so does that of -x.

theorem TauCeti.FreeLieAlgebra.lieSpan_range_of_eq_top (R : Type u_3) [CommRing R] (X : Type u_4) : LieSubalgebra.lieSpan R (FreeLieAlgebra R X) (Set.range (FreeLieAlgebra.of R)) = ⊤

The generators of a free Lie algebra generate it as a Lie subalgebra.