Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.InnerProductSpace.Basic
public import Mathlib.Geometry.Manifold.DiffeomorphThe 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.
@[expose] public section
The type TimeMan represents the time manifold.
Mathematically TimeMan is a manifold diffeomorphic to β with an orientation but no additional
structure.
The choice of a map from TimeMan to β.
structure TimeMan where val : βThe topology on TimeMan.
The topology on TimeMan is induced from the topology on β, via the choice
of map TimeMan.val.
The instance of a topological space on TimeMan induced by the map TimeMan.val. s
instance : TopologicalSpace TimeMan := TopologicalSpace.induced TimeMan.val
PseudoMetricSpace.toUniformSpace.toTopologicalSpacelemma val_surjective : Function.Surjective TimeMan.val := β’ Function.Surjective val
t:ββ’ β a, a.val = t
All goals completed! π@[simp]
lemma val_range : Set.range val = Set.univ := β’ Set.range val = Set.univ
All goals completed! πlemma val_inducing : Topology.IsInducing TimeMan.val where
eq_induced := rfllemma val_injective : Function.Injective TimeMan.val := β’ Function.Injective val
t1:TimeMant2:TimeManh:t1.val = t2.valβ’ t1 = t2
t2:TimeManvalβ:βh:{ val := valβ }.val = t2.valβ’ { val := valβ } = t2
valβΒΉ:βvalβ:βh:{ val := valβΒΉ }.val = { val := valβ }.valβ’ { val := valβΒΉ } = { val := valβ }
All goals completed! πlemma val_isOpenEmbedding : Topology.IsOpenEmbedding TimeMan.val where
eq_induced := rfl
isOpen_range := β’ IsOpen (Set.range val)
All goals completed! π
injective := val_injectivelemma isOpen_iff {s : Set TimeMan} :
IsOpen s β IsOpen (TimeMan.val '' s) :=
Topology.IsOpenEmbedding.isOpen_iff_image_isOpen val_isOpenEmbedding
The choice of map Time.val from TimeMan to β as a homeomorphism.
s:Set TimeManhs:IsOpen (val '' s)β’ IsOpen (?m.66 '' s)s:Set TimeManhs:IsOpen (val '' s)β’ Function.LeftInverse (fun t => { val := t }) ?m.66s:Set TimeManhs:IsOpen (val '' s)β’ Function.RightInverse (fun t => { val := t }) ?m.66s:Set TimeManhs:IsOpen (val '' s)β’ TimeMan β β
s:Set TimeManhs:IsOpen (val '' s)β’ IsOpen (?m.66 '' s) All goals completed! π
s:Set TimeManhs:IsOpen (val '' s)β’ Function.LeftInverse (fun t => { val := t }) val s:Set TimeManhs:IsOpen (val '' s)t:TimeManβ’ (fun t => { val := t }) t.val = t
All goals completed! π
s:Set TimeManhs:IsOpen (val '' s)β’ Function.RightInverse (fun t => { val := t }) val s:Set TimeManhs:IsOpen (val '' s)x:ββ’ ((fun t => { val := t }) x).val = x
All goals completed! πThe manifold structure on TimeMan
The structure of a charted space on TimeMan
instance : ChartedSpace β TimeMan where
atlas := { valHomeomorphism.toOpenPartialHomeomorph }
chartAt _ := valHomeomorphism.toOpenPartialHomeomorph
mem_chart_source := β’ β (x : TimeMan), x β valHomeomorphism.toOpenPartialHomeomorph.source
All goals completed! π
chart_mem_atlas := β’ β (x : TimeMan), valHomeomorphism.toOpenPartialHomeomorph β {valHomeomorphism.toOpenPartialHomeomorph}
x:TimeManβ’ valHomeomorphism.toOpenPartialHomeomorph β {valHomeomorphism.toOpenPartialHomeomorph}
All goals completed! π
The structure of a manifold on TimeMan induced by the choice of map Time.val.
instance : IsManifold π(β, β) Ο TimeMan where
compatible := β’ β {e e' : OpenPartialHomeomorph TimeMan β},
e β atlas β TimeMan β e' β atlas β TimeMan β e.symm β«β e' β contDiffGroupoid Ο π(β, β)
e1:OpenPartialHomeomorph TimeMan βe2:OpenPartialHomeomorph TimeMan βh1:e1 β atlas β TimeManh2:e2 β atlas β TimeManβ’ e1.symm β«β e2 β contDiffGroupoid Ο π(β, β)
e1:OpenPartialHomeomorph TimeMan βe2:OpenPartialHomeomorph TimeMan βh1:e1 = valHomeomorphism.toOpenPartialHomeomorphh2:e2 = valHomeomorphism.toOpenPartialHomeomorphβ’ e1.symm β«β e2 β contDiffGroupoid Ο π(β, β)
β’ valHomeomorphism.toOpenPartialHomeomorph.symm β«β valHomeomorphism.toOpenPartialHomeomorph β contDiffGroupoid Ο π(β, β)
All goals completed! πlemma val_contDiff : ContMDiff π(β, β) π(β, β) Ο TimeMan.val := β’ ContMDiff π(β, β) π(β, β) Ο val
β’ ContMDiffOn π(β, β) π(β, β) Ο val Set.univ
All goals completed! πThe orientation on TimeMan
The instance of an orientation on TimeMan.