Chapter 7. Lie Algebra Homology and Cohomology
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 14 definitions, 7 theorems, 1 proposition, 9 lemmas, 14 corollaries, 11 examples, 11 constructions, 1 remark and 12 other statements.
Of the 80 statements checked against Lean, 17 are formalized somewhere and 63 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 63 | 79% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 16 | 20% | Mathlib states and proves it. |
| in another Lean project | 1 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 80 |
- Project-first search was performed at repo HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete C07 source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. EveryPtarget cited in the chapter table was inspected at that revision. Two composite interfaces were also compiled against the pinned project environment: the UEA map induced by a Lie homomorphism (fromUniversalEnvelopingAlgebra.lift/hom_ext) and the exact Weibel-sign affine Killing cocycle used in U074. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. H-only declarations are not treated as project-compatible. The currentMathlib/Algebra/Lie/Cochain.leanstill lists comparison with the Chevalley–Eilenberg complex as future work; targeted current searches found no Lie-module category, Lie derived-functor (co)homology, Hochschild–Serre spectral sequence, PBW completion, or universal-central-extension theory closing the unmatched bundles. T=bf90834bad4dd74ef016776cd6b4843eebb49f67isgit@github.com:TauCetiProject/TauCeti.git, Apache-2.0, audited at Lean 4.34.0-rc2. U007 is an exact reference-port throughTauCeti/Algebra/Lie/Derivation.lean::TauCeti.derivationLieAlgebra. Other TauCeti Lie infrastructure was audited but is not promoted when its hypotheses or conclusion are narrower than the source bundle.- In particular, TauCeti’s PBW development at T proves the surjective half of the symmetric-algebra-to-associated-graded map but not injectivity, so U027–U029 remain unmatched. Its complete-reducibility theorem is stated over an algebraically closed field, narrower than Weibel’s characteristic-zero-field theorem U062. Its Casimir development proves basis formulas, centrality, and nontrivial-module injectivity, but the audit found no theorem placing the source Casimir element in the augmentation ideal, so bundled U059 remains unmatched.
- Pinned Mathlib has no category of modules over a fixed Lie algebra. TauCeti explicitly records the same limitation. Therefore the pointwise U(L)-module/Lie-module dictionary is not upgraded to the natural categorical isomorphism U023, and the source enough-projectives/injectives statement U024 is not inferred from ordinary module-category facts.
- Pinned/current Mathlib and TauCeti contain extension and 2-cocycle infrastructure, but no equivalence-of-extensions structure, H² classification, or universal-central-extension package matching U044–U046 or U067–U072. Similarly no checked declaration supplies the Hochschild–Serre spectral sequence or its low-degree exact sequences U041–U042.
- The source U055 is bundled: besides Cartan’s semisimplicity/Killing criterion it asserts nondegeneracy of the trace form for a semisimple matrix Lie algebra. The latter whole-source interface was not found, so the row is not partially credited. U056’s direct-product-of-simple structure theorem and semisimplicity of every ideal likewise exceed the checked structural semisimplicity API.
- The source U003, U004, U008, U009, U012, U015 and U016 each bundle more than the adjacent pinned definitions found in the audit: respectively an arbitrary-module zero-bracket constructor, universal abelianization, free Lie algebra on a module (not merely a set), the strictly-upper-triangular nilpotence example, the upper-triangular counterexample, an additive Lie-module category, and the exact trivial-module/invariant/coinvariant functor package. Strict bundle semantics therefore leave them unmatched.
Nis dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, the exact T revision above, recorded open/current/indexed searches, GitHub code/PR searches, and broad Lean-source searches. A prerequisite, a derived consequence requiring an unformalized source theorem, a stronger restriction on the base field, or one clause of a bundled row is not credited as the route for that row.
Definition — Lie algebra over a commutative ring
Fix a commutative ring k. A Lie algebra is a nonassociative k-algebra with a bilinear bracket. After the word “satisfies,” the extraction preserves the displayed Jacobi identity but does not preserve any companion defining axiom; no absent condition is reconstructed here.
Formalized. Mathlib/Algebra/Lie/Basic.lean::LieRing; LieAlgebra — Pinned Mathlib bundles the additive/module structure, bilinear bracket, alternating law and Jacobi identity of a Lie algebra; this directly realizes the source Lie-algebra object over a commutative base ring.
Searched: P
Definition — Lie ideal, quotient, and Lie morphism
A Lie ideal h⊂g is a k-submodule with [g,h]⊂h; g/h inherits a Lie bracket, Lie morphisms are bracket-preserving k-linear maps, and 0→h→g→g/h→0 is exact.
Formalized. Mathlib/Algebra/Lie/Ideal.lean::LieIdeal, LieIdeal.incl, LieIdeal.incl_injective; Mathlib/Algebra/Lie/Quotient.lean::LieModule.Quotient.mk', LieModule.Quotient.surjective_mk', LieModule.Quotient.mk'_ker; Mathlib/Algebra/Lie/Basic.lean::LieHom — The pinned ideal inclusion and quotient map have the source injectivity, surjectivity and kernel equalities, while LieHom is the bracket-preserving linear morphism.
Searched: P
Example 7.1.1 — Abelian Lie algebras
A Lie algebra is abelian when every bracket vanishes; every k-module has this zero-bracket Lie algebra structure.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A Lie algebra is abelian when every bracket vanishes; every k-module has this zero-bracket Lie algebra structure. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction — Commutator ideal and abelianization
[g,g] is the ideal generated by all brackets and g^ab=g/[g,g] is the largest abelian quotient Lie algebra.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: [g,g] is the ideal generated by all brackets and g^ab=g/[g,g] is the largest abelian quotient Lie algebra. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Example 7.1.2 — Lie algebra underlying an associative algebra
For an associative k-algebra A, the commutator [x,y]=xy-yx makes the underlying k-module a Lie algebra Lie(A), functorially in A.
Formalized. Mathlib/Algebra/Lie/OfAssociative.lean::LieRing.ofAssociativeRing, LieAlgebra.ofAssociativeAlgebra, AlgHom.toLieHom, AlgHom.toLieHom_comp — Pinned Mathlib puts the commutator bracket on an associative algebra and sends algebra maps functorially to Lie maps, exactly the source construction.
Searched: P
Examples 7.1.3 — Matrix Lie algebras
For an associative k-algebra A, gl_m(A)=Lie(M_m(A)); standard Lie subalgebras include the orthogonal, special-linear, upper-triangular, and strictly-upper-triangular algebras, with sl_m(A)=ker(tr:gl_m(A)→A/[A,A]).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For an associative k-algebra A, gl_m(A)=Lie(M_m(A)); standard Lie subalgebras include the orthogonal, special-linear, upper-triangular, and strictly-upper-triangular algebras, with sl_m(A)=ker(tr:gl_m(A)→A/[A,A]). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Example 7.1.4 — Derivation Lie algebra
For a nonassociative k-algebra A, derivations D satisfying D(ab)=D(a)b+aD(b) form a Lie subalgebra Der(A)⊂Lie(End_k(A)) under the commutator.
Formalized. TauCeti/Algebra/Lie/Derivation.lean::TauCeti.derivationLieAlgebra; TauCeti.mem_derivationLieAlgebra; TauCeti.derivationLieAlgebra.leibniz — TauCeti defines the Leibniz derivations of an arbitrary non-unital nonassociative algebra as a Lie subalgebra of Module.End under commutator, exactly the source example. Its Lean 4.34.0-rc2 toolchain makes this reference-port only.
Searched: T
Example 7.1.5 — Free Lie algebra
The free Lie algebra f(M) on a k-module M contains M and represents k-linear maps from M to Lie algebras: Hom_k(M,g)≅Hom_Lie(f(M),g); similarly for a free Lie algebra on a set.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The free Lie algebra f(M) on a k-module M contains M and represents k-linear maps from M to Lie algebras: Hom_k(M,g)≅Hom_Lie(f(M),g); similarly for a free Lie algebra on a set. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.1.6 — Lower central series and nilpotence
Define g^2=[g,g] and g^n=[g^{n-1},g]. The Lie algebra is nilpotent when g^n=0 for some n; strictly upper-triangular matrix Lie algebras are examples.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Define g^2=[g,g] and g^n=[g^{n-1},g]. The Lie algebra is nilpotent when g^n=0 for some n; strictly upper-triangular matrix Lie algebras are examples. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.1.7 — Derived series and solvability
Define g’=[g,g] and g^{(n)}=[g{(n-1)},g{(n-1)}]. The Lie algebra is solvable when this derived series reaches zero.
Formalized. Mathlib/Algebra/Lie/Solvable.lean::LieIdeal.derivedSeriesOfIdeal; LieAlgebra.derivedSeries; LieAlgebra.IsSolvable — The pinned recursive derived series brackets each stage with itself, and IsSolvable is termination at zero, exactly the source definition.
Searched: P
Lemma 7.1.8 — Nilpotent implies solvable
Every nilpotent Lie algebra is solvable; the proof uses [gi,gj]⊂g^{i+j} to compare the derived and lower-central series.
Formalized. Mathlib/Algebra/Lie/Nilpotent.lean::LieAlgebra.isSolvable_of_isNilpotent — Pinned Mathlib supplies the source implication from nilpotence to solvability directly.
Searched: P
Example 7.1.9 — Upper-triangular Lie algebra
For commutative A, the upper-triangular Lie algebra t_m(A) is solvable but not nilpotent.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For commutative A, the upper-triangular Lie algebra t_m(A) is solvable but not nilpotent. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition — Left g-module
A left g-module is a k-module M with a bilinear action g⊗M→M satisfying [x,y]m=x(ym)-y(xm).
Formalized. Mathlib/Algebra/Lie/Basic.lean::LieRingModule; LieModule — The pinned module action satisfies the source identity [x,y]m=x(ym)-y(xm) together with scalar bilinearity.
Searched: P
Examples 7.2.1 — Standard g-modules
An A-module is a Lie(A)-module; g acts on itself by the adjoint representation; and any k-module becomes a trivial g-module by zero action.
Formalized. Mathlib/Algebra/Lie/OfAssociative.lean::LieRingModule.ofAssociativeModule, LieModule.ofAssociativeModule; Mathlib/Algebra/Lie/Basic.lean::lieAlgebraSelfModule; Mathlib/Algebra/Lie/Abelian.lean::TrivialLieModule, LieModule.IsTrivial — Pinned Mathlib supplies all three source examples: modules over an associative algebra, the adjoint self-module, and the zero-action trivial module.
Searched: P
Definition — g-module maps and g-mod
A g-module morphism is a k-linear map commuting with the g-action. These form Hom_g(M,N), and left g-modules form the additive category g-mod.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A g-module morphism is a k-linear map commuting with the g-action. These form Hom_g(M,N), and left g-modules form the additive category g-mod. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction — Trivial modules, invariants, and coinvariants
The trivial-module functor k-mod→g-mod is exact. For a g-module M, the main text defines M^g={m:xm=0 for all x}≅Hom_g(k,M) and M_g=M/gM. The adjunction and one-sided exactness conclusions assigned to Exercise 7.2.4 are not promoted.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The trivial-module functor k-mod→g-mod is exact. For a g-module M, the main text defines M^g={m:xm=0 for all x}≅Hom_g(k,M) and M_g=M/gM. The adjunction and one-sided exactness conclusions assigned to Exercise 7.2.4 are not promoted. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.2.2 — Lie algebra homology and cohomology
Define H_^{Lie}(g,M)=L_(-*g)(M), with H_0=M_g, and H^**{Lie}(g,M)=R^*(-^g)(M), with H0=Mg.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Define H_^{Lie}(g,M)=L_(-*g)(M), with H_0=M_g, and H^**{Lie}(g,M)=R^*(-^g)(M), with H0=Mg. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Examples 7.2.3 — Basic Lie (co)homology calculations
For g=0 all higher groups vanish. For a finite-rank abelian g, Lie (co)homology identifies with Tor/Ext over the polynomial enveloping ring; for a free Lie algebra on X it identifies with Tor/Ext over the free associative ring k{X}.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For g=0 all higher groups vanish. For a finite-rank abelian g, Lie (co)homology identifies with Tor/Ext over the polynomial enveloping ring; for a free Lie algebra on X it identifies with Tor/Ext over the free associative ring k{X}. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Proposition 7.2.4 — Free-ring augmentation ideal resolution
For R=k{X}, the augmentation ideal I=Xk{X} is free as a right R-module on X, so 0→I→R→k→0 is a free resolution of k.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For R=k{X}, the augmentation ideal I=Xk{X} is free as a right R-module on X, so 0→I→R→k→0 is a free resolution of k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.2.5 — (Co)homology of a free Lie algebra
For the free Lie algebra f(X), H_n(f,M)=H^n(f,M)=0 for n≥2. With trivial coefficients k, H_1(f,k)≅⊕{x∈X}k and H^1(f,k)≅∏{x∈X}k.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For the free Lie algebra f(X), H_n(f,M)=H^n(f,M)=0 for n≥2. With trivial coefficients k, H_1(f,k)≅⊕{x∈X}k and H^1(f,k)≅∏{x∈X}k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.3.1 — Tensor algebra
For a k-module M, T(M) is the graded unital associative k-algebra generated by M; the surviving text describes its tensor-power pieces M^{⊗n} and multiplication by concatenation, and says that for free M it is the free associative algebra on a basis. The defining display itself is lost at L6574.
Formalized. Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean::TensorAlgebra; TensorAlgebra.ι; TensorAlgebra.lift — Pinned TensorAlgebra is the graded unital associative algebra freely generated by the module, with the universal map and lift realizing the source tensor-algebra construction.
Searched: P
Definition 7.3.2 — Universal enveloping algebra
For a Lie algebra g, U(g)=T(g)/(i([x,y])-i(x)i(y)+i(y)i(x)); the canonical i:g→Lie(Ug) is a Lie map and U is functorial.
Formalized. Mathlib/Algebra/Lie/UniversalEnveloping.lean::UniversalEnvelopingAlgebra; UniversalEnvelopingAlgebra.ι; UniversalEnvelopingAlgebra.lift; UniversalEnvelopingAlgebra.hom_ext — Pinned Mathlib defines the quotient by the commutator relations and its universal Lie-to-algebra map. The audited P-compiled probe defines U(f) by lift (ι ∘ f) and proves identity/composition by hom_ext, supplying the source functoriality at the exact project pin.
Searched: P
Theorem 7.3.3 — g-modules are U(g)-modules
The category of left g-modules is naturally isomorphic to U(g)-mod: a g-action extends uniquely to U(g), and restriction along i gives the inverse construction.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The category of left g-modules is naturally isomorphic to U(g)-mod: a g-action extends uniquely to U(g), and restriction along i gives the inverse construction. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.3.4 — Enough projectives and injectives in g-mod
Via g-mod≅U(g)-mod, the category g-mod has enough projectives and enough injectives; U(g) itself is projective.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Via g-mod≅U(g)-mod, the category g-mod has enough projectives and enough injectives; U(g) itself is projective. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Example 7.3.5 — Augmentation ideal of U(g)
The unique algebra map ε:U(g)→k killing g is the augmentation; its kernel I is the two-sided ideal generated by i(g), and k≅U(g)/I is the trivial g-module.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The unique algebra map ε:U(g)→k killing g is the augmentation; its kernel I is the two-sided ideal generated by i(g), and k≅U(g)/I is the trivial g-module. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.3.6 — Lie (co)homology as Tor and Ext
For every g-module M, H_(g,M)≅Tor_^{U(g)}(k,M) and H^*(g,M)≅Ext^**{U(g)}(k,M), because coinvariants are k⊗*{U(g)}M and invariants are Hom_{U(g)}(k,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For every g-module M, H_(g,M)≅Tor_^{U(g)}(k,M) and H^*(g,M)≅Ext^**{U(g)}(k,M), because coinvariants are k⊗*{U(g)}M and invariants are Hom_{U(g)}(k,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Poincaré–Birkhoff–Witt Theorem 7.3.7
If g is free as a k-module with ordered basis {e_α}, then U(g) is free over k with basis the ordered monomials e_{α1}⋯e_{αp} for nondecreasing index sequences.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If g is free as a k-module with ordered basis {e_α}, then U(g) is free over k with basis the ordered monomials e_{α1}⋯e_{αp} for nondecreasing index sequences. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.3.8 — g embeds in U(g)
Under the PBW hypotheses, i:g→U(g) is injective, so g may be identified with its image in U(g).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Under the PBW hypotheses, i:g→U(g) is injective, so g may be identified with its image in U(g). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.3.9 — Freeness over an enveloping subalgebra
If h⊂g is a Lie subalgebra over a field k, then U(g) is free as a U(h)-module, by extending an ordered basis of h to one of g and applying PBW.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If h⊂g is a Lie subalgebra over a field k, then U(g) is free as a U(h)-module, by extending an ordered basis of h to one of g and applying PBW. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction — Augmentation-ideal Tor exact sequences for H1
From 0→I→U(g)→k→0, applying Tor gives H_n(g,M)≅Tor_{n-1}^{U(g)}(I,M) for n≥2 and the exact sequence 0→H_1(g,M)→I⊗_{U(g)}M→M→M_g→0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: From 0→I→U(g)→k→0, applying Tor gives H_n(g,M)≅Tor_{n-1}^{U(g)}(I,M) for n≥2 and the exact sequence 0→H_1(g,M)→I⊗_{U(g)}M→M→M_g→0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.4.1 — H1(g,k) is the abelianization
For every Lie algebra g, H_1(g,k)≅g^ab.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For every Lie algebra g, H_1(g,k)≅g^ab. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.4.2 — H1 with trivial coefficients
For a trivial g-module M, H_1(g,M)≅g^ab⊗_k M.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For a trivial g-module M, H_1(g,M)≅g^ab⊗_k M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction / Definition 7.4.3 — Cohomological augmentation sequence and derivations
After the interleaved exercises, main text resumes by applying Ext to 0→I→U(g)→k→0: Hn(g,M)≅Ext_{U(g)}{n-1}(I,M) for n≥2 and 0→Mg→M→Hom_g(I,M)→H1(g,M)→0. Definition 7.4.3 then defines derivations D:g→M by D([x,y])=x(Dy)−y(Dx); for trivial M, Der(g,M)=Hom_k(g^ab,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: After the interleaved exercises, main text resumes by applying Ext to 0→I→U(g)→k→0: Hn(g,M)≅Ext_{U(g)}{n-1}(I,M) for n≥2 and 0→Mg→M→Hom_g(I,M)→H1(g,M)→0. Definition 7.4.3 then defines derivations D:g→M by D([x,y])=x(Dy)−y(Dx); for trivial M, Der(g,M)=Hom_k(g^ab,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Example 7.4.4 — Inner derivations
Each m∈M defines D_m(x)=xm; these inner derivations form the submodule Der_Inn(g,M)⊂Der(g,M).
Formalized. Mathlib/Algebra/Lie/Derivation/Basic.lean::LieDerivation.inner — The pinned linear map sends m to the derivation x ↦ x·m; its range is precisely the source submodule of inner derivations.
Searched: P
Example 7.4.5 — Derivations from augmentation-ideal maps
A g-map φ:I→M gives a derivation D_φ(x)=φ(i(x)); this is the Lie-algebra analogue of the group-cohomology augmentation-ideal construction.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A g-map φ:I→M gives a derivation D_φ(x)=φ(i(x)); this is the Lie-algebra analogue of the group-cohomology augmentation-ideal construction. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Lemma 7.4.6 — Homg(I,M) represents derivations
The assignment φ↦D_φ is a natural isomorphism Hom_g(I,M)≅Der(g,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The assignment φ↦D_φ is a natural isomorphism Hom_g(I,M)≅Der(g,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.4.7 — H^1 is derivations modulo inner derivations
There is a natural isomorphism H^1(g,M)≅Der(g,M)/Der_Inn(g,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: There is a natural isomorphism H^1(g,M)≅Der(g,M)/Der_Inn(g,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.4.8 — H^1 for a trivial module
If M is trivial, H1(g,M)≅Der(g,M)≅Hom_Lie(g,M)≅Hom_k(gab,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If M is trivial, H1(g,M)≅Der(g,M)≅Hom_Lie(g,M)≅Hom_k(gab,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction 7.4.9 — Semidirect product Lie algebra
For a g-module M, the k-module M×g becomes M⋊g with [(m,g),(n,h)]=(gn-hm,[g,h]); it is an extension of g by the abelian ideal M.
Formalized. Mathlib/Algebra/Lie/SemiDirect.lean::LieAlgebra.SemiDirectSum; LieAlgebra.SemiDirectSum.inl; LieAlgebra.SemiDirectSum.projr; LieAlgebra.SemiDirectSum.instIsExtension — For an abelian coefficient module, the pinned bracket specializes to [(m,g),(n,h)]=(g·n-h·m,[g,h]), and the inclusion/projection form the source extension.
Searched: P
Lemma 7.5.1 — Invariants/coinvariants for a Lie ideal
If h⊲g and M is a g-module, M_h and M^h are g/h-modules; restriction g/h-mod→g-mod has -_h as left adjoint and -^h as right adjoint.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If h⊲g and M is a g-module, M_h and M^h are g/h-modules; restriction g/h-mod→g-mod has -_h as left adjoint and -^h as right adjoint. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Hochschild–Serre Spectral Sequence 7.5.2
For h⊲g there are convergent first-quadrant sequences E^2_{pq}=H_p(g/h,H_q(h,M))⇒H_{p+q}(g,M) and E_2{pq}=Hp(g/h,Hq(h,M))⇒H{p+q}(g,M).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For h⊲g there are convergent first-quadrant sequences E^2_{pq}=H_p(g/h,H_q(h,M))⇒H_{p+q}(g,M) and E_2{pq}=Hp(g/h,Hq(h,M))⇒H{p+q}(g,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction 7.5.3 — Low-degree Hochschild–Serre exact sequences
The homological and cohomological five-term/low-degree exact sequences are extracted from 7.5.2, relating H_2,H_1 and H1,H2 of g, g/h, and h with the induced (co)invariants.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The homological and cohomological five-term/low-degree exact sequences are extracted from 7.5.2, relating H_2,H_1 and H1,H2 of g, g/h, and h with the induced (co)invariants. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.6.1 — Extension of Lie algebras
An extension of g by M is 0→M→e→g→0 with M abelian; it canonically induces a g-module structure on M by g·m=[g~,m], independent of the chosen lift g~.
Formalized. Mathlib/Algebra/Lie/Extension.lean::LieAlgebra.Extension; LieAlgebra.Extension.incl_injective; LieAlgebra.Extension.proj_surjective; LieAlgebra.Extension.ringModuleOf; LieAlgebra.Extension.lieModuleOf; LieAlgebra.Extension.ringModuleOf_bracket_proj — Pinned Mathlib bundles the short exact Lie extension and, when the kernel is abelian, constructs the quotient Lie-module action; ringModuleOf_bracket_proj proves it is computed by bracketing with any lift, hence independent of the lift as in the source.
Searched: P
Construction 7.6.2 — Extension problem and equivalence
For a fixed g-module M, two extensions inducing that action are equivalent when an isomorphism of middle Lie algebras fixes M and g; Ext(g,M) denotes the set of equivalence classes.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For a fixed g-module M, two extensions inducing that action are equivalent when an isomorphism of middle Lie algebras fixes M and g; Ext(g,M) denotes the set of equivalence classes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Classification Theorem 7.6.3 — H^2 classifies Lie algebra extensions
Equivalence classes of extensions of g by M are in natural bijection with H^2_{Lie}(g,M); the class of an extension is d^2(id_M) in its Hochschild–Serre low-degree sequence.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Equivalence classes of extensions of g by M are in natural bijection with H^2_{Lie}(g,M); the class of an extension is d^2(id_M) in its Hochschild–Serre low-degree sequence. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Lemma 7.6.4 — Every H^2 class is realized by an extension
Every class in H^2(g,M) is the class of some extension, constructed from a free presentation f→g and a suitable quotient of the semidirect product M⋊f.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Every class in H^2(g,M) is the class of some extension, constructed from a free presentation f→g and a suitable quotient of the semidirect product M⋊f. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction — Chevalley–Eilenberg modules and augmentation
Assume g is free over k. Set V_p(g)=U(g)⊗_kΛ^p g, so each V_p is free over U(g); with V_0=U(g), V_1=U(g)⊗g, the augmentation and multiplication differential give V_1→V_0→k→0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Assume g is free over k. Set V_p(g)=U(g)⊗_kΛ^p g, so each V_p is free over U(g); with V_0=U(g), V_1=U(g)⊗g, the augmentation and multiplication differential give V_1→V_0→k→0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.7.1 — Chevalley–Eilenberg differential
On V_p=U(g)⊗Λ^p g, define d as the alternating sum of action terms ux_i and bracket terms [x_i,x_j]; this extends the low-degree map and makes V_*(g) the Chevalley–Eilenberg (standard) complex.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: On V_p=U(g)⊗Λ^p g, define d as the alternating sum of action terms ux_i and bracket terms [x_i,x_j]; this extends the low-degree map and makes V_*(g) the Chevalley–Eilenberg (standard) complex. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.7.2 — Chevalley–Eilenberg resolution
The augmented complex V_(g)→k is a projective U(g)-resolution of k; the proof filters V_ and uses PBW, the spectral sequence of a filtered complex, and a Koszul complex.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The augmented complex V_(g)→k is a projective U(g)-resolution of k; the proof filters V_ and uses PBW, the spectral sequence of a filtered complex, and a Koszul complex. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.7.3 — Chevalley–Eilenberg formulas for homology and cohomology
For right M, H_*(g,M) is the homology of M⊗_kΛ^g; for left M, H^(g,M) is the cohomology of Hom_k(Λ^*g,M), with the standard alternating action-and-bracket coboundary.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For right M, H_*(g,M) is the homology of M⊗_kΛ^g; for left M, H^(g,M) is the cohomology of Hom_k(Λ^*g,M), with the standard alternating action-and-bracket coboundary. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Application 7.7.4 — Cohomological dimension bound
If g is n-dimensional over a field, then H_i(g,M)=H^i(g,M)=0 for i>n for all coefficients, since Λ^i g=0; the following exercise shows the cohomological dimension is exactly n.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If g is n-dimensional over a field, then H_i(g,M)=H^i(g,M)=0 for i>n for all coefficients, since Λ^i g=0; the following exercise shows the cohomological dimension is exactly n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.8.1 — Solvable radical and semisimple Lie algebra
For finite-dimensional g, rad(g) is its largest solvable ideal. The Lie algebra is semisimple when rad(g)=0, and simple when it is nonabelian with no nonzero proper ideals.
Formalized. Mathlib/Algebra/Lie/Solvable.lean::LieAlgebra.radical, LieAlgebra.radicalIsSolvable, LieIdeal.solvable_iff_le_radical; Mathlib/Algebra/Lie/Semisimple/Defs.lean::LieAlgebra.HasTrivialRadical, LieAlgebra.IsSimple — In the finite-dimensional/Noetherian source setting, the pinned radical is solvable and contains exactly every solvable ideal; HasTrivialRadical states radical zero, and IsSimple is nonabelian with no proper nonzero ideal.
Searched: P
Lemma 7.8.2 — Quotient by the radical is semisimple
For finite-dimensional g, the quotient g/rad(g) is semisimple.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For finite-dimensional g, the quotient g/rad(g) is semisimple. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition 7.8.3 — Killing form
For finite-dimensional g, the Killing form κ(x,y)=tr(ad(x)ad(y)) is a symmetric g-invariant bilinear form; for matrix subalgebras the trace form β(x,y)=tr(xy) is likewise invariant.
Formalized. Mathlib/Algebra/Lie/TraceForm.lean::LieModule.traceForm, LieModule.traceForm_isSymm, LieModule.traceForm_lieInvariant, LieAlgebra.killingForm — Pinned Mathlib defines the trace form of any finite-dimensional Lie representation, proves symmetry and Lie invariance, and specializes the adjoint trace form to the Killing form. The defining matrix representation gives the source matrix trace form.
Searched: P
Cartan Criterion 7.8.4
Over a characteristic-zero field, a finite-dimensional g is semisimple iff its Killing form is nondegenerate; for a semisimple matrix Lie algebra the trace form is also nondegenerate.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Over a characteristic-zero field, a finite-dimensional g is semisimple iff its Killing form is nondegenerate; for a semisimple matrix Lie algebra the trace form is also nondegenerate. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Structure Theorem 7.8.5 — Semisimple Lie algebras split into simples
A finite-dimensional Lie algebra over a characteristic-zero field is semisimple iff it is a finite direct product of simple Lie algebras; consequently every ideal of a semisimple algebra is semisimple.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A finite-dimensional Lie algebra over a characteristic-zero field is semisimple iff it is a finite direct product of simple Lie algebras; consequently every ideal of a semisimple algebra is semisimple. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.8.6 — Semisimple Lie algebras are perfect
In characteristic zero, finite-dimensional semisimple g satisfies g=[g,g], hence H_1(g,k)=H^1(g,k)=0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: In characteristic zero, finite-dimensional semisimple g satisfies g=[g,g], hence H_1(g,k)=H^1(g,k)=0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.8.7 — Semisimple matrix Lie algebras lie in sln
If g⊂gl_n is semisimple, then g⊂sl_n=[gl_n,gl_n].
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If g⊂gl_n is semisimple, then g⊂sl_n=[gl_n,gl_n]. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction 7.8.8 — Casimir operator
For a finite-dimensional g-module M with semisimple g, let h be the image of g in gl(M). Using dual bases for the nondegenerate trace form on h, c_M=Σe_i e^i∈U(g) is basis-independent, central, lies in the augmentation ideal, and acts by a nonzero scalar on nontrivial simple M.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For a finite-dimensional g-module M with semisimple g, let h be the image of g in gl(M). Using dual bases for the nondegenerate trace form on h, c_M=Σe_i e^i∈U(g) is basis-independent, central, lies in the augmentation ideal, and acts by a nonzero scalar on nontrivial simple M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.8.9 — Vanishing for nontrivial simple modules
If g is semisimple over a characteristic-zero field and M is simple with M≠k, then H_i(g,M)=H^i(g,M)=0 for every i; the Casimir element acts invertibly on M but trivially on k.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: If g is semisimple over a characteristic-zero field and M is simple with M≠k, then H_i(g,M)=H^i(g,M)=0 for every i; the Casimir element acts invertibly on M but trivially on k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.8.10 — Whitehead’s first lemma
For finite-dimensional M over a characteristic-zero semisimple g, H^1(g,M)=0; equivalently every derivation g→M is inner.
Formalized. Mathlib/Algebra/Lie/CartanCriterion.lean::LieAlgebra.hasTrivialRadical_iff_isKilling; Mathlib/Algebra/Lie/Derivation/Killing.lean::LieDerivation.exists_eq_ad — Under the source finite-dimensional characteristic-zero semisimple hypothesis, the pinned Cartan criterion gives nondegenerate Killing form, and exists_eq_ad proves every derivation is inner. This is the equivalence explicitly stated on the source row as Whitehead first lemma.
Searched: P
Weyl’s Theorem 7.8.11 — Complete reducibility
Every finite-dimensional module over a characteristic-zero semisimple Lie algebra is a direct sum of simple g-modules.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Every finite-dimensional module over a characteristic-zero semisimple Lie algebra is a direct sum of simple g-modules. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.8.12 — Whitehead’s second lemma
For finite-dimensional M over a characteristic-zero semisimple g, H^2(g,M)=0; equivalently every such Lie extension class vanishes.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For finite-dimensional M over a characteristic-zero semisimple g, H^2(g,M)=0; equivalently every such Lie extension class vanishes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Reusable comparison — No third Whitehead lemma
For sl_2 over the stated field, H^3(sl_2,k)≅k, so the degree-one and degree-two Whitehead vanishing has no degree-three analogue.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For sl_2 over the stated field, H^3(sl_2,k)≅k, so the degree-one and degree-two Whitehead vanishing has no degree-three analogue. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Levi’s Theorem 7.8.13
Every finite-dimensional Lie algebra g over a characteristic-zero field has a semisimple Levi factor L with g≅rad(g)⋊L and L≅g/rad(g).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Every finite-dimensional Lie algebra g over a characteristic-zero field has a semisimple Levi factor L with g≅rad(g)⋊L and L≅g/rad(g). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Reusable comparison — Levi factors and Malcev conjugacy
Any Levi factors are isomorphic to g/rad(g); Malcev’s refinement says all Levi factors are conjugate by suitable automorphisms of g.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Any Levi factors are isomorphic to g/rad(g); Malcev’s refinement says all Levi factors are conjugate by suitable automorphisms of g. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Definition — Central and universal central extensions; perfect Lie algebra
A central extension has kernel in the center, hence trivial g-action. It is universal if it admits a unique map over g to every central extension. Existence forces g to be perfect, g=[g,g].
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A central extension has kernel in the center, hence trivial g-action. It is universal if it admits a unique map over g to every central extension. Existence forces g to be perfect, g=[g,g]. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction 7.9.1 — Universal central extension from a free presentation
For a free presentation 0→r→f→g→0, f/[r,f]→g is central; if g is perfect, restricting to [f,f]/[r,f] gives a central extension with kernel (r∩[f,f])/[r,f]=H_2(g,k).
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For a free presentation 0→r→f→g→0, f/[r,f]→g is central; if g is perfect, restricting to [f,f]/[r,f] gives a central extension with kernel (r∩[f,f])/[r,f]=H_2(g,k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.9.2 — Existence and kernel of the universal central extension
A Lie algebra g has a universal central extension iff it is perfect. For a free presentation f/r, the universal extension is 0→H_2(g,k)→[f,f]/[r,f]→g→0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: A Lie algebra g has a universal central extension iff it is perfect. For a free presentation f/r, the universal extension is 0→H_2(g,k)→[f,f]/[r,f]→g→0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Lemma 7.9.3 — Uniqueness from a perfect source
Between central extensions over g, if the source middle Lie algebra e is perfect, there is at most one homomorphism e→e’ over g.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Between central extensions over g, if the source middle Lie algebra e is perfect, there is at most one homomorphism e→e’ over g. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Recognition Criterion 7.9.4 — Simply connected Lie algebras
Call g simply connected when every central extension splits uniquely. A central extension e→g is universal iff e is perfect and simply connected; then H_1(e,k)=H_2(e,k)=0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Call g simply connected when every central extension splits uniquely. A central extension e→g is universal iff e is perfect and simply connected; then H_1(e,k)=H_2(e,k)=0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.9.5 — Semisimple Lie algebras are simply connected
For finite-dimensional semisimple g over a characteristic-zero field, the corollary states that g is simply connected. The extraction renders the accompanying homology vanishing as H_2(e,k)=0 although no e is introduced on the corollary line; this OCR-variable gap is not silently normalized.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For finite-dimensional semisimple g over a characteristic-zero field, the corollary states that g is simply connected. The extraction renders the accompanying homology vanishing as H_2(e,k)=0 although no e is introduced on the corollary line; this OCR-variable gap is not silently normalized. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Construction — Current Lie algebra and base-change homology
For simple finite-dimensional g in characteristic zero, g[t,t^{-1}]=g⊗k[t,t^{-1}]. Its Chevalley–Eilenberg complex base-changes from g, so over k[t,t^{-1}] its homology is H_*(g,k)⊗k[t,t^{-1}], implying H_1=H_2=0 there; viewed over k it remains perfect but acquires nonzero H_2.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For simple finite-dimensional g in characteristic zero, g[t,t^{-1}]=g⊗k[t,t^{-1}]. Its Chevalley–Eilenberg complex base-changes from g, so over k[t,t^{-1}] its homology is H_*(g,k)⊗k[t,t^{-1}], implying H_1=H_2=0 there; viewed over k it remains perfect but acquires nonzero H_2. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Affine Lie Algebras 7.9.6 — Cocycle central extension of the current algebra
Using the Killing form κ, define β(Σx_iti,Σy_jtj)=Σ i κ(x_i,y_{-i}). This alternating form is a 2-cocycle and yields 0→k→ĝ→g[t,t^{-1}]→0, the affine Lie algebra attached to g.
Formalized. Mathlib/Algebra/Lie/Loop.lean::LieAlgebra.loopAlgebra, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear, LieAlgebra.LoopAlgebra.residuePairing_apply; Mathlib/Algebra/Lie/TraceForm.lean::LieAlgebra.killingForm; Mathlib/Algebra/Lie/Extension.lean::LieAlgebra.Extension.ofTwoCocycle — The audited P-compiled sign probe shows that the negative of the pinned loop cocycle evaluates on x t^i,y t^j as i·κ(x,y) when j=-i and zero otherwise, exactly Weibel’s β; Extension.ofTwoCocycle yields the stated central extension.
Searched: P
Lemma 7.9.7 — The affine Lie algebra is perfect
The affine central extension ĝ is perfect: its center lies in [ĝ,ĝ] by the cocycle formula and the quotient current algebra is already perfect.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: The affine central extension ĝ is perfect: its center lies in [ĝ,ĝ] by the cocycle formula and the quotient current algebra is already perfect. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Lemma 7.9.8 — Normalized splittings exist
For every central extension of g[t,t^{-1}], there exists a vector-space splitting σ whose associated 2-cocycle f_σ vanishes whenever one argument lies in the constant copy of g; Whitehead’s first lemma supplies the correcting coboundary.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For every central extension of g[t,t^{-1}], there exists a vector-space splitting σ whose associated 2-cocycle f_σ vanishes whenever one argument lies in the constant copy of g; Whitehead’s first lemma supplies the correcting coboundary. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Lemma 7.9.9 — Normalized cocycles are Killing-form valued
Over k=C, for a normalized splitting σ every coefficient bilinear form f_σ(x t^i,y t^j) is g-invariant, hence equals κ(x,y)c_{ij} for some c_{ij} in the central kernel.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Over k=C, for a normalized splitting σ every coefficient bilinear form f_σ(x t^i,y t^j) is g-invariant, hence equals κ(x,y)c_{ij} for some c_{ij} in the central kernel. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Corollary 7.9.10 — Normalized cocycles are multiples of β
Over C, the cocycle of a normalized splitting has the form f_σ(x,y)=β(x,y)c for a single central element c; equivalently c_{i,-i}=ic and c_{ij}=0 when i+j≠0.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: Over C, the cocycle of a normalized splitting has the form f_σ(x,y)=β(x,y)c for a single central element c; equivalently c_{i,-i}=ic and c_{ij}=0 when i+j≠0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Theorem 7.9.11 (Garland) — Universal affine central extension
For finite-dimensional simple g over C, the affine Lie algebra ĝ of 7.9.6 is the universal central extension of g[t,t^{-1}].
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For finite-dimensional simple g over C, the affine Lie algebra ĝ of 7.9.6 is the universal central extension of g[t,t^{-1}]. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.
Remark 7.9.12 — Semisimple and base-field variants
For semisimple g=∏g_i over C, the universal central extension of the current algebra is the product of the affine extensions with kernel k^r. Over subfields, the kernel dimension reflects the number of simple factors after complexification.
Not formalized. partial: adjacent Lie-algebra, enveloping-algebra, extension, semisimple, or cochain infrastructure — No checked A/P/H/T declaration realizes the whole source bundle: For semisimple g=∏g_i over C, the universal central extension of the current algebra is the product of the affine extensions with kernel k^r. Over subfields, the kernel dimension reflects the number of simple factors after complexification. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, or a proper subset do not own the row.