tangentBundle_model_space_chartAt
theorem tangentBundle_model_space_chartAt :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
(p : TangentBundle I H),
(chartAt (ModelProd H E) p).toPartialEquiv = (Bundle.TotalSpace.toProd H E).toPartialEquiv
This theorem states that for any non-trivially normed field ๐, normed additive commutative group E, and topological space H, with given model with corners I, and any point p in the tangent bundle of H with respect to I, the preferred chart at point p (represented by `chartAt (ModelProd H E) p`) is equivalent to the trivial bundle corresponding to the product of H and E (expressed as `(Bundle.TotalSpace.toProd H E)`). In other words, it asserts that in the tangent bundle to the model space, the charts just correspond to the canonical identification between a product type and a sigma type, also known as `TotalSpace.toProd`.
More concisely: For any non-trivially normed field ๐, normed additive commutative group E, and topological space H with model with corners I, the chart at any point p in the tangent bundle of H with respect to I is equivalent to the trivial bundle of the product H x E.
|
contDiffOn_fderiv_coord_change
theorem contDiffOn_fderiv_coord_change :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ๐ E H)
{M : Type u_6} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
(i j : โ(atlas H M)),
ContDiffOn ๐ โค (fderivWithin ๐ (โ((โj).extend I) โ โ((โi).extend I).symm) (Set.range โI))
(((โi).extend I).symm.trans ((โj).extend I)).source
This theorem, `contDiffOn_fderiv_coord_change`, is an auxiliary lemma for tangent spaces in differential geometry. It states that for a given non-trivially normed field `๐`, types `E` and `H` with given normed add comm group and normed space structures (over `๐`), and a topological space `M` with a charted space structure (over `H`) and a smooth manifold with corners structure (associated with a model with corners `I` on `๐`, `E` and `H`), the derivative of a coordinate change between two charts (represented by `i` and `j` from the atlas of the charted space) is smooth over its source. This is quantified precisely by saying that the derivative of the composed function `j โ iโปยน` (with derivative taken within the range of `I`) is continuously differentiable on the source of the transformation from `i` to `j`. This property is essential in the theory of differential geometry for the smooth transition between different local coordinate systems (charts).
More concisely: The derivative of a coordinate change between two charts in a smooth manifold with corners is continuously differentiable on its source.
|