Bundle.contMDiffWithinAt_totalSpace
theorem Bundle.contMDiffWithinAt_totalSpace :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
[inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
[inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
{EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
[inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
[inst_12 : ChartedSpace HM M] {n : ℕ∞} [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B]
[inst_15 : FiberBundle F E] (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M},
ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔
ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s
x₀
The theorem `Bundle.contMDiffWithinAt_totalSpace` characterizes functions that are continuously differentiable up to order `n` into a smooth vector bundle. For all types `𝕜`, `B`, `F`, `M`, `E`, `EB`, `HB`, `EM`, `HM`, and a function `f` from `M` to the total space of the bundle `F E`, and for a subset `s` of `M` and a point `x₀` in `M`, the function `f` is continuously differentiable within the set `s` at the point `x₀` if and only if both the projection of the function `f` and the trivialization (a process that simplifies the function `f` at the point `x₀`) are continuously differentiable within the set `s` at the point `x₀`. The theorem makes use of the `ModelWithCorners` structure, which provides a smooth transition from the manifold to the Euclidean space, and a `FiberBundle`, which is a generalization of the notion of a vector bundle.
More concisely: A function from a manifold to its smooth vector bundle is continuously differentiable up to order n at a point if and only if both the projection and the trivialization of the function are continuously differentiable at that point.
|
Bundle.contMDiffAt_section
theorem Bundle.contMDiffAt_section :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
[inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
[inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
{n : ℕ∞} [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
(s : (x : B) → E x) (x₀ : B),
ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => Bundle.TotalSpace.mk' F x (s x)) x₀ ↔
ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2)
x₀
The theorem `Bundle.contMDiffAt_section` characterizes the sections of a smooth vector bundle that are continuously differentiable up to order `n`. Given a section `s` of a fiber bundle `F` over base space `B`, the theorem asserts that the section is continuously differentiable at a point `x₀` of `B` in the total space of the bundle (with the model with corners `IB.prod (modelWithCornersSelf 𝕜 F)`) if and only if the second component of the trivialization of the bundle at `x₀` applied to the pair `(x, s x)` is continuously differentiable at `x₀` with respect to the model with corners `IB` and `modelWithCornersSelf 𝕜 F`. Here, continuous differentiability is defined with respect to a general field `𝕜`, which is equipped with a non-trivial normed field structure.
More concisely: A section of a smooth vector bundle over a base space is continuously differentiable up to order n at a point in the base space if and only if the second component of the trivialization of the bundle at that point applied to the pair (x, section value at x) is continuously differentiable with respect to the bundle's fiber model and the base space model, with respect to a general normed field.
|
VectorPrebundle.smoothVectorBundle
theorem VectorPrebundle.smoothVectorBundle :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
[inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
(IB : ModelWithCorners 𝕜 EB HB) [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
[inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
[inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E)
[ha : VectorPrebundle.IsSmooth IB a], SmoothVectorBundle F E IB
This theorem states that given a 'VectorPrebundle' in a certain mathematical context, it is always possible to construct from it a 'SmoothVectorBundle'. The context is defined by several conditions on the types and structures involved, including that 𝕜 is a nontrivially normed field, EB is a normed additive commutative group that forms a normed space over 𝕜, HB is a topological space, B is a topological space charted over HB, E is an additive commutative monoid and a module over 𝕜 for each x in B, F is a normed additive commutative group and a normed space over 𝕜, and E has a topological space structure for each x in B. The 'VectorPrebundle' a must satisfy the 'VectorPrebundle.IsSmooth' property with respect to the model with corners IB.
More concisely: Given a VectorPrebundle a over a charted topological space B in a nontrivially normed field 𝕜 satisfying certain conditions, it can be smoothily upgraded to a SmoothVectorBundle.
|
Bundle.contMDiffAt_totalSpace
theorem Bundle.contMDiffAt_totalSpace :
∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
[inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
[inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
{EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
[inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
[inst_12 : ChartedSpace HM M] {n : ℕ∞} [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B]
[inst_15 : FiberBundle F E] (f : M → Bundle.TotalSpace F E) (x₀ : M),
ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔
ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
This theorem characterizes continuously differentiable functions of order $n$ into a smooth vector bundle. Given a non-trivially normed field, a normed additive group, a normed space, a topological space, a charted space, a model with corners, and a fiber bundle, the theorem states that a function $f$ from a manifold $M$ to the total space of a fiber bundle is continuously differentiable at a point $x_0$ in $M$ if and only if the projection of $f$ at $x_0$ is continuously differentiable and the second component of the trivialization of $f$ at $x_0$ is also continuously differentiable. This theorem thus gives a precise condition for the differentiability of functions into a vector bundle.
More concisely: A function from a manifold to a fiber bundle is continuously differentiable at a point if and only if the projection and the second component of the trivialization are both continuously differentiable at that point.
|