Chapter I. Basic Concepts
FC14 — Humphreys, Introduction to Lie Algebras and Representation Theory.
This chapter contains 24 definitions, 3 theorems, 3 propositions, 2 lemmas, 2 corollaries, 4 examples, 10 constructions, 1 convention, 1 notation, 1 formula and 1 other statements.
Of the 52 statements checked against Lean, 31 are formalized somewhere and 21 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 29 | 56% | Mathlib states and proves it. |
| not formalized | 21 | 40% | A documented search found no Lean statement of it anywhere. |
| in a Lean package | 2 | 4% | A library available as a Lake dependency has it. |
| checked in total | 52 |
- Canonical block: FC14 Humphreys Chapter I,
FC14-C01-U001–FC14-C01-U052, exactly 52 unique contiguous rows. - Search order: project
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current MathlibH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6, current/open/indexed search, Reservoir/packages, broad GitHub Lean repositories, and local reference/mapped corpora. - C01 has 29 pinned
mathlibrows, 2package-importrows, and 21 datedunmatchedrows. Mathlib positives: U001, U002, U003, U004, U005, U006, U012, U013, U015, U016, U018, U021, U022, U023, U024, U025, U027, U028, U030, U032, U033, U035, U039, U043, U045, U046, U047, U048, U049. Package positives: U020, U041. /tmp/fc14-c01-witness.leancompiles at exact P and checks the central Lie API: Lie algebras/equivalences, ideals/quotients, derivations/adjoint action, derived/lower-central series, radical, nilpotence, Engel, and flags.- The strongest external hit is
LieLean/LowDimSolvClassification@3c0efe0b3f84f3960c469a84c76fb71162a5d4d5(Apache-2.0). ItsClassification1.leanandClassification2.leangive Humphreys’ complete dimension-≤2 classification. ItsQuotientSolvable.leansupplies the extension clause missing from Mathlib’s otherwise complete solvability-closure API. A disposable copy of the full package was rebuilt unchanged against this repository’s Lean 4.33.0 and pinned Mathlib with exit 0, so these arepackage-import, not ports. - Classical
sl/sp/soobjects exist in Mathlib, but U007–U010 also bundle exact bases/dimension formulas not found as checked declarations; strict semantics keep those rows unmatched. Likewise Mathlib’s genericBasis.flagdoes not by itself supply simultaneous strict triangularization. N=2026-09-07marks dated unmatched decisions. Strict whole-row semantics apply uniformly.
Convention: ambient field and dimension convention
F denotes an arbitrary commutative field. Lie algebras are finite-dimensional over F unless explicitly stated otherwise.
Formalized. Lean/Mathlib core::Field; Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean::FiniteDimensional — Field F and FiniteDimensional F L are exactly the standing coefficient/dimension hypotheses.
Definition: Lie algebra, bracket, and Jacobi identity
A Lie algebra over F is an F-vector space L with a bilinear bracket [x,y] satisfying [x,x]=0 and the Jacobi identity [x,[y,z]]+[y,[z,x]]+[z,[x,y]]=0. Anticommutativity [x,y]=−[y,x] follows; conversely it implies [x,x]=0 when char F≠2.
Formalized. Mathlib/Algebra/Lie/Basic.lean::LieRing, LieAlgebra, LieEquiv — LieRing packages alternation and Jacobi, LieAlgebra bilinearity, and LieEquiv is a bracket-preserving linear equivalence.
Definition: Lie-algebra isomorphism
An isomorphism L→L′ is a vector-space isomorphism preserving brackets.
Formalized. Mathlib/Algebra/Lie/Basic.lean::LieRing, LieAlgebra, LieEquiv — LieRing packages alternation and Jacobi, LieAlgebra bilinearity, and LieEquiv is a bracket-preserving linear equivalence.
Definition: Lie subalgebra
A subspace K⊆L is a Lie subalgebra when [K,K]⊆K; it inherits a Lie-algebra structure.
Formalized. Mathlib/Algebra/Lie/Subalgebra.lean::LieSubalgebra — A LieSubalgebra F L is exactly a linear subspace closed under the bracket and inherits the Lie structure.
Construction: general linear Lie algebra gl(V)
For a vector space V, End(V) becomes a Lie algebra under [x,y]=xy−yx; this Lie algebra is gl(V). Relative to a basis, gl(V)≅gl(n,F) with [e_ij,e_kl]=δ_jk e_il−δ_li e_kj.
Formalized. Mathlib/Algebra/Lie/OfAssociative.lean::LieRing.ofAssociativeRing, LieAlgebra.ofAssociativeAlgebra; Mathlib/Algebra/Lie/Matrix.lean::lieEquivMatrix’ — Mathlib gives every endomorphism algebra the commutator Lie bracket and identifies endomorphisms of a coordinate module with matrices as Lie algebras; the matrix-unit bracket formula is the entrywise specialization.
Definition: linear Lie algebra
A linear Lie algebra is a Lie subalgebra of gl(V).
Formalized. Mathlib/Algebra/Lie/Subalgebra.lean::LieSubalgebra; Mathlib/Algebra/Lie/OfAssociative.lean::Module.End.instLieModule — A linear Lie algebra is exactly a LieSubalgebra of the commutator Lie algebra Module.End F V.
Construction: special linear algebra Al
The four families A_l,B_l,C_l,D_l are called the classical Lie algebras. For A_l, dim V=l+1 and sl(V)=sl(l+1,F) is the trace-zero subalgebra of gl(V), of dimension (l+1)^2−1, with the stated standard basis.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines SpecialLinear.sl and elementary trace-zero matrices, but no checked declaration owns the bundled dimension and stated standard basis for sl(l+1,F). Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: symplectic algebra Cl
A nondegenerate skew-symmetric bilinear form exists only in even dimension. For dim V=2l with such a fixed form f, sp(V)=sp(2l,F) consists of x satisfying f(xv,w)=−f(v,xw), equivalently sx=−x^t s; dim sp(2l,F)=2l^2+l.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines Symplectic.sp, but no checked theorem gives the bundled even-dimension existence criterion and dimension 2l²+l at this interface. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: odd orthogonal algebra Bl
For dim V=2l+1 with the displayed nondegenerate symmetric form, o(V)=o(2l+1,F) consists of skew-adjoint endomorphisms for that form and has dimension 2l^2+l.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines the orthogonal Lie algebra as skew-adjoint endomorphisms, but the row also fixes the displayed odd-dimensional form and its dimension formula, for which no checked bundled theorem was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: even orthogonal algebra Dl
For dim V=2l with the displayed symmetric form, o(V)=o(2l,F) is the corresponding orthogonal Lie algebra and has dimension 2l^2−l.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines the orthogonal Lie algebra, but the row also fixes the displayed even-dimensional form and dimension 2l²-l; no checked whole-row theorem was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: triangular, strictly triangular, and diagonal Lie algebras
t(n,F), n(n,F), and d(n,F) denote respectively upper triangular, strictly upper triangular, and diagonal matrix Lie algebras. One has t=d⊕n as vector spaces, [d,n]=n and [t,t]=n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No dedicated Lie subalgebras of upper-triangular, strictly-upper-triangular, and diagonal matrices with all three stated bracket/decomposition identities were found in P/H. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Notation: commutator subspace [H,K]
For subalgebras H,K⊆L, [H,K] denotes the subspace spanned by commutators [x,y] with x∈H,y∈K.
Formalized. Mathlib/Algebra/Lie/Submodule.lean::LieSubmodule.lieSpan; Mathlib/Algebra/Lie/IdealOperations.lean::LieSubmodule.lieIdeal_oper_eq_linear_span — The commutator subspace is the linear span of brackets; Mathlib’s Lie-span/bracket operation supplies exactly that span construction.
Definition: F-algebra
An F-algebra here means an F-vector space equipped with a bilinear multiplication, not assumed associative.
Formalized. Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean::NonUnitalNonAssocAlgebra — Mathlib’s nonunital nonassociative algebra interface is precisely a module with bilinear multiplication, with no associativity assumption.
Definition: derivation and Der(A)
A derivation δ:A→A is F-linear and satisfies δ(ab)=aδ(b)+δ(a)b. Der(A) is a vector subspace of End(A) closed under commutators, hence a Lie subalgebra of gl(A).
Not formalized. none; no complete checked declaration under strict bundle semantics — LieDerivation formalizes derivations of Lie algebras, while generic ring derivations assume associative algebra structure. Humphreys allows an arbitrary nonassociative bilinear algebra and also asserts its derivations form a commutator Lie subalgebra; no exact owner was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: inner and outer derivations
For a Lie algebra L, ad x:y↦[x,y] is a derivation. Derivations of the form ad x are inner; the others are outer.
Formalized. Mathlib/Algebra/Lie/Derivation/Basic.lean::LieDerivation, LieDerivation.inner; Mathlib/Algebra/Lie/AdjointAction/Derivation.lean::LieDerivation.ad; Mathlib/Algebra/Lie/OfAssociative.lean::LieAlgebra.ad — LieDerivation.inner realizes inner derivations and the adjoint map; LieAlgebra.ad is the adjoint representation into endomorphisms.
Definition: adjoint representation
The map ad:L→Der(L) sending x to ad x is the adjoint representation.
Formalized. Mathlib/Algebra/Lie/Derivation/Basic.lean::LieDerivation, LieDerivation.inner; Mathlib/Algebra/Lie/AdjointAction/Derivation.lean::LieDerivation.ad; Mathlib/Algebra/Lie/OfAssociative.lean::LieAlgebra.ad — LieDerivation.inner realizes inner derivations and the adjoint map; LieAlgebra.ad is the adjoint representation into endomorphisms.
Theorem/recorded result: Ado–Iwasawa linearity theorem
Every finite-dimensional Lie algebra over F is isomorphic to a linear Lie algebra, i.e. to a Lie subalgebra of gl(V) for some finite-dimensional V. The source records the Ado–Iwasawa theorem without proof.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked implementation of the Ado–Iwasawa theorem was found in P/H, current work, packages, or broad GitHub Lean search. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: abelian Lie algebra
A Lie algebra with identically zero bracket is abelian.
Formalized. Mathlib/Algebra/Lie/Abelian.lean::IsLieAbelian — IsLieAbelian L is exactly the assertion that every bracket in L is zero.
Construction: structure constants
For a basis x_1,…,x_n, structure constants a^k_ij are defined by [x_i,x_j]=Σ_k a^k_ij x_k. Conversely scalars satisfying the identities forced by alternation and Jacobi define an abstract Lie algebra.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has bases, brackets, and finite coordinates, but no canonical structure-constant object with the converse construction from scalars satisfying the full alternation/Jacobi identities. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Classification: Lie algebras of dimension at most two
Up to isomorphism there is one one-dimensional Lie algebra; in dimension two there are exactly the abelian algebra and, when nonabelian, the algebra with basis x,y and [x,y]=x.
Formalized. LieLean/LowDimSolvClassification@3c0efe0b3f84f3960c469a84c76fb71162a5d4d5; Lie/Classification1.lean::LieAlgebra.Dim1.classification; Lie/Classification2.lean::LieAlgebra.Dim2.classification, LieAlgebra.Dim2.not_iso — The package proves every one-dimensional Lie algebra is the unique abelian one and every two-dimensional Lie algebra is either the abelian model or the affine model, with non-isomorphism of the two models. Its complete library builds against this repository’s Lean 4.33.0 and pinned Mathlib; Apache-2.0.
Searched: LieLean/LowDimSolvClassification@3c0efe0b3f84f3960c469a84c76fb71162a5d4d5; Apache-2.0; original Lean/Mathlib v4.19.0; verified 2026-09-07 to build unchanged against Lean 4.33.0 and P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: ideal
A subspace I⊆L is an ideal when [L,I]⊆I.
Formalized. Mathlib/Algebra/Lie/Ideal.lean::LieIdeal — LieIdeal F L is a Lie submodule of the self-module, exactly a subspace stable under [L,-].
Definition: center
Z(L)={z∈L | [x,z]=0 for all x∈L} is an ideal, the center of L; L is abelian iff Z(L)=L.
Formalized. Mathlib/Algebra/Lie/Abelian.lean::LieAlgebra.center, LieAlgebra.isLieAbelian_iff_center_eq_top — Mathlib’s center is the kernel of the self action and proves L abelian iff its center is top.
Definition: derived algebra
[L,L] is the span of all commutators and is an ideal, called the derived algebra; L is abelian iff [L,L]=0.
Formalized. Mathlib/Algebra/Lie/Solvable.lean::LieAlgebra.derivedSeries, LieAlgebra.coe_derivedSeries_one_eq, LieAlgebra.abelian_iff_derived_one_eq_bot — The first derived ideal is exactly the span of all commutators, and Mathlib proves it vanishes exactly for an abelian algebra.
Construction: sum and commutator of ideals
If I,J are ideals, then I+J and [I,J] are ideals.
Formalized. Mathlib/Algebra/Lie/IdealOperations.lean::LieSubmodule.lieIdeal_oper_eq_linear_span; Mathlib/Algebra/Lie/Ideal.lean::LieIdeal — The Lie-ideal lattice supplies sums, while the bracket operation on ideals is again a Lie ideal and is the linear span of pairwise brackets.
Definition: simple Lie algebra
L is simple when its only ideals are 0 and L and [L,L]≠0. Then Z(L)=0 and L=[L,L].
Formalized. Mathlib/Algebra/Lie/Semisimple/Defs.lean::LieAlgebra.IsSimple; Mathlib/Algebra/Lie/Semisimple/Basic.lean::LieAlgebra.IsSimple.non_abelian, LieAlgebra.IsSimple.eq_bot_or_eq_top — Mathlib’s IsSimple is defined by exactly the two clauses: only zero/top ideals and non-abelianity; the center/derived consequences are immediate from those packaged lemmas and the abelian criteria.
Example: simplicity of sl(2,F)
For char F≠2, sl(2,F) with standard basis x,y,h and [x,y]=h,[h,x]=2x,[h,y]=−2y is simple.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has an sl₂ infrastructure, but targeted P/H/current/external search found no theorem proving simplicity of sl(2,F) under char F ≠ 2 at the source statement. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: quotient Lie algebra
For an ideal I, L/I is a Lie algebra with [x+I,y+I]=[x,y]+I.
Formalized. Mathlib/Algebra/Lie/Quotient.lean::LieSubmodule.Quotient — The quotient by a Lie ideal carries the induced bracket and Lie algebra structure exactly as in the source.
Definition: normalizer and self-normalizing subalgebra
For a subspace K⊆L, N_L(K)={x∈L | [x,K]⊆K} is a subalgebra and is the largest subalgebra in which K is an ideal when K is a subalgebra. K is self-normalizing when N_L(K)=K.
Formalized. Mathlib/Algebra/Lie/Normalizer.lean::LieSubalgebra.normalizer, LieSubalgebra.normalizer_eq_self_iff — Mathlib’s normalizer is exactly the largest subalgebra in which the given Lie subalgebra is an ideal, and it packages the self-normalizing equality.
Definition: centralizer
For X⊆L, C_L(X)={x∈L | [x,X]=0} is a subalgebra; C_L(L)=Z(L).
Not formalized. none; no complete checked declaration under strict bundle semantics — No Lie-subalgebra centralizer of an arbitrary subset is packaged in P/H; the center is present but only covers the special case X=L. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: Lie homomorphism, monomorphism, epimorphism
A linear map φ:L→L′ is a Lie homomorphism when it preserves brackets; it is mono when Ker φ=0, epi when Im φ=L′, and iso when both.
Formalized. Mathlib/Algebra/Lie/Basic.lean::LieHom, LieEquiv — LieHom is a bracket-preserving linear map; injective/surjective/bijective predicates give mono/epi/isomorphism, while LieEquiv is the bijective form.
Proposition: homomorphism theorems
For a Lie homomorphism φ, L/Kerφ≅Imφ and maps factor uniquely through quotients by ideals inside Kerφ; if I⊆J are ideals then (L/I)/(J/I)≅L/J; for ideals I,J, (I+J)/J≅I/(I∩J).
Not formalized. none; no complete checked declaration under strict bundle semantics — LieHom.quotKerEquivRange gives the first isomorphism theorem, but the row bundles three further quotient universal/isomorphism theorems. No checked Lie-specific declarations for the complete bundle were found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: representation of a Lie algebra
A representation of L is a Lie homomorphism φ:L→gl(V), with V allowed arbitrary dimension.
Formalized. Mathlib/Algebra/Lie/OfAssociative.lean::LieModule.toEnd — A Lie representation is equivalently a Lie-module structure; LieModule.toEnd is its Lie homomorphism into Module.End F V.
Corollary: kernel of adjoint representation
Ker(ad)=Z(L). Hence every simple Lie algebra embeds into gl(L) via its adjoint representation.
Formalized. Mathlib/Algebra/Lie/Abelian.lean::LieAlgebra.self_module_ker_eq_center; Mathlib/Algebra/Lie/AdjointAction/Derivation.lean::injective_ad_of_center_eq_bot — Mathlib identifies the adjoint kernel with the center and proves trivial center makes the adjoint representation injective; a simple Lie algebra has trivial center.
Definition: automorphism group
An automorphism is a Lie-algebra isomorphism L→L; Aut(L) denotes the group of all automorphisms.
Not formalized. none; no complete checked declaration under strict bundle semantics — L ≃ₗ⁅F⁆ L is the correct automorphism type and has identity/composition/inverse operations, but P/H does not package Beauville/Humphreys’ Aut(L) as the stated automorphism group object; the group structure would have to be assembled. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Construction: exponential of a nilpotent derivation
In characteristic zero, if δ is a nilpotent derivation then exp(δ)=Σ δ^i/i! is a finite sum and lies in Aut(L). In particular exp(ad x) is an automorphism when ad x is nilpotent.
Formalized. Mathlib/Algebra/Lie/Derivation/Basic.lean::LieDerivation.exp — In characteristic zero Mathlib defines the exponential of a nilpotent Lie derivation as a LieEquiv, exactly the stated automorphism.
Definition: inner automorphisms and Int(L)
Automorphisms exp(ad x) with ad x nilpotent are called inner; Int(L) is the subgroup of Aut(L) they generate. Int(L) is normal in Aut(L).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked Int(L) subgroup generated by exponentials of nilpotent adjoint derivations, nor its normality in the full automorphism group, was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Example: standard inner automorphism of sl(2,F)
For sl(2,F), σ=exp(ad x)exp(ad(−y))exp(ad x) is inner, has order two, and sends x↦−y, y↦−x, h↦−h; it agrees with conjugation by the corresponding product in SL(2,F).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked formalization of the displayed sl₂ inner-automorphism computation was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Formula: conjugation-exponential identity
For a linear Lie algebra L⊆gl(V) in characteristic zero and nilpotent x∈L, (exp x)y(exp x)^{-1}=exp(ad x)(y) for all y∈L.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has conjugation of endomorphisms and exponentials, but no checked theorem at this Lie interface giving exp(ad x) ad y exp(-ad x)=ad(exp(ad x)y) as a bundled identity. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: derived series and solvable Lie algebra
The derived series is L^(0)=L, L^(1)=[L,L], L^(i)=[L(i−1),L(i−1)]. L is solvable if L^(n)=0 for some n.
Formalized. Mathlib/Algebra/Lie/Solvable.lean::LieAlgebra.derivedSeries, LieAlgebra.IsSolvable, LieAlgebra.isSolvable_iff — Mathlib’s derived series is defined recursively by self-commutators and IsSolvable is exactly eventual vanishing.
Example: upper triangular Lie algebra is solvable
For L=t(n,F), L^(1)=n(n,F); higher derived terms are spanned by matrix units whose level grows at least by powers of two, so the derived series terminates.
Not formalized. none; no complete checked declaration under strict bundle semantics — No dedicated theorem that the upper-triangular matrix Lie algebra is solvable, together with its exact derived algebra identification, was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Proposition: closure properties of solvability
Subalgebras and homomorphic images of a solvable Lie algebra are solvable; if I is a solvable ideal and L/I solvable then L is solvable; the sum of two solvable ideals is solvable.
Formalized. LieLean/LowDimSolvClassification@3c0efe0b3f84f3960c469a84c76fb71162a5d4d5; Lie/QuotientSolvable.lean::LieAlgebra.solvable_of_ideal_and_quot_solvable; Mathlib/Algebra/Lie/Solvable.lean::Function.Injective.lieAlgebra_isSolvable, Function.Surjective.lieAlgebra_isSolvable, LieAlgebra.isSolvableAdd — Mathlib supplies solvability of subalgebras/injective images, surjective images, and sums of solvable ideals. The compatible package supplies the missing extension theorem: if an ideal and its quotient are solvable, then the ambient Lie algebra is solvable. Together these are exactly the bundled closure row; package builds on Lean 4.33/pinned Mathlib, Apache-2.0.
Searched: LieLean/LowDimSolvClassification@3c0efe0b3f84f3960c469a84c76fb71162a5d4d5; Apache-2.0; original Lean/Mathlib v4.19.0; verified 2026-09-07 to build unchanged against Lean 4.33.0 and P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: radical and semisimple Lie algebra
The unique maximal solvable ideal is Rad L, the radical. L is semisimple when Rad L=0; L/Rad L is semisimple.
Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib defines the radical and semisimplicity/trivial radical, but targeted search found no checked theorem that the quotient by the radical has zero radical; the full bundled row is therefore incomplete. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Definition: descending central series and nilpotent Lie algebra
The descending/lower central series is L^0=L, L^1=[L,L], L^i=[L,L^{i−1}]. L is nilpotent if L^n=0 for some n. Nilpotent Lie algebras are solvable.
Formalized. Mathlib/Algebra/Lie/Nilpotent.lean::LieModule.lowerCentralSeries, LieModule.IsNilpotent, LieAlgebra.isSolvable_of_isNilpotent — Mathlib defines the lower central series and nilpotence by its eventual vanishing and directly installs nilpotent Lie algebras as solvable.
Example: strictly upper triangular Lie algebra is nilpotent
n(n,F) is nilpotent; its lower central terms are spanned by matrix units of increasing level.
Not formalized. none; no complete checked declaration under strict bundle semantics — No dedicated theorem that the strictly-upper-triangular matrix Lie algebra is nilpotent was found in the Lie API. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Proposition: basic properties of nilpotent Lie algebras
Subalgebras and homomorphic images of a nilpotent Lie algebra are nilpotent; if L/Z(L) is nilpotent then L is nilpotent; every nonzero nilpotent L has nonzero center.
Formalized. Mathlib/Algebra/Lie/Nilpotent.lean::Function.Injective.lieAlgebra_isNilpotent, Function.Surjective.lieAlgebra_isNilpotent, LieAlgebra.nilpotent_of_nilpotent_quotient, LieAlgebra.non_trivial_center_of_isNilpotent — Mathlib supplies nilpotence under subalgebras/injective maps and quotients/surjections, the central-extension criterion L/Z(L) nilpotent ⇒ L nilpotent, and nontrivial center of a nonzero nilpotent Lie algebra.
Definition: ad-nilpotent element
An element x∈L is ad-nilpotent when ad x is a nilpotent endomorphism. Nilpotent Lie algebras consist of ad-nilpotent elements.
Formalized. Mathlib/Algebra/Lie/Nilpotent.lean::LieAlgebra.nilpotent_ad_of_nilpotent_algebra — For a nilpotent Lie algebra Mathlib gives a uniform power killing every adjoint map, hence each ad x is nilpotent.
Theorem: Engel’s Theorem
If every element of L is ad-nilpotent, then L is nilpotent.
Formalized. Mathlib/Algebra/Lie/Engel.lean::LieAlgebra.isNilpotent_iff_forall, LieModule.isNilpotent_iff_forall — Mathlib’s Engel theorem states exactly that a finite/Noetherian Lie algebra or module is nilpotent iff every represented endomorphism is nilpotent.
Lemma: nilpotent endomorphism gives ad-nilpotent operator
If x∈gl(V) is nilpotent, then ad x is nilpotent as an endomorphism of gl(V).
Formalized. Mathlib/Algebra/Lie/AdjointAction/Basic.lean::LieAlgebra.ad_nilpotent_of_nilpotent — Mathlib directly proves that if an endomorphism is nilpotent, then its adjoint action in the associative-commutator Lie algebra is nilpotent.
Theorem: Engel common-zero-vector theorem
If L⊆gl(V), V finite-dimensional and nonzero, and every element of L is a nilpotent endomorphism, then there exists 0≠v∈V with L·v=0.
Formalized. Mathlib/Algebra/Lie/Engel.lean::LieModule.isNilpotent_iff_forall; Mathlib/Algebra/Lie/Nilpotent.lean::LieModule.nontrivial_max_triv_of_isNilpotent — Engel gives nilpotence of the module from nilpotent operators; nontrivial_max_triv_of_isNilpotent then gives a nonzero vector annihilated by all of L, exactly the common-zero-vector theorem.
Definition: flag and stabilization
A flag in n-dimensional V is 0=V_0⊂V_1⊂⋯⊂V_n=V with dim V_i=i. An endomorphism stabilizes it when xV_i⊆V_i.
Not formalized. none; no complete checked declaration under strict bundle semantics — Basis.flag formalizes a full flag induced by a basis, but no canonical structure packages an arbitrary full flag together with the endomorphism-stabilization predicate exactly as stated. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Corollary: simultaneous strict triangularization
Under the common-zero-vector theorem hypotheses, there is a flag stable under L with xV_i⊆V_{i−1}; equivalently some basis identifies all elements of L with strictly upper triangular matrices.
Not formalized. none; no complete checked declaration under strict bundle semantics — The common-zero-vector theorem is formalized, but no checked simultaneous strict-triangularization theorem producing a stable flag/basis for the whole Lie algebra was found. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6
Lemma: nonzero ideal meets center in nilpotent Lie algebra
If L is nilpotent and K is a nonzero ideal, then K∩Z(L)≠0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked theorem was found stating that every nonzero ideal of a nilpotent Lie algebra intersects the center nontrivially; proving it from the central-series machinery would be substantive. Strict whole-row semantics reject proper subsets and substantive reconstruction from adjacent Lie-algebra ingredients.
Searched: N=2026-09-07; A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; P=db584cd6d46c92f209a44c0f1c829460d327499d; H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6