API: TimeAndSpace

[jstoobysmith]

Details

Key data structure

This is Euclidean SpaceTime. The key data structure should be a type TimeAndSpace d which is an abbreviation of Time x Space d.

• is defined.

Need

This API is needed throughout PhysLean, for example in Euclidean field theory, but also areas such as electromagnetism and classical mechanics.

Requirements

• The API shall contain isometry projections from TimeAndSpace d to Time and `Space.
• The API shall contain an action of the Euclidean group on TimeAndSpace d.
• The API shall contain an action of the Euclidean group on Schwartz maps with targets TimeAndSpace d.

Corresponding file system

The corresponding file system is:
https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/SpaceAndTime/TimeAndSpace

References

Specifics of the material in this section appears here:

• https://github.com/mrdouglasny/OSforGFF/tree/main

Parent APIs

#854 #855 #940