WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Universal enveloping algebra

Revision #1650 → #2471 · back to history

modifiedUniversal enveloping algebra (informal)e27d99e4ed7f
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—The universal enveloping algebra as an R-algebra is defined in Mathlib.Algebra.Lie.UniversalEnveloping.
status—formalized
modifiedIdentification with left-invariant differential operatorsf86af6cc4f7c
FieldFrom #1650To #2471
mathlib.decl—LeftInvariantDerivation
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
note—Mathlib defines the Lie algebra of left-invariant derivations on a Lie group but not its isomorphism with U(g).
status—partial
modifiedUniversal enveloping algebra as largest embedding801602344f52
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—This is Mathlib's `UniversalEnvelopingAlgebra R L`, characterised by the universal property `UniversalEnvelopingAlgebra.lift`.
status—formalized
modifiedU(g) via generators and relations3f5c39a64be6
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—Mathlib builds U(g) as the tensor algebra quotiented by the Lie-compatibility relation `UniversalEnvelopingAlgebra.Rel`, i.e. by exactly this generators/relations presentation.
status—formalized
modifiedUniversal enveloping algebra of sl(2,C)46768e7588ac
FieldFrom #1650To #2471
mathlib.decl—IsSl2Triple
mathlib.match_kind——
mathlib.module—Mathlib.Algebra.Lie.Sl2
note—Mathlib has `IsSl2Triple` characterising sl₂-triples in a Lie algebra but does not compute the enveloping algebra of sl(2,ℂ) explicitly.
status—partial
modifiedPBW basis spans U(g) (preview)5dad205518dd
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Poincaré–Birkhoff–Witt basis result appears in Mathlib (grep and loogle for `Birkhoff`/`PBW` return no hits).
status—not_formalized
modifiedFormal definition of U(g) as a quotient063cf150569d
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—`UniversalEnvelopingAlgebra R L` is literally the quotient of the tensor algebra by the ring congruence generated by `Rel.lie_compat`.
status—formalized
modifiedU for Lie superalgebras0ee6974adba8
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not have Lie superalgebras (grep for `LieSuperalgebra` returns no files).
status—not_formalized
modifiedGerstenhaber algebra via exterior productfe1d1f6b6339
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Gerstenhaber algebra in Mathlib (grep returns no hits).
status—not_formalized
modifiedUniversal property of U(g)02ac0cc12702
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra.lift
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—`UniversalEnvelopingAlgebra.lift` gives the bijection between Lie-algebra maps `L →ₗ⁅R⁆ A` and algebra maps `U(L) →ₐ[R] A`, with uniqueness via `hom_ext`/`lift_unique`.
status—formalized
modifiedPoincaré–Birkhoff–Witt theorem (basis form)877d4358cd7d
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Comments in `Mathlib.Algebra.Lie.Free` and `Mathlib.Algebra.Lie.SerreConstruction` explicitly note that PBW is not available in Mathlib.
status—not_formalized
modifiedPBW: U(g) and symmetric algebra are isomorphic vector spaces793ed4ea9184
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `SymmetricAlgebra` but no vector-space isomorphism `U(g) ≃ S(g)` from PBW.
status—not_formalized
modifiedPBW theorem (coordinate-free)554d9de1d299
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No PBW statement (basis or filtered/graded form) exists in Mathlib.
status—not_formalized
modifiedJordan algebra construction yields exterior algebra71de074ca3db
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has Jordan algebras and exterior algebras separately but no PBW-style relation between them.
status—not_formalized
modifiedLeft-invariant differential operators isomorphic to U(g)16ac15aa5f9d
FieldFrom #1650To #2471
mathlib.decl—LeftInvariantDerivation
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
note—Only the Lie algebra of left-invariant derivations is defined; its algebra of higher-order operators and the isomorphism with `UniversalEnvelopingAlgebra` are not.
status—partial
modifiedAlgebra of symbols74cdf7571480
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `algebra of symbols` construction on U(g) exists in Mathlib.
status—not_formalized
modifiedHeisenberg algebra and Weyl algebra (Moyal product)00f749f145d0
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the Heisenberg Lie algebra nor the Weyl algebra is defined in Mathlib.
status—not_formalized
modifiedRepresentations of g correspond to U(g)-modules6e542e4037d0
FieldFrom #1650To #2471
mathlib.decl—UniversalEnvelopingAlgebra.lift
mathlib.match_kind——
mathlib.module—Mathlib.Algebra.Lie.UniversalEnveloping
note—The infrastructure (`LieModule`, `UniversalEnvelopingAlgebra.lift` into `Module.End`) is present but the explicit equivalence between Lie modules and U(g)-modules is not stated as a theorem.
status—partial
modifiedKronecker product isomorphism385a74759caa
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Hopf-algebra comultiplication/Kronecker product on `UniversalEnvelopingAlgebra` is defined in Mathlib.
status—not_formalized
modifiedU of free Lie algebra is free associative algebra77c43eddbf40
FieldFrom #1650To #2471
mathlib.decl—FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Lie.Free
note—`FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra` gives the algebra equivalence `U(FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X`.
status—formalized
modifiedCasimir operators as basis of center15f9ce1f5b42
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Casimir` declarations in Mathlib (grep and loogle both return zero hits).
status—not_formalized
modifiedQuadratic Casimir operator99d3a54f9975
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no Casimir operator construction.
status—not_formalized
addedHarish-Chandra isomorphism for center of U(g)2c5921d9ed3a
modifiedNumber of independent Casimirs equals rank84336cdb501c
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`LieAlgebra.rank` exists but no theorem relating it to the number of independent Casimirs (which are not defined).
status—not_formalized
modifiedCasimir for SO(3): squared angular momentum91a3a76c07cf
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Casimir for SO(3) or angular-momentum-squared operator is defined in Mathlib.
status—not_formalized
modifiedQuadratic Casimir as Laplacian on Riemannian manifoldsccc966192031
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This link between Casimir operator and Laplace–Beltrami operator is not formalized.
status—not_formalized
modifiedAbelian Lie algebra: U(g) is polynomial algebraac2d75b32e43
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `IsLieAbelian` and `MvPolynomial` but no isomorphism `U(g) ≃ MvPolynomial ι R` for abelian g.
status—not_formalized
modifiedLie group case: U(g) as left-invariant differential operators14864b944c48
FieldFrom #1650To #2471
mathlib.decl—LeftInvariantDerivation
mathlib.match_kind——
mathlib.module—Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
note—The Lie algebra of left-invariant derivations exists, but no realisation of U(g) as invariant differential operators.
status—partial
modifiedU(g) as convolution algebra of distributions at identity3f04cc3998ee
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No convolution algebra of point-supported distributions on a Lie group in Mathlib.
status—not_formalized
modifiedWeyl algebra from Heisenberg Lie algebra3fc258dd1728
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the Weyl algebra nor the Heisenberg Lie algebra is defined in Mathlib.
status—not_formalized
modifiedU(g) is a filtered quadratic algebra8b8db32a81d8
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`QuadraticAlgebra` exists but no filtration or quadratic-algebra structure is put on `UniversalEnvelopingAlgebra`.
status—not_formalized
addedU(g) inherits Hopf algebra structure from tensor algebra02cbcbe8fe13
modifiedGelfand–Naimark for commutative Hopf algebrasfa519f748cbe
FieldFrom #1650To #2471
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Gelfand–Naimark theorem for commutative Hopf algebras exists in Mathlib (grep for `GelfandNaimark` returns no hits).
status—not_formalized