Documentation

Physicslib4.Spacetime.DiffeoPath

Pushforward of a smooth path along a diffeomorphism #

The pushforward ψ ∘ μ of a smooth path along a C^∞ diffeomorphism of the underlying manifolds, its tangent vector (the chain rule along the parameter space) and the transport of past and future endpoints.

No metric appears anywhere in this file, which is why it sits below Physicslib4/Spacetime/IsometryCausality.lean in the import graph: the single-metric pushforward Isometry.pushforwardPath there is the instance N := M of pushforwardPath at ψ := g.toDiffeo and is defined as such, rather than being a second copy of the same construction. The cross-metric consumers live in Physicslib4/Spacetime/CrossMetricIsometry.lean.

Main definitions #

source
theorem Physicslib4.Spacetime.mfderivWithin_comp_diffeo {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) :
(mfderiv[μ.parameterSpace] (⇑ψ ∘ μ.toFun) s) 1 = (mfderiv% ⇑ψ (μ.toFun s)) ((mfderiv[μ.parameterSpace] μ.toFun s) 1)

The tangent chain rule along a path (lmm:cross-metric-pushforward-path-tangent): d/ds (ψ ∘ μ)(s) = dψ_{μ s}(μ̇ s), the derivatives being taken within the parameter space. The identity is about the differential of ψ alone and mentions no metric.

source
noncomputable def Physicslib4.Spacetime.pushforwardPath {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) :
N.SmoothPath

Pushforward of a path along a diffeomorphism (lmm:cross-metric-pushforward-path): ψ ∘ μ on the same parameter space, with the same closedness, connectedness and non-triviality data. The only real obligation is non-vanishing of the tangent vector, which follows from injectivity of dψ_{μ s} (mfderivEquiv).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Physicslib4.Spacetime.pushforwardPath_parameterSpace {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) :
    (pushforwardPath ψ μ).parameterSpace = μ.parameterSpace
    source
    @[simp]
    theorem Physicslib4.Spacetime.pushforwardPath_toFun {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) :
    (pushforwardPath ψ μ).toFun = ⇑ψ ∘ μ.toFun
    source
    theorem Physicslib4.Spacetime.pushforwardPath_tangent {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) :
    (pushforwardPath ψ μ).tangent s = (mfderiv% ⇑ψ (μ.toFun s)) (μ.tangent s)

    The tangent vector of the pushforward path is dψ applied to the tangent vector of μ (lmm:cross-metric-pushforward-path-tangent).

    source
    theorem Physicslib4.Spacetime.pushforwardPath_isPastEndpoint {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) {p : M.Carrier} (h : M.IsPastEndpoint μ p) :
    N.IsPastEndpoint (pushforwardPath ψ μ) (ψ p)

    The pushforward transports past endpoints (lmm:cross-metric-pushforward-path-endpoints). No metric or causal input is used: the same parameter witnesses the condition.

    source
    theorem Physicslib4.Spacetime.pushforwardPath_isFutureEndpoint {M : Spacetime} {N : Spacetime} (ψ : M.Diffeo N) (μ : M.SmoothPath) {p : M.Carrier} (h : M.IsFutureEndpoint μ p) :
    N.IsFutureEndpoint (pushforwardPath ψ μ) (ψ p)

    The pushforward transports future endpoints (lmm:cross-metric-pushforward-path-endpoints).