refactor(Time): add manifold structure and remove TimeTransMan

Physlib.lean

@@ -529,7 +529,6 @@ public import Physlib.SpaceAndTime.Time.Derivatives
 public import Physlib.SpaceAndTime.Time.InnerProductSpace
 public import Physlib.SpaceAndTime.Time.MatrixDerivatives
 public import Physlib.SpaceAndTime.Time.TimeMan
-public import Physlib.SpaceAndTime.Time.TimeTransMan
 public import Physlib.SpaceAndTime.Time.TimeUnit
 public import Physlib.SpaceAndTime.TimeAndSpace.Basic
 public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist

Physlib/SpaceAndTime/Time/API-map.yaml

@@ -9,9 +9,8 @@ Overview: |
     time, and no instant is canonically zero. Choosing the implicit origin `Time.mk 0`
     gives the version of time most often used in non-relativistic physics,
     forming a 1d real inner-product space. The API also contains the time
-    derivative `∂ₜ` of functions on `Time`, and the related types `TimeMan`,
-    `TimeTransMan` and `TimeUnit`, versions of time with fewer choices made,
-    related to `Time` via a choice of units or origin.
+    derivative `∂ₜ` of functions on `Time`, the oriented time manifold `TimeMan`,
+    and the type `TimeUnit` of choices of time unit.
 
 ParentAPIs:
   - "Space (Physlib/SpaceAndTime/Space)"
@@ -65,10 +64,6 @@ Requirements:
     done: true
     location: "Physlib/SpaceAndTime/Time/TimeUnit.lean (TimeUnit, HDiv TimeUnit TimeUnit ℝ≥0, scale, seconds, hours_div_seconds)"
 
-  - description: "The API contains the time manifold `TimeTransMan` with a transitive action of `ℝ`, an orientation, unit-dependent differences and translations (`diff`, `addTime`, `neg`), and the homeomorphism `toTime` to `Time` given a choice of origin and unit."
-    done: true
-    location: "Physlib/SpaceAndTime/Time/TimeTransMan.lean (TimeTransMan, AddAction ℝ TimeTransMan, diff, addTime, neg, toTime)"
-
   - description: "The API shall contain an action of the translation group on `Time`."
     done: false
     location: N/A
@@ -80,11 +75,3 @@ Requirements:
   - description: "The API shall contain derivatives of distributions from `Time` to manifolds."
     done: false
     location: N/A
-
-  - description: "The API shall show that the homeomorphism `toTime` from `TimeTransMan` to `Time` is a diffeomorphism."
-    done: false
-    location: N/A
-
-  - description: "The API shall show that translationally-invariant metrics on `TimeTransMan` are in one-to-one correspondence with the positive reals (choices of `TimeUnit`)."
-    done: false
-    location: N/A

Physlib/SpaceAndTime/Time/Basic.lean

@@ -5,7 +5,9 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Mathlib.Basic.Real.Basic
+public import Mathlib.Analysis.Normed.Group.AddTorsor
+public import Mathlib.Analysis.Normed.Group.Real
+public import Mathlib.Geometry.Manifold.IsManifold.Basic
 public import Mathlib.LinearAlgebra.AffineSpace.Defs
 /-!
 # Time
@@ -18,9 +20,12 @@ The field `Time.val` is an implementation coordinate, not a frame-relative time
 coordinate. A reference frame chooses its own time origin. Import
 `Physlib.SpaceAndTime.Time.InnerProductSpace` to use the inner product space structure with the
 implicit origin `Time.mk 0`, including addition of instants, norms, and derivatives.
+
 -/
 
-@[expose] public section
+@[expose] public noncomputable section
+
+open scoped Manifold ContDiff
 
 /-!
 # A. The `Time` type
@@ -60,4 +65,25 @@ instance : AddTorsor ℝ Time where
   vsub_vadd' t₁ t₂ := by ext; simp
   vadd_vsub' dt t := by simp
 
+/-!
+# C. The metric and manifold structure
+-/
+
+instance : MetricSpace Time := metricSpaceOfNormedAddCommGroupOfAddTorsor ℝ Time
+
+instance : NormedAddTorsor ℝ Time where
+  dist_eq_norm' _ _ := rfl
+
+instance : ChartedSpace ℝ Time :=
+  let chartAt t := (Homeomorph.vaddConst t).symm.toOpenPartialHomeomorph
+  { chartAt,
+    atlas := Set.range chartAt,
+    mem_chart_source := Set.mem_univ,
+    chart_mem_atlas := by simp }
+
+instance : IsManifold 𝓘(ℝ, ℝ) ω Time := by
+  apply isManifold_of_contDiffOn
+  rintro _ _ ⟨_, rfl⟩ ⟨_, rfl⟩
+  exact contDiff_id.add contDiff_const |>.sub contDiff_const |>.contDiffOn
+
 end Time

Physlib/SpaceAndTime/Time/InnerProductSpace.lean

@@ -32,10 +32,6 @@ the angular frequency `ω` are consistent.
 
 With this choice, `Time` becomes a 1d vector space over `ℝ` with an inner product.
 
-Within other modules e.g. `TimeMan` and `TimeTransMan`, we define
-versions of time with less choices made, and relate them to `Time` via a choice of units
-or origin.
-
 ## ii. Key results
 
 - `toRealCLE` : The continuous linear equivalence from `Time` to `ℝ`.
@@ -254,31 +250,19 @@ instance : Norm Time where
 lemma norm_eq_val (t : Time) :
     ‖t‖ = ‖t.val‖ := rfl
 
-instance : Dist Time where
-  dist t1 t2 := ‖t1 - t2‖
-
 lemma dist_eq_val (t1 t2 : Time) :
     dist t1 t2 = ‖t1.val - t2.val‖ := rfl
 
 lemma dist_eq_real_dist (t1 t2 : Time) :
     dist t1 t2 = dist t1.val t2.val := by rfl
 
 instance : SeminormedAddCommGroup Time where
-  dist_self t := by simp [dist_eq_real_dist]
-  dist_comm t1 t2 := by simp [dist_eq_real_dist, dist_comm]
-  dist_triangle := by simp [dist_eq_real_dist, dist_triangle]
   dist_eq t1 t2 := by
     simp [dist_eq_val, norm_eq_val]
     rw [abs_eq_iff_mul_self_eq]
     ring
 
 instance : NormedAddCommGroup Time where
-  eq_of_dist_eq_zero := by
-    intro a b h
-    simp [dist, norm] at h
-    ext
-    rw [sub_eq_zero] at h
-    exact h
   dist_eq t1 t2 := by
     simp [dist_eq_val, norm_eq_val]
     rw [abs_eq_iff_mul_self_eq]