Revision #1885 → #2734 · back to history
modifiedPoisson manifolde169d97a8327
| Field | From #1885 | To #2734 |
|---|
| note | Mathlib has no Poisson manifolds; Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean explicitly notes Poisson algebras are 'not yet defined'. | No Poisson manifold structure exists in Mathlib; Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean explicitly comments that Poisson algebras are 'not yet defined'. |
modifiedPoisson structure (informal)02c9eb92a4d9
| Field | From #1885 | To #2734 |
|---|
| note | No Poisson structure/bracket on smooth manifolds is defined in Mathlib. | Grep for 'Poisson' in Mathlib returns only Poisson summation, distribution, and integral files — no Poisson structure on smooth manifolds. |
modifiedPhase space of a free particled9952f682c09
| Field | From #1885 | To #2734 |
|---|
| note | Classical mechanics phase spaces are not formalized in Mathlib. | Classical mechanics phase spaces are not modelled in Mathlib. |
modifiedPhase space as cotangent bundle3b68a694d8c2
| Field | From #1885 | To #2734 |
|---|
| note | Cotangent bundle of a smooth manifold is not defined in Mathlib. | No smooth cotangent bundle exists in Mathlib — 'cotangent' occurrences are all algebraic (Kähler differentials). |
modifiedDarboux theorem (symplectic)b6fb61556d4e
| Field | From #1885 | To #2734 |
|---|
| note | Mathlib's `Darboux` file concerns the IVT for derivatives; the symplectic Darboux theorem is absent. | Mathlib's 'Darboux' file is the IVT for derivatives; symplectic Darboux is absent (no symplectic manifolds). |
modifiedQuotient of symplectic manifold by symplectomorphisms99f93d40b2ef
| Field | From #1885 | To #2734 |
|---|
| note | Neither symplectic manifolds nor symplectomorphism quotients exist in Mathlib. | Neither symplectic manifolds nor symplectomorphisms appear in Mathlib. |
modifiedPoisson's theorem on integrals of motionc1af367be7e9
| Field | From #1885 | To #2734 |
|---|
| note | No formalization of Poisson brackets or integrals of motion in Mathlib. | No Poisson bracket on smooth functions in Mathlib, so no theorem about integrals of motion. |
modifiedBracket of functions vs. bracket of Hamiltonian vector fields (Jacobi)227767d51f01
| Field | From #1885 | To #2734 |
|---|
| note | Hamiltonian vector fields and the Poisson-to-Lie bracket morphism are not in Mathlib. | No Hamiltonian vector fields in Mathlib (grep for 'Hamiltonian' returns only the graph-theoretic file). |
modifiedPoisson bracket (formal)4277c9fae846
| Field | From #1885 | To #2734 |
|---|
| note | Mathlib has no Poisson bracket on C^∞(M). | No Poisson bracket on C^∞(M) in Mathlib. |
modifiedHamiltonian vector field96bab19b348c
| Field | From #1885 | To #2734 |
|---|
| note | Hamiltonian vector fields are not defined in Mathlib. | No definition of Hamiltonian vector field in Mathlib. |
modifiedLocal coordinate expression of Poisson bracket195236647bda
| Field | From #1885 | To #2734 |
|---|
| note | Coordinate expression depends on absent Poisson bracket infrastructure. | Depends on the absent Poisson bracket definition. |
modifiedPoisson bivector5c5585fa27f2
| Field | From #1885 | To #2734 |
|---|
| note | No bivector field on smooth manifolds defined in Mathlib. | Grep for 'bivector' returns only Clifford-algebra bivector files — no smooth bivector fields. |
modifiedLocal coordinate expression of Poisson bivector481d3db44c1d
| Field | From #1885 | To #2734 |
|---|
| note | Depends on absent Poisson bivector / smooth tensor field machinery. | No smooth bivector-field infrastructure in Mathlib. |
modifiedEquivalence of bracket and bivector definitions72538d383043
| Field | From #1885 | To #2734 |
|---|
| note | Neither side of this equivalence is formalized. | Neither the bracket nor the bivector side is formalized. |
modifiedAlmost Poisson structure19ccf95b70da
| Field | From #1885 | To #2734 |
|---|
| note | Almost Poisson structures are not defined in Mathlib. | No almost-Poisson structures in Mathlib. |
modifiedEquivalent integrability conditions for almost Poissonc00804fd8617
| Field | From #1885 | To #2734 |
|---|
| note | Schouten bracket / Jacobi integrability conditions are not in Mathlib. | No Schouten–Nijenhuis bracket or Jacobi integrability formalism in Mathlib. |
modifiedSymplectic leaves2b0caa73cf11
| Field | From #1885 | To #2734 |
|---|
| note | Symplectic leaves of a Poisson manifold are not formalized. | Symplectic leaves of a Poisson manifold are not defined in Mathlib. |
modifiedRank of a Poisson structure at a point94624dd3de0b
| Field | From #1885 | To #2734 |
|---|
| note | Requires Poisson bivector, which Mathlib lacks. | Requires the absent Poisson bivector. |
modifiedRegular Poisson manifolds admit a foliation by symplectic leaves1bd76f518a3e
| Field | From #1885 | To #2734 |
|---|
| note | Mathlib has no general foliation theory or Poisson structures. | Grep for 'foliation' returns only the Analysis/Calculus/Implicit file (unrelated); no smooth foliation theory. |
modifiedIntegral submanifold and leaves of Poisson distribution666366f20992
| Field | From #1885 | To #2734 |
|---|
| note | Integral submanifolds for singular distributions are not in Mathlib. | No integral submanifolds for singular distributions in Mathlib. |
modifiedNatural symplectic form on each leaf75b8d992f0aa
| Field | From #1885 | To #2734 |
|---|
| note | Symplectic forms on leaves require absent infrastructure. | Requires the absent symplectic-form-on-manifold infrastructure. |
modifiedTrivial Poisson structure342e53dc0507
| Field | From #1885 | To #2734 |
|---|
| note | Even the zero Poisson structure has no place to live in Mathlib. | There is no Poisson-structure type in Mathlib for the zero bivector to inhabit. |
modifiedNondegenerate Poisson bivectors correspond to symplectic manifolds186a37733bf5
| Field | From #1885 | To #2734 |
|---|
| note | Neither side of this equivalence exists in Mathlib. | Neither side of the equivalence exists in Mathlib. |
modifiedLinear Poisson structure57e6644dacc1
| Field | From #1885 | To #2734 |
|---|
| note | Linear Poisson structures on vector spaces are not formalized. | No linear Poisson structures on vector spaces in Mathlib. |
modifiedLinear Poisson structures correspond to Lie algebras (KKS bracket)647fa9226bc5
| Field | From #1885 | To #2734 |
|---|
| note | Kirillov-Kostant-Souriau bracket is not formalized; Mathlib has Lie algebras but no Poisson structure on their duals. | Mathlib formalizes Lie algebras but has no Poisson structure on their duals (no KKS bracket). |
modifiedSymplectic leaves of Lie-Poisson are coadjoint orbits82ee5d6f0e8f
| Field | From #1885 | To #2734 |
|---|
| note | Coadjoint orbits are not formalized in Mathlib. | Coadjoint orbits and Lie–Poisson leaves are not formalized in Mathlib. |
modifiedFibrewise linear Poisson structure19539c4df4d4
| Field | From #1885 | To #2734 |
|---|
| note | Fibrewise linear Poisson structures on vector bundles are not formalized. | No fibrewise-linear Poisson structures on vector bundles in Mathlib. |
modifiedFibrewise linear Poisson structures correspond to Lie algebroids5c5c877e4a50
| Field | From #1885 | To #2734 |
|---|
| note | Lie algebroids are not defined in Mathlib. | Only algebraic Lie–Rinehart algebras exist in Mathlib (Mathlib/Algebra/LieRinehartAlgebra/Defs.lean); no geometric Lie algebroids and no Poisson correspondence. |
modifiedSymplectic leaves via integrating groupoidc0773e47b9ce
| Field | From #1885 | To #2734 |
|---|
| note | Lie groupoids and their integration are absent from Mathlib. | Grep for 'Lie groupoid' returns nothing in Mathlib. |
modifiedConstant bivector field is Poissonce6294a81a26
| Field | From #1885 | To #2734 |
|---|
| note | Requires Poisson bivector machinery that does not exist in Mathlib. | Requires absent Poisson bivector machinery. |
modifiedBivector field on 2-manifold is Poissonb68fa0f96ee5
| Field | From #1885 | To #2734 |
|---|
| note | Not formalized; no smooth bivector fields in Mathlib. | No smooth bivector fields in Mathlib. |
modifiedRescaled Poisson bivector in dimension 3a43d83a1cfb5
| Field | From #1885 | To #2734 |
|---|
| note | Not formalized. | Not formalized — depends on absent Poisson bivector. |
modifiedCartesian product of Poisson manifolds927d7ab4ad44
| Field | From #1885 | To #2734 |
|---|
| note | Product of Poisson manifolds is not formalized. | Product of Poisson manifolds is not defined in Mathlib. |
modifiedRegular Poisson structure from foliation and foliated two-formd61ff7586ad7
| Field | From #1885 | To #2734 |
|---|
| note | Neither foliations of smooth manifolds nor foliated forms are in Mathlib. | Foliations of smooth manifolds and foliated forms are absent from Mathlib. |
modifiedQuotient Poisson structure from group action86801ff88578
| Field | From #1885 | To #2734 |
|---|
| note | Not formalized. | Not formalized — no Poisson manifolds to quotient. |
modifiedPoisson cohomology groups9318389a21c4
| Field | From #1885 | To #2734 |
|---|
| note | Poisson cohomology is not defined in Mathlib. | No Poisson cohomology in Mathlib. |
modifiedMorphism from de Rham to Poisson cohomologye5d61d75293f
| Field | From #1885 | To #2734 |
|---|
| note | Neither smooth de Rham cohomology nor Poisson cohomology exist in Mathlib. | Neither smooth de Rham nor Poisson cohomology are in Mathlib. |
modifiedModular vector fielde3cda4eacb6f
| Field | From #1885 | To #2734 |
|---|
| note | Modular vector fields are not defined in Mathlib. | Not defined in Mathlib. |
modifiedModular class is well-defined50dd29e5b12d
| Field | From #1885 | To #2734 |
|---|
| note | Modular class of Poisson manifolds is not formalized. | Not formalized. |
modifiedSymplectic structures are unimodular4859e71e2f44
| Field | From #1885 | To #2734 |
|---|
| note | Not formalized; symplectic manifolds absent. | Not formalized — no symplectic manifolds. |
modifiedPoisson homology ≅ Poisson cohomology for unimodular casef9c5c4277f5b
| Field | From #1885 | To #2734 |
|---|
| note | Poisson (co)homology theory is not in Mathlib. | No Poisson (co)homology theory in Mathlib. |
modifiedPoisson map from Lie algebra homomorphism74f13884159b
| Field | From #1885 | To #2734 |
|---|
| note | Mathlib has Lie algebra morphisms but no Lie-Poisson structure to map between. | Mathlib has Lie algebra morphisms but no Lie–Poisson structure to map between. |
modifiedPoisson map from Lie algebroid morphism1f54d338da35
| Field | From #1885 | To #2734 |
|---|
| note | Lie algebroids are absent from Mathlib. | Geometric Lie algebroids are absent from Mathlib. |
modifiedCotangent Lie algebroid of a Poisson manifold7e80bc0330d3
| Field | From #1885 | To #2734 |
|---|
| note | Cotangent Lie algebroid is not formalized. | Cotangent Lie algebroid is not formalized in Mathlib. |
modifiedSymplectic groupoidf4bb7d11b218
| Field | From #1885 | To #2734 |
|---|
| note | Lie groupoids and symplectic groupoids are absent from Mathlib. | Neither Lie groupoids nor symplectic groupoids exist in Mathlib. |
modifiedSymplectic realisationad92abaf49c1
| Field | From #1885 | To #2734 |
|---|
| note | Symplectic realisations are not in Mathlib. | Not in Mathlib. |
modifiedMoyal-Weyl product on constant Poisson spacea572a763a54f
| Field | From #1885 | To #2734 |
|---|
| note | Moyal-Weyl product is not formalized. | Moyal–Weyl product is not formalized. |
modifiedIsotropy Lie algebra at a pointf6983fb69155
| Field | From #1885 | To #2734 |
|---|
| note | Isotropy Lie algebra of a Poisson zero is not defined in Mathlib. | Not defined in Mathlib. |
modifiedConn's linearisation theoremce4009b17257
| Field | From #1885 | To #2734 |
|---|
| note | Conn's linearisation theorem is not formalized in Mathlib. | Conn's linearisation theorem is not in Mathlib. |
modifiedPoisson-Lie group3c4c6dd6ca92
| Field | From #1885 | To #2734 |
|---|
| note | Poisson-Lie groups are not defined in Mathlib. | Poisson–Lie groups are not defined in Mathlib. |
addedPoisson algebra structure on smooth functions1a653b23728a
addedSchouten–Nijenhuis bracket7873666ed16b
addedDirac structure via graph of Poisson bivectorbe61df7928e0
addedCasimir functionsbff1227caa04
addedPoisson vector fields modulo Hamiltonianeba293175588
addedDivergence of a vector field with respect to a volume form168c46bbc3c0
addedPoisson-diffeomorphism definition724be0d1cd94
addedPoisson cohomology equals Lie algebroid cohomology of cotangent algebroidb95e33aee88e
addedLocal existence of symplectic realisations60789f6e8259
addedKontsevich formality quasi-isomorphism682a5b4afa7d