The time manifold with a transitive action of ℝ

In this module we define the type TimeTransMan. This type physically corresponds to the manifold of time (diffeomorphic to ℝ) with the following additional structure:

1. a transitive action of ℝ,
2. a choice of orientation.

The manifold TimeTransMan is not equipped with a translationally-invariant metric. Such metrics are in one-to-one correspondence (to be shown) with positive reals, and as such we define the type TimeUnit (equivalent to the positive reals) to represent the choice of metric on TimeTransMan. This is defined in a different module.

From the point of view of physics, this choice of metric corresponds to a choice of units, hence the name, and we will use the phrase 'units of time' interchangeably 'choice of metric'.

Given a x : TimeUnit, and the structure above, we can define the following operations on TimeTransMan:

• diff x t1 t2, for t1 t2 : TimeTransMan gives the signed difference between two points in time in the units x.
• addTime x r t, for r : ℝ and t : TimeTransMan, gives the point in TimeTransMan that separated from t, by r in the unit x. For example, if x is the unit of seconds, then addTime x 1 t gives the point in TimeTransMan that is one second after t.
• neg zero t, for a given zero : TimeTransMan, gives the point in TimeTransMan that is the same distance away from zero as t but in the opposite direction. This is defined using a choice of units, but is independent of the choice.

Recall that the type Time corresponds to the manifold of time with a given (but arbitrary) choice of units and origin (and therefore has a structure of a module over ℝ). Here we define the homeomorphism:

• toTime zero x from TimeTransMan to Time where zero : TimeTransMan is the choice of origin and x : TimeUnit is the choice of units. This map is a diffeomorphism (to be shown).

structure TimeTransMan : Type

The type TimeTransMan represents the time manifold with an orientation and a transitive action of the reals.

• val : ℝ

  The choice of a map from TimeTransMan to ℝ.

theorem TimeTransMan.ext_of {t1 t2 : TimeTransMan} (h : t1.val = t2.val) : t1 = t2

theorem TimeTransMan.ext_of_iff {t1 t2 : TimeTransMan} : t1 = t2 ↔ t1.val = t2.val

The topology on TimeTransMan.

The topology on TimeTransMan is induced from the topology on ℝ, via the choice of map TimeTransMan.val.

instance TimeTransMan.instTopologicalSpace : TopologicalSpace TimeTransMan

The instance of a topological space on TimeTransMan induced by the map TimeTransMan.val.

Equations

• TimeTransMan.instTopologicalSpace = TopologicalSpace.induced TimeTransMan.val PseudoMetricSpace.toUniformSpace.toTopologicalSpace

theorem TimeTransMan.val_surjective : Function.Surjective val

@[simp]

theorem TimeTransMan.val_range : Set.range val = Set.univ

theorem TimeTransMan.val_inducing : Topology.IsInducing val

theorem TimeTransMan.val_injective : Function.Injective val

theorem TimeTransMan.val_isOpenEmbedding : Topology.IsOpenEmbedding val

theorem TimeTransMan.isOpen_iff {s : Set TimeTransMan} : IsOpen s ↔ IsOpen (val '' s)

def TimeTransMan.valHomeomorphism : TimeTransMan ≃ₜ ℝ

The choice of map Time.val from TimeTransMan to ℝ as a homeomorphism.

Equations

• One or more equations did not get rendered due to their size.

The manifold structure on TimeTransMan

instance TimeTransMan.instChartedSpaceReal : ChartedSpace ℝ TimeTransMan

The structure of a charted space on TimeTransMan

Equations

• One or more equations did not get rendered due to their size.

instance TimeTransMan.instIsManifoldRealModelWithCornersSelfTopWithTopENat : IsManifold (modelWithCornersSelf ℝ ℝ) ⊤ TimeTransMan

The structure of a manifold on TimeTransMan induced by the choice of map Time.val.

theorem TimeTransMan.val_contDiff : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) ⊤ val

noncomputable def TimeTransMan.valDiffeomorphism : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) TimeTransMan ℝ ⊤

The choice of map Time.val from TimeTransMan to ℝ as a diffeomorphism.

Equations

• TimeTransMan.valDiffeomorphism = { toEquiv := TimeTransMan.valHomeomorphism.toEquiv, contMDiff_toFun := TimeTransMan.val_contDiff, contMDiff_invFun := TimeTransMan.valDiffeomorphism._proof_1 }

The transitive group action on TimeTransMan

instance TimeTransMan.instVAddReal : VAdd ℝ TimeTransMan

Equations

• TimeTransMan.instVAddReal = { vadd := fun (p : ℝ) (t : TimeTransMan) => { val := p + t.val } }

@[simp]

theorem TimeTransMan.vadd_val (p : ℝ) (t : TimeTransMan) : (p +ᵥ t).val = p + t.val

instance TimeTransMan.instAddActionReal : AddAction ℝ TimeTransMan

Equations

• TimeTransMan.instAddActionReal = { toVAdd := TimeTransMan.instVAddReal, zero_vadd := TimeTransMan.instAddActionReal._proof_1, add_vadd := TimeTransMan.instAddActionReal._proof_2 }

A choice of orientation on TimeTransMan

instance TimeTransMan.instLE : LE TimeTransMan

Equations

• TimeTransMan.instLE = { le := fun (x y : TimeTransMan) => x.val ≤ y.val }

theorem TimeTransMan.le_def (t1 t2 : TimeTransMan) : t1 ≤ t2 ↔ t1.val ≤ t2.val

instance TimeTransMan.instNonempty : Nonempty TimeTransMan

Functions based on a choice of unit

noncomputable def TimeTransMan.dist (x : TimeUnit) (t1 t2 : TimeTransMan) : ℝ

The distance between two points in TimeTransMan in the units of x : TimeUnit.

Equations

• TimeTransMan.dist x t1 t2 = 1 / x.val * ‖t2.val - t1.val‖

Signed difference

noncomputable def TimeTransMan.diff (x : TimeUnit) (t2 t1 : TimeTransMan) : ℝ

The signed difference between two points in on the manifold TimeTransMan in the units of x : TimeUnit.

Equations

• TimeTransMan.diff x t2 t1 = if t1 ≤ t2 then TimeTransMan.dist x t1 t2 else -TimeTransMan.dist x t1 t2

theorem TimeTransMan.diff_eq_val (x : TimeUnit) (t1 t2 : TimeTransMan) : diff x t1 t2 = 1 / x.val * (t1.val - t2.val)

@[simp]

theorem TimeTransMan.diff_self (x : TimeUnit) (t : TimeTransMan) : diff x t t = 0

theorem TimeTransMan.diff_fst_injective (x : TimeUnit) (t : TimeTransMan) : Function.Injective fun (x_1 : TimeTransMan) => diff x x_1 t

theorem TimeTransMan.diff_fst_surjective (x : TimeUnit) (t : TimeTransMan) : Function.Surjective fun (x_1 : TimeTransMan) => diff x x_1 t

theorem TimeTransMan.diff_fst_bijective (x : TimeUnit) (t : TimeTransMan) : Function.Bijective fun (x_1 : TimeTransMan) => diff x x_1 t

Adding time

noncomputable def TimeTransMan.addTime (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : TimeTransMan

Given a time unit x : TimeUnit, addTime x r t, for a real ℝ and t : TimeTransMan, is the point in TimeTransMan separated from t by a difference of r in the units x. For example, if x corresponds to seconds addTime x 1 t is the time 1 second more then t.

Equations

• TimeTransMan.addTime x r t = Function.invFun (fun (x_1 : TimeTransMan) => TimeTransMan.diff x x_1 t) r

theorem TimeTransMan.addTime_eq_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : addTime x r t = { val := x.val * r + t.val }

theorem TimeTransMan.addTime_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) : (addTime x r t).val = x.val * r + t.val

Negation of time around a zero

noncomputable def TimeTransMan.negMetric (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : TimeTransMan

Given a zero and an x : TimeUnit, negMetric zero x t is the time the same distance away from zero as t in units x but in the opposite direction. This does actually depend on x, as a result see neg and neg_eq_negMetric.

Equations

• zero.negMetric x t = TimeTransMan.addTime x (TimeTransMan.diff x zero t) zero

noncomputable def TimeTransMan.neg (zero t : TimeTransMan) : TimeTransMan

Given a zero, neg zero t is the time the same distance away from zero as t in any units but in the opposite direction.

Equations

• zero.neg t = zero.negMetric default t

theorem TimeTransMan.neg_eq_negMetric (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : zero.neg t = zero.negMetric x t

The map from TimeTransMan to Time

noncomputable def TimeTransMan.toTime (zero : TimeTransMan) (x : TimeUnit) : TimeTransMan ≃ₜ Time

With a choice of zero zero : TimeTransMan and a choice of units x : TimeUnit, toTime is the homeomorphism between the type TimeTransMan and Time.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TimeTransMan.toTime_zero (zero : TimeTransMan) (x : TimeUnit) : (zero.toTime x) zero = 0

@[simp]

theorem TimeTransMan.toTime_symm_zero_add (zero : TimeTransMan) (x : TimeUnit) : (zero.toTime x).symm 0 = zero

theorem TimeTransMan.toTime_val (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : ((zero.toTime x) t).val = diff x t zero

theorem TimeTransMan.toTime_symm_val (zero : TimeTransMan) (x : TimeUnit) (r : Time) : (zero.toTime x).symm r = addTime x r.val zero

@[simp]

theorem TimeTransMan.toTime_addTime (zero : TimeTransMan) (x : TimeUnit) (r : ℝ) (τ : TimeTransMan) : (zero.toTime x) (addTime x r τ) = { val := r } + (zero.toTime x) τ

theorem TimeTransMan.toTime_symm_add (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) : (zero.toTime x).symm (t1 + t2) = addTime x (diff x ((zero.toTime x).symm t1) zero) ((zero.toTime x).symm t2)

theorem TimeTransMan.toTime_symm_add' (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) : (zero.toTime x).symm (t1 + t2) = addTime x (diff x ((zero.toTime x).symm t2) zero) ((zero.toTime x).symm t1)

theorem TimeTransMan.diff_eq_toTime_sub (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : TimeTransMan) : diff x t2 t1 = ((zero.toTime x) t2).val - ((zero.toTime x) t1).val

theorem TimeTransMan.toTime_neg (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) : (zero.toTime x) (zero.neg t) = -(zero.toTime x) t

theorem TimeTransMan.toTime_symm_neg (zero : TimeTransMan) (x : TimeUnit) (t : Time) : (zero.toTime x).symm (-t) = zero.neg ((zero.toTime x).symm t)

theorem TimeTransMan.toTime_symm_sub (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) : (zero.toTime x).symm (t1 - t2) = addTime x (diff x zero ((zero.toTime x).symm t2)) ((zero.toTime x).symm t1)