Physlib

Physlib.SpaceAndTime.Time.TimeMan

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.

The topology on TimeMan.

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

The manifold structure on TimeMan

The orientation on TimeMan

13 declarations

instance

Topological space structure on TimeMan\text{TimeMan} induced by val\text{val}

The manifold TimeMan\text{TimeMan} is equipped with a topological space structure. This topology is the induced topology (the coarsest topology) such that the map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is continuous, where R\mathbb{R} carries its standard topology.

theorem

val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is surjective

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R}, which relates the time manifold TimeMan\text{TimeMan} to the real numbers R\mathbb{R}, is surjective.

theorem

range(val)=R\text{range}(\text{val}) = \mathbb{R}

The range of the map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R}, which maps elements of the time manifold to the real numbers, is the set of all real numbers R\mathbb{R}.

theorem

val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is an Inducing Map

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is an inducing map, meaning that the topology on the time manifold TimeMan\text{TimeMan} is the induced topology (the pullback topology) from the standard topology on R\mathbb{R} via the map val\text{val}.

theorem

val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is Injective

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R}, which maps elements of the time manifold to the real numbers, is injective.

theorem

val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is an open embedding

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R}, which maps elements of the time manifold to the real numbers, is an open embedding.

theorem

s⊆TimeMans \subseteq \text{TimeMan} is open iff val(s)⊆R\text{val}(s) \subseteq \mathbb{R} is open

For any subset s⊆TimeMans \subseteq \text{TimeMan}, ss is an open set in the time manifold if and only if its image val(s)={val(x)∣x∈s}\text{val}(s) = \{ \text{val}(x) \mid x \in s \} is an open set in the real numbers R\mathbb{R} under the standard topology.

definition

Homeomorphism TimeMan≅R\text{TimeMan} \cong \mathbb{R} via val\text{val}

The map val:TimeMan→R\text{val}: \text{TimeMan} \to \mathbb{R} is a homeomorphism between the time manifold TimeMan\text{TimeMan} and the real numbers R\mathbb{R}. It identifies elements of TimeMan\text{TimeMan} with their corresponding real values, where TimeMan\text{TimeMan} is equipped with the topology induced by the val\text{val} map.

instance

ChartedSpace\text{ChartedSpace} structure on TimeMan\text{TimeMan} modeled on R\mathbb{R}

The time manifold TimeMan\text{TimeMan} is equipped with the structure of a charted space modeled on the real numbers R\mathbb{R}. This structure is defined by an atlas containing a single global chart, which is the homeomorphism val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} that identifies points in the time manifold with their corresponding real values.

instance

TimeMan\text{TimeMan} is a CωC^\omega manifold modeled on R\mathbb{R}

The time manifold TimeMan\text{TimeMan} is a real-analytic (CωC^\omega) manifold modeled on the real numbers R\mathbb{R} with the standard model with corners I(R,R)\mathcal{I}(\mathbb{R}, \mathbb{R}). This manifold structure is induced by the map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R}, which identifies the manifold with the real line.

theorem

TimeMan.val\text{TimeMan.val} is CωC^\omega

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is real-analytic (of class CωC^\omega) as a map between manifolds, where both the time manifold TimeMan\text{TimeMan} and the real numbers R\mathbb{R} are equipped with their standard manifold structures modeled on R\mathbb{R} with the model with corners I(R,R)\mathcal{I}(\mathbb{R}, \mathbb{R}).

definition

val\text{val} is a CωC^\omega diffeomorphism TimeMan≅R\text{TimeMan} \cong \mathbb{R}

The map val:TimeMan→R\text{val} : \text{TimeMan} \to \mathbb{R} is a real-analytic (CωC^\omega) diffeomorphism between the time manifold TimeMan\text{TimeMan} and the real numbers R\mathbb{R}. This diffeomorphism is established using the homeomorphism val\text{val} and the fact that both val\text{val} and its inverse are of class CωC^\omega with respect to the standard manifold structures on TimeMan\text{TimeMan} and R\mathbb{R}.

instance

Ordering on the time manifold TimeMan\text{TimeMan}

This definition establishes a "less than or equal to" relation ≤\le on the time manifold TimeMan\text{TimeMan}. For any two points x,y∈TimeManx, y \in \text{TimeMan}, the relation x≤yx \le y holds if and only if their corresponding real values satisfy x.val≤y.valx.\text{val} \le y.\text{val}, where val:TimeMan→R\text{val}: \text{TimeMan} \to \mathbb{R} is the canonical map identifying the manifold with the real numbers. This ordering provides a way to define an orientation on the manifold.