UniqueMDiffOn.tangentBundle_proj_preimage
theorem UniqueMDiffOn.tangentBundle_proj_preimage :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ๐ E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{s : Set M}, UniqueMDiffOn I s โ UniqueMDiffOn I.tangent (Bundle.TotalSpace.proj โปยน' s)
The theorem `UniqueMDiffOn.tangentBundle_proj_preimage` states that for any non-trivially normed field `๐`, normed add commutative group `E`, topological space `H`, model with corners `I`, topological space `M`, charted space `M`, smooth manifold with corners `I M`, and set `s` of `M` with unique differentiability, the pre-image of `s` under the projection from the tangent bundle also has unique differentiability. Essentially, if a set in the base space of a tangent bundle has unique differentiability, then its pre-image in the total space (or tangent space) also has unique differentiability. This is useful in differential geometry, where differentiability properties of base spaces and their corresponding tangent spaces are often interconnected.
More concisely: For any non-trivially normed field `๐`, normed add commutative group `E`, topological space `H`, model with corners `I`, topological space `M`, charted space `M`, smooth manifold with corners `IM`, and set `s` of `M` with unique differentiability, the pre-image of `s` under the projection from the tangent bundle `TM` has unique differentiability as well.
|
UniqueMDiffOn.smooth_bundle_preimage
theorem UniqueMDiffOn.smooth_bundle_preimage :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ๐ E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{s : Set M} {F : Type u_8} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ๐ F] (Z : M โ Type u_9)
[inst_9 : TopologicalSpace (Bundle.TotalSpace F Z)] [inst_10 : (b : M) โ TopologicalSpace (Z b)]
[inst_11 : (b : M) โ AddCommMonoid (Z b)] [inst_12 : (b : M) โ Module ๐ (Z b)] [inst_13 : FiberBundle F Z]
[inst_14 : VectorBundle ๐ F Z] [inst_15 : SmoothVectorBundle F Z I],
UniqueMDiffOn I s โ UniqueMDiffOn (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s)
This theorem states that given a smooth fiber bundle, if a set in the base space possesses a unique differential structure, then its preimage under the bundle projection also possesses a unique differential structure. In detail, this occurs under the following conditions:
- The base space and fibers are normed additive commutative groups.
- The base space and fibers are both normed spaces over a nontrivially normed field.
- The base space is a smooth manifold with corners.
- The fibers form a vector bundle over the base space.
- The total space of this vector bundle is a topological space.
- Each fiber is also a topological space.
- Each fiber is a module over the same nontrivially normed field.
- The bundle is a fiber bundle and a smooth vector bundle.
The unique differential structure on the preimage is with respect to the product of the model with corners of the base space and the model with corners of the fibers.
More concisely: Given a smooth fiber bundle of normed additive commutative groups over a smooth manifold with corners, if each fiber possesses a unique differential structure as a normed vector space, then the preimage of any set in the base space under the bundle projection also inherits a unique differential structure as the product of the differential structures on the base space and fiber.
|
UniqueMDiffOn.uniqueMDiffOn_preimage
theorem UniqueMDiffOn.uniqueMDiffOn_preimage :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ๐ E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace ๐ E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {s : Set M},
UniqueMDiffOn I s โ
โ {e : PartialHomeomorph M M'},
PartialHomeomorph.MDifferentiable I I' e โ UniqueMDiffOn I' (e.target โฉ โe.symm โปยน' s)
This theorem states that if a set possesses a unique differential property within the context of a certain mathematical structure (a smooth manifold with corners), then the image of this set under a local diffeomorphism (a kind of smooth, invertible function) also possesses this unique differential property, given that the local diffeomorphism is differentiable. The mathematical structure in this case includes the topological properties of the set, the normed field over which it is defined, and the NormedAddCommGroup, NormedSpace, TopologicalSpace, and ChartedSpace structures it inhabits, along with the associated ModelWithCorners.
More concisely: If a set on a smooth manifold with corners has a unique differential property and is mapped under a local diffeomorphism, then the image set also has that unique differential property.
|
UniqueMDiffOn.uniqueDiffOn_target_inter
theorem UniqueMDiffOn.uniqueDiffOn_target_inter :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ๐ E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{s : Set M},
UniqueMDiffOn I s โ โ (x : M), UniqueDiffOn ๐ ((extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' s)
This theorem states that for every set in a smooth manifold with corners that has the unique derivative property, the pullback of that set by any extended chart also has the unique derivative property. In more detail, given a non-trivially normed field `๐`, a normed additive commutative group `E` over `๐`, a topological space `H`, a model with corners `I` from `๐` to `E` and `H`, a topological space `M` with a charted space structure relative to `H`, and a smooth manifold with corners structure on `M` with respect to `I`, if a set `s` in `M` has the unique derivative property, then for each point `x` in `M`, the intersection of the target of the extended chart at `x` with the pre-image under the inverse of the extended chart at `x` of `s` also has the unique derivative property in the normed field `๐`.
More concisely: Given a smooth manifold with corners `M` over a normed field `๐` with the unique derivative property at each point, and a smooth chart `c : M โ_open H` for some open subset `H` of a normed additive commutative group `E`, the pullback of any subset `s` in `M` with the unique derivative property under `c` also has the unique derivative property in `E`.
|
UniqueMDiffOn.uniqueDiffOn_inter_preimage
theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ๐ E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace ๐ E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners ๐ E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] {s : Set M},
UniqueMDiffOn I s โ
โ (x : M) (y : M') {f : M โ M'},
ContinuousOn f s โ
UniqueDiffOn ๐
((extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' (s โฉ f โปยน' (extChartAt I' y).source))
This theorem is about the unique differential of pullback functions between differential manifolds. Given a non-trivially normed field `๐`, normed add commutative group `E` and `E'`, topological spaces `H`, `H'`, `M`, and `M'`, along with ModelWithCorners `I` and `I'`, and a set `s` of `M`, if `s` is a unique differentiability set on `I`, then for any points `x` in `M` and `y` in `M'` and any function `f` from `M` to `M'` that is continuous on `s`, the intersection of the target of the extended chart at `x` and the preimage under the inverse of the symmetrical extended chart at `x` of the intersection of `s` and the preimage of the source of the extended chart at `y` under `f`, is a unique differentiability set on `๐`. In simple terms, it states a condition under which the differential of a pullback function between manifolds is unique.
More concisely: Given continuous functions between manifolds, if their restrictions to a common differentiability set have unique differentials, then those differentials define a unique pullback differential between the manifolds.
|