Smooth fibrewise translation of vector bundles #
Let V be a vector bundle over B and b : X → B a map. A family s x ∈ V (b x) is a section
of V along b, and its total-space map is x ↦ ⟨b x, s x⟩. Fibrewise sums of C^n sections
along the same map are C^n (ContMDiff.add_sectionAlong); for b = id this is Mathlib's
ContMDiff.add_section. So are fibrewise differences (ContMDiff.sub_sectionAlong); for
products with C^n functions, see ContMDiff.smul_totalSpace. Finite sums follow
(ContMDiff.sum_sectionAlong); smoothness of the base map is assumed so that the empty sum, the
zero section along b, is covered. The general form applies to maps defined on the total space
itself, which are sections along the projection. Differences of differentiable sections along a
common base map are differentiable as well
(MDifferentiableWithinAt.sub_sectionAlong).
Consequently a C^n section s of V translates the fibres by a C^n diffeomorphism
p ↦ p + s (π p) of the total space, with inverse the translation by -s
(TauCeti.vectorBundleTranslateDiffeomorph). Like the fibrewise rescaling
TauCeti.vectorBundleScalarDiffeomorph, it preserves the projection and needs no global
trivialization. For the cotangent bundle, translation by a one-form is the basic example of a
fibre-preserving map whose effect on the canonical forms is computed by the one-form.
theorem
ContMDiffWithinAt.add_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{u : Set X}
{x₀ : X}
(hs : ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) u x₀)
(ht : ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) u x₀)
:
ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x + t x⟩) u x₀
The fibrewise sum of two C^n sections along the same map is C^n.
theorem
ContMDiffAt.add_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{x₀ : X}
(hs : ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) x₀)
(ht : ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) x₀)
:
ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x + t x⟩) x₀
The fibrewise sum of two C^n sections along the same map is C^n.
theorem
ContMDiffOn.add_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{u : Set X}
(hs : ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) u)
(ht : ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) u)
:
ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x + t x⟩) u
The fibrewise sum of two C^n sections along the same map is C^n.
theorem
ContMDiff.add_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
(hs : ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, s x⟩)
(ht : ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, t x⟩)
:
ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, s x + t x⟩
The fibrewise sum of two C^n sections along the same map is C^n.
theorem
ContMDiffWithinAt.sum_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{u : Set X}
{x₀ : X}
{ι : Type u_10}
(A : Finset ι)
(s : ι → (x : X) → V (b x))
(hb : ContMDiffWithinAt IX IB n b u x₀)
(hs : ∀ i ∈ A, ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s i x⟩) u x₀)
:
ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, ∑ i ∈ A, s i x⟩) u x₀
A finite sum of C^n sections along a C^n map is C^n within a set at a point.
theorem
ContMDiffAt.sum_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{x₀ : X}
{ι : Type u_10}
(A : Finset ι)
(s : ι → (x : X) → V (b x))
(hb : ContMDiffAt IX IB n b x₀)
(hs : ∀ i ∈ A, ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s i x⟩) x₀)
:
ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, ∑ i ∈ A, s i x⟩) x₀
A finite sum of C^n sections along a C^n map is C^n at a point.
theorem
ContMDiffOn.sum_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{u : Set X}
{ι : Type u_10}
(A : Finset ι)
(s : ι → (x : X) → V (b x))
(hb : ContMDiffOn IX IB n b u)
(hs : ∀ i ∈ A, ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s i x⟩) u)
:
ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, ∑ i ∈ A, s i x⟩) u
A finite sum of C^n sections along a C^n map is C^n on a set.
theorem
ContMDiff.sum_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommMonoid (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{ι : Type u_10}
(A : Finset ι)
(s : ι → (x : X) → V (b x))
(hb : ContMDiff IX IB n b)
(hs : ∀ i ∈ A, ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, s i x⟩)
:
ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, ∑ i ∈ A, s i x⟩
A finite sum of C^n sections along a C^n map is C^n.
theorem
ContMDiffWithinAt.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{u : Set X}
{x₀ : X}
(hs : ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) u x₀)
(ht : ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) u x₀)
:
ContMDiffWithinAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x - t x⟩) u x₀
The fibrewise difference of two C^n sections along the same map is C^n.
theorem
ContMDiffAt.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{x₀ : X}
(hs : ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) x₀)
(ht : ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) x₀)
:
ContMDiffAt IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x - t x⟩) x₀
The fibrewise difference of two C^n sections along the same map is C^n.
theorem
ContMDiffOn.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{u : Set X}
(hs : ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x⟩) u)
(ht : ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, t x⟩) u)
:
ContMDiffOn IX (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : X) => ⟨b x, s x - t x⟩) u
The fibrewise difference of two C^n sections along the same map is C^n.
theorem
ContMDiff.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
(hs : ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, s x⟩)
(ht : ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, t x⟩)
:
ContMDiff IX (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (x : X) => ⟨b x, s x - t x⟩
The fibrewise difference of two C^n sections along the same map is C^n.
theorem
MDifferentiableWithinAt.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{u : Set X}
{x₀ : X}
(hs : (MDiffAt[u] fun (x : X) => ⟨b x, s x⟩) x₀)
(ht : (MDiffAt[u] fun (x : X) => ⟨b x, t x⟩) x₀)
:
(MDiffAt[u] fun (x : X) => ⟨b x, s x - t x⟩) x₀
The difference of differentiable sections along the same base map is differentiable.
theorem
MDifferentiableAt.sub_sectionAlong
{𝕜 : Type u_1}
{B : Type u_2}
{X : Type u_3}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
{EX : Type u_7}
{HX : Type u_8}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup EX]
[NormedSpace 𝕜 EX]
[TopologicalSpace HX]
{IX : ModelWithCorners 𝕜 EX HX}
[TopologicalSpace X]
[ChartedSpace HX X]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{b : X → B}
{s t : (x : X) → V (b x)}
{x₀ : X}
(hs : (MDiffAt fun (x : X) => ⟨b x, s x⟩) x₀)
(ht : (MDiffAt fun (x : X) => ⟨b x, t x⟩) x₀)
:
(MDiffAt fun (x : X) => ⟨b x, s x - t x⟩) x₀
The difference of differentiable sections along the same base map is differentiable.
def
TauCeti.vectorBundleTranslateDiffeomorph
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(σ : (y : B) → V y)
(hσ : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (y : B) => ⟨y, σ y⟩)
:
Diffeomorph (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace F V)
(Bundle.TotalSpace F V) n
A C^n section σ of a vector bundle translates the fibres by a C^n diffeomorphism
p ↦ p + σ (π p) of the total space. Its inverse is the translation by -σ.
Instances For
@[simp]
theorem
TauCeti.vectorBundleTranslateDiffeomorph_apply
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(σ : (y : B) → V y)
(hσ : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (y : B) => ⟨y, σ y⟩)
(p : Bundle.TotalSpace F V)
:
Fibrewise translation by σ adds the value of σ at the base point.
@[simp]
theorem
TauCeti.vectorBundleTranslateDiffeomorph_symm
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(σ : (y : B) → V y)
(hσ : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (y : B) => ⟨y, σ y⟩)
:
The inverse of the translation by σ is the translation by -σ.
@[simp]
theorem
TauCeti.vectorBundleTranslateDiffeomorph_zero
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
vectorBundleTranslateDiffeomorph 0 ⋯ = Diffeomorph.refl (IB.prod (modelWithCornersSelf 𝕜 F)) (Bundle.TotalSpace F V) n
Translation by the zero section is the identity diffeomorphism.
theorem
TauCeti.vectorBundleTranslateDiffeomorph_trans
{𝕜 : Type u_1}
{B : Type u_2}
{F : Type u_4}
{EB : Type u_5}
{HB : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup EB]
[NormedSpace 𝕜 EB]
[TopologicalSpace HB]
{IB : ModelWithCorners 𝕜 EB HB}
[TopologicalSpace B]
[ChartedSpace HB B]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{V : B → Type u_9}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[FiberBundle F V]
{n : WithTop ℕ∞}
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(σ τ : (y : B) → V y)
(hσ : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (y : B) => ⟨y, σ y⟩)
(hτ : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n fun (y : B) => ⟨y, τ y⟩)
:
(vectorBundleTranslateDiffeomorph σ hσ).trans (vectorBundleTranslateDiffeomorph τ hτ) = vectorBundleTranslateDiffeomorph (σ + τ) ⋯
Successive fibre translations add the sections.