Revision #3102 → #3588 · back to history
modifiedUniversal enveloping algebra (informal)e27d99e4ed7f
| Field | From #3102 | To #3588 |
|---|
| note | The universal enveloping algebra as an R-algebra is defined in Mathlib.Algebra.Lie.UniversalEnveloping. | The universal enveloping algebra as an R-algebra is defined in Mathlib.Algebra.Lie.UniversalEnveloping (verified via decl_exists). |
addedVerma modules as quotients of U(g)10408fbff5ad
modifiedU(g) via generators and relations3f5c39a64be6
| Field | From #3102 | To #3588 |
|---|
| 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. | Mathlib builds U(g) as the tensor algebra quotiented by the Lie-compatibility relation `UniversalEnvelopingAlgebra.Rel.lie_compat`, matching this generators/relations presentation. |
modifiedPBW basis spans U(g) (preview)5dad205518dd
| Field | From #3102 | To #3588 |
|---|
| note | No Poincaré–Birkhoff–Witt basis result appears in Mathlib (grep and loogle for `Birkhoff`/`PBW` return no hits). | No Poincaré–Birkhoff–Witt basis result appears in Mathlib (grep for `PBW` returns no hits; `Birkhoff` matches unrelated results). |
modifiedFormal definition of U(g) as a quotient063cf150569d
| Field | From #3102 | To #3588 |
|---|
| note | `UniversalEnvelopingAlgebra R L` is literally the quotient of the tensor algebra by the ring congruence generated by `Rel.lie_compat`. | `UniversalEnvelopingAlgebra R L` is literally the `RingQuot` of the tensor algebra by the ring congruence generated by `Rel.lie_compat`. |
addedLifted bracket is bilinear, skew-symmetric, and Jacobi56a17dc37ab3
modifiedU(g) as tensor algebra modulo two-sided ideal0ad887b2c82e
| Field | From #3102 | To #3588 |
|---|
| mathlib.match_kind | close | exact |
| note | This equivalent presentation as T(g)/I with I generated by x⊗y − y⊗x − [x,y] matches the `RingQuot` of `UniversalEnvelopingAlgebra.Rel` in Mathlib. | The equivalent presentation as T(g)/I with I generated by x⊗y − y⊗x − [x,y] matches the `RingQuot` of `UniversalEnvelopingAlgebra.Rel.lie_compat`. |
modifiedU for Lie superalgebras0ee6974adba8
| Field | From #3102 | To #3588 |
|---|
| note | Mathlib does not have Lie superalgebras (grep for `LieSuperalgebra` returns no files). | Mathlib does not have Lie superalgebras (grep for `LieSuperalgebra`/`LieSuper` returns no files). |
addedGeneralization to Malcev, Bol, and left alternative algebras1d210dd4e6ed
modifiedUniversal property of U(g)02ac0cc12702
| Field | From #3102 | To #3588 |
|---|
| 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`. | `UniversalEnvelopingAlgebra.lift` gives the bijection between Lie-algebra maps `L →ₗ⁅R⁆ A` and algebra maps `U(L) →ₐ[R] A`, with uniqueness via `hom_ext`. |
addedEvery g-representation extends uniquely to U(g)5d82b6cde160
addedFree Lie algebra basis via Hall/Lyndon wordseade2ddce52c
modifiedJordan algebra construction yields exterior algebra71de074ca3db
| Field | From #3102 | To #3588 |
|---|
| note | Mathlib has Jordan algebras and exterior algebras separately but no PBW-style relation between them. | Mathlib has Jordan algebras (`Mathlib.Algebra.Jordan.Basic`) and exterior algebras separately but no PBW-style relation between them. |
addedBerezin formula from Baker–Campbell–Hausdorff6033ad38d3d9
modifiedHeisenberg algebra and Weyl algebra (Moyal product)00f749f145d0
| Field | From #3102 | To #3588 |
|---|
| note | Neither the Heisenberg Lie algebra nor the Weyl algebra is defined in Mathlib. | Neither the Heisenberg Lie algebra nor the Weyl algebra is defined in Mathlib (grep for `Heisenberg`/`WeylAlgebra` returns no hits). |
modifiedU of free Lie algebra is free associative algebra77c43eddbf40
| Field | From #3102 | To #3588 |
|---|
| note | `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra` gives the algebra equivalence `U(FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X`. | `FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra` gives the algebra equivalence `U(FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X` (verified via decl_exists). |
modifiedCasimir operators as basis of center15f9ce1f5b42
| Field | From #3102 | To #3588 |
|---|
| note | No `Casimir` declarations in Mathlib (grep and loogle both return zero hits). | No `Casimir` declarations in Mathlib (grep returns zero hits). |
modifiedHarish-Chandra isomorphism for center of U(g)2c5921d9ed3a
| Field | From #3102 | To #3588 |
|---|
| note | No Harish-Chandra isomorphism in Mathlib (grep returns no hits). | No Harish-Chandra isomorphism in Mathlib (grep for `HarishChandra`/`Harish-Chandra` returns no hits). |
modifiedU(g) inherits Hopf algebra structure from tensor algebra02cbcbe8fe13
| Field | From #3102 | To #3588 |
|---|
| note | `HopfAlgebra` is defined in Mathlib but no `HopfAlgebra` instance is placed on `UniversalEnvelopingAlgebra`. | `HopfAlgebra` is defined in Mathlib but no `HopfAlgebra` instance is placed on `UniversalEnvelopingAlgebra` (grep for `UniversalEnveloping.*Hopf` returns no hits). |
modifiedGelfand–Naimark for commutative Hopf algebrasfa519f748cbe
| Field | From #3102 | To #3588 |
|---|
| note | No Gelfand–Naimark theorem for commutative Hopf algebras exists in Mathlib (grep for `GelfandNaimark` returns no hits). | No Gelfand–Naimark theorem for commutative Hopf algebras exists in Mathlib (only `GelfandNaimarkSegal` on C*-algebras is present). |