Skip to content

feat(PhyslibAlpha): the mass cocycle of the Galilean group (Souriau) #1687

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
KevorkianPhilippe wants to merge 9 commits into
base: master
Choose a base branch
from
Open

feat(PhyslibAlpha): the mass cocycle of the Galilean group (Souriau) #1687

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
c7d4f8b
feat(PhyslibAlpha/ClassicalMechanics): the mass as a cohomology class…
Sep 24, 2026
1a8ee8c
feat(PhyslibAlpha/ClassicalMechanics): the mass cocycle of the Galile…
Sep 24, 2026
67c3d7f
feat(PhyslibAlpha/ClassicalMechanics): state the mass cocycle results…
Sep 24, 2026
d45d65c
docs(PhyslibAlpha/ClassicalMechanics): GalileanMass docstrings after …
Sep 24, 2026
c6b5074
Merge branch 'galilee-1' into galilee-2
Sep 24, 2026
fb5250d
Merge remote-tracking branch 'origin/master' into galilee-1
Sep 25, 2026
ae21c03
refactor(PhyslibAlpha/ClassicalMechanics): move the moment map files …
Sep 25, 2026
f691590
Merge branch 'galilee-1' into galilee-2
Sep 25, 2026
1e6c267
refactor(PhyslibAlpha/ClassicalMechanics): move GalileanMassCocycle.l…
Sep 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions PhyslibAlpha.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,10 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell
public import PhyslibAlpha.ClassicalMechanics.MomentMap
public import PhyslibAlpha.ClassicalMechanics.MomentMapCohomology
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology
public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass
public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMassCocycle
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism
public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem
Expand Down
0 ...ibAlpha/ClassicalMechanics/MomentMap.lean → ...a/ClassicalMechanics/MomentMap/Basic.lean
View file
Open in desktop
File renamed without changes.
4 changes: 2 additions & 2 deletions ...assicalMechanics/MomentMapCohomology.lean → ...ssicalMechanics/MomentMap/Cohomology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Philippe Kevorkian
-/
module

public import PhyslibAlpha.ClassicalMechanics.MomentMap
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic
public import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-!

Expand All @@ -25,7 +25,7 @@ group `Sp(E) ⋉ E` of a real symplectic vector space `E`, acting by `x ↦ B x
`moment` of (11.7): the defect `θ(a)` does not depend on `x` and equals `μ(C)` (a computation here,
not a consequence of connectedness), `θ` is a 1-cocycle of the coadjoint action, its derivative
at the identity along a curve is the Lie algebra cocycle of
`PhyslibAlpha.ClassicalMechanics.MomentMap`, and its cohomology class is not zero. It does NOT
`PhyslibAlpha.ClassicalMechanics.MomentMap.Basic`, and its cohomology class is not zero. It does NOT
prove (11.18), (11.20) or (11.21): by (11.21) the non-zero class means that no potential of `σ` is
invariant under this group, but that implication is Souriau's and is not formalised here.

Expand Down
Loading
Loading