Coordinates of vector-bundle sections along curves

This file records the coordinate reading of a section of a vector bundle along a curve in one of the bundle's canonical trivializations. It also relates manifold differentiability of the corresponding total-space map to differentiability and higher regularity of that coordinate reading.

Main definitions and results

• TauCeti.Manifold.sectionCoord: the coordinate reading of a section along a curve.
• TauCeti.Manifold.differentiableWithinAt_sectionCoord: a differentiability entry point for that reading within a parameter set.
• TauCeti.Manifold.differentiableWithinAt_sectionCoord_sum: finite sums of sections with differentiable readings have differentiable readings.
• TauCeti.Manifold.contDiffWithinAt_sectionCoord_iff: the C^n coordinate characterization for a section along a C^n base curve.

noncomputable def TauCeti.Manifold.sectionCoord {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) (x : M) (t : 𝕜) : F

The model-fibre reading of a section W along γ in the vector-bundle trivialization centred at x. The continuous linear map is defined everywhere, carrying Mathlib's junk value 0 at parameters with γ t outside (trivializationAt F V x).baseSet.

@[simp]

theorem TauCeti.Manifold.sectionCoord_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) (x : M) (t : 𝕜) : sectionCoord γ W x t = (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F V x) (γ t)) (W t)

The defining formula for the coordinate reading of a section along a curve.

@[simp]

theorem TauCeti.Manifold.sectionCoord_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W W' : (t : 𝕜) → V (γ t)) (x : M) : sectionCoord γ (fun (t : 𝕜) => W t + W' t) x = sectionCoord γ W x + sectionCoord γ W' x

Coordinate reading commutes with pointwise addition of sections along a curve.

@[simp]

theorem TauCeti.Manifold.sectionCoord_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W W' : (t : 𝕜) → V (γ t)) (x : M) : sectionCoord γ (fun (t : 𝕜) => W t - W' t) x = sectionCoord γ W x - sectionCoord γ W' x

Coordinate reading commutes with pointwise subtraction of sections along a curve.

@[simp]

theorem TauCeti.Manifold.sectionCoord_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) {ι : Type u_7} (A : Finset ι) (U : ι → (t : 𝕜) → V (γ t)) (x : M) : sectionCoord γ (fun (t : 𝕜) => ∑ i ∈ A, U i t) x = fun (t : 𝕜) => ∑ i ∈ A, sectionCoord γ (U i) x t

Coordinate reading commutes with finite sums of sections along a curve.

@[simp]

theorem TauCeti.Manifold.sectionCoord_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) (f : 𝕜 → 𝕜) (x : M) : sectionCoord γ (fun (t : 𝕜) => f t • W t) x = f • sectionCoord γ W x

Coordinate reading commutes with pointwise scalar multiplication of a section along a curve.

@[simp]

theorem TauCeti.Manifold.sectionCoord_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (x : M) : sectionCoord γ (fun (t : 𝕜) => 0) x = 0

The zero section along a curve has zero coordinate reading.

@[simp]

theorem TauCeti.Manifold.sectionCoord_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) (φ : 𝕜 → 𝕜) (x : M) : sectionCoord (γ ∘ φ) (fun (t : 𝕜) => W (φ t)) x = sectionCoord γ W x ∘ φ

The coordinate reading of a reparametrized section is the composition of its reading with the reparametrizing function.

Differentiability of the coordinate reading

theorem TauCeti.Manifold.differentiableWithinAt_sectionCoord_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {M : Type u_4} [TopologicalSpace M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) {ι : Type u_7} {A : Finset ι} {U : ι → (t : 𝕜) → V (γ t)} {x : M} {s : Set 𝕜} {t : 𝕜} (hU : ∀ i ∈ A, DifferentiableWithinAt 𝕜 (sectionCoord γ (U i) x) s t) : DifferentiableWithinAt 𝕜 (sectionCoord γ (fun (r : 𝕜) => ∑ i ∈ A, U i r) x) s t

A finite sum of sections along a curve whose coordinate readings are differentiable within s at t again has a coordinate reading differentiable within s at t.

theorem TauCeti.Manifold.contDiffWithinAt_sectionCoord_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) {n : WithTop ℕ∞} {s : Set 𝕜} {x : M} {t : 𝕜} [ContMDiffVectorBundle n F V I] (hγ : ContMDiffWithinAt (modelWithCornersSelf 𝕜 𝕜) I n γ s t) (hx : γ t ∈ (trivializationAt F V x).baseSet) : ContDiffWithinAt 𝕜 n (sectionCoord γ W x) s t ↔ ContMDiffWithinAt (modelWithCornersSelf 𝕜 𝕜) (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (r : 𝕜) => ⟨γ r, W r⟩) s t

Given a C^n base curve, a section along it is C^n as a map into the total space if and only if its coordinate reading in any trivialization containing the base point is C^n. This statement uses the section's original fibre carriers.

theorem TauCeti.Manifold.differentiableWithinAt_sectionCoord {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) {s : Set 𝕜} {x : M} {t : 𝕜} [ContMDiffVectorBundle 1 F V I] (h : (MDiffAt[s] fun (r : 𝕜) => ⟨γ r, W r⟩) t) (hx : γ t ∈ (trivializationAt F V x).baseSet) : DifferentiableWithinAt 𝕜 (sectionCoord γ W x) s t

A section along a curve which is differentiable within s at t as a map into the total space has a differentiable coordinate reading in the canonical trivialization at any point x whose base set contains γ t.

theorem TauCeti.Manifold.differentiableAt_sectionCoord {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) {x : M} {t : 𝕜} [ContMDiffVectorBundle 1 F V I] (h : (MDiffAt fun (r : 𝕜) => ⟨γ r, W r⟩) t) (hx : γ t ∈ (trivializationAt F V x).baseSet) : DifferentiableAt 𝕜 (sectionCoord γ W x) t

A section along a curve which is differentiable at t as a map into the total space has a differentiable coordinate reading in the canonical trivialization at any point x whose base set contains γ t.

theorem TauCeti.Manifold.differentiableAt_sectionCoord_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] (γ : 𝕜 → M) (W : (t : 𝕜) → V (γ t)) {x : M} {t : 𝕜} [ContMDiffVectorBundle 1 F V I] (hγ : MDiffAt γ t) (hx : γ t ∈ (trivializationAt F V x).baseSet) : DifferentiableAt 𝕜 (sectionCoord γ W x) t ↔ (MDiffAt fun (r : 𝕜) => ⟨γ r, W r⟩) t

Given a differentiable base curve, differentiability of a section along it is equivalent to differentiability of its reading in any bundle chart containing the current base point.