The time manifold

In this module we define the type TimeMan, corresponding to the time manifold, without any additional structures except an orientation, such as a choice of metric or origin. I.e. it is a manifold diffeomorphic to ℝ with no additional structure.

If you are looking for a more standard version of time see the type Time.

TimeMan is sometimes called topological time, due to the absence of a metric, and its use in topological field theories.

Implementation details

The manifold TimeMan is defined via the type ℝ, and thus inherits a given choice of map TimeMan.val : TimeMan → ℝ, which can be extended to a homeomorphism or a diffeomorphism. When using TimeMan.val, one should be aware that using it does constitute a choice being made.

structure TimeMan : Type

The type TimeMan represents the time manifold. Mathematically TimeMan is a manifold diffeomorphic to ℝ with an orientation but no additional structure.

• val : ℝ

  The choice of a map from TimeMan to ℝ.

The topology on TimeMan.

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

instance TimeMan.instTopologicalSpace : TopologicalSpace TimeMan

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

Equations

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

theorem TimeMan.val_surjective : Function.Surjective val

@[simp]

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

theorem TimeMan.val_inducing : Topology.IsInducing val

theorem TimeMan.val_injective : Function.Injective val

theorem TimeMan.val_isOpenEmbedding : Topology.IsOpenEmbedding val

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

def TimeMan.valHomeomorphism : TimeMan ≃ₜ ℝ

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

Equations

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

The manifold structure on TimeMan

instance TimeMan.instChartedSpaceReal : ChartedSpace ℝ TimeMan

The structure of a charted space on TimeMan

Equations

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

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

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

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

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

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

Equations

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

The orientation on TimeMan

instance TimeMan.instLE : LE TimeMan

The instance of an orientation on TimeMan.

Equations

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