feat(SpaceAndTime): add Galilean group API#1245
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
| rw [map_smul] | ||
|
|
||
| /-- The identity Galilean transformation. -/ | ||
| def identity : GalileanGroup d := |
There was a problem hiding this comment.
I would not define this explicitly, nor inv and mil, I would instead include them directly in the instance
There was a problem hiding this comment.
Or define them in parts using instances of One, Mul etc.
| namespace GalileanGroup | ||
|
|
||
| /-- A spatial vector viewed as a displacement of the chosen origin in `Space d`. -/ | ||
| noncomputable def vectorToSpace (v : EuclideanSpace ℝ (Fin d)) : Space d := |
There was a problem hiding this comment.
Should go in the corresponding Space file if indeed needed.
| @[simp] lemma one_rotation : (1 : GalileanGroup d).rotation = 1 := rfl | ||
| @[simp] lemma one_velocity : (1 : GalileanGroup d).velocity = 0 := rfl | ||
| @[simp] lemma one_spaceTranslation : (1 : GalileanGroup d).spaceTranslation = 0 := rfl | ||
| @[simp] lemma one_timeTranslation : (1 : GalileanGroup d).timeTranslation = 0 := rfl |
There was a problem hiding this comment.
If you use the instances One you can put these lemmas below that (giving a nice structure to the file). I would also put new lines between lemmas like this.
jstoobysmith
added
the
awaiting-author
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
|
@jstoobysmith Sure, I think I integrated those into my updates, if not just let me know what you'd like to see. Thanks! |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
This looks great to me, many thanks for making the changes. I've approved, will check it works with the bump, and if so merge.
jstoobysmith
added
the
ready-to-merge
2 participants
Addresses #911.
Summary
This adds the algebraic Galilean-group API in arbitrary spatial dimension.
Changes
GalileanGroup dwith orthogonal, boost-velocity, spatial-translation, and time-translation fieldsGroup (GalileanGroup d)instanceTime × Space das aMulActionRelated: #1116 added a first-step datatype and coordinate action. This PR takes a different route by adding the composition law, inverse,
MulActioninstance, and subgroup inclusions requested for #911.The Lie-group instance is not included here. Physlib does not yet have the needed Lie-group or charted-space layer for
Matrix.orthogonalGrouporEuclideanGroup, so that part should be a follow-up once the manifold API is in place.Verification
lake build Physlib.SpaceAndTime.GalileanGroup.Basiclake build Physliblake env lean /tmp/physlib-911-probe/GalileanProbe.lean#lintonPhyslib/SpaceAndTime/GalileanGroup/Basic.leanlake exe lint_all --fast(build/import/tag/sorry checks pass; the repo-wide style phase still reports unrelated existing style issues)./scripts/lint-style.py Physlib/SpaceAndTime/GalileanGroup/Basic.leangit diff --checksorry,admit, oraxiomin touched files