Documentation

Mathlib.Geometry.Manifold.VectorBundle.Tangent

Tangent bundles #

This file defines the tangent bundle as a smooth vector bundle.

Let M be a smooth manifold with corners with model I on (E, H). We define the tangent bundle of M using the VectorBundleCore construction indexed by the charts of M with fibers E. Given two charts i, j : PartialHomeomorph M H, the coordinate change between i and j at a point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I โŠ† E at I (i x) : E. This defines a smooth vector bundle TangentBundle with fibers TangentSpace.

Main definitions #

theorem contDiffOn_fderiv_coord_change {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) (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

Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.

@[simp]
theorem tangentBundleCore_coordChange {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) (j : โ†‘(atlas H M)) (x : M) :
(tangentBundleCore I M).coordChange i j x = fderivWithin ๐•œ (โ†‘((โ†‘j).extend I) โˆ˜ โ†‘((โ†‘i).extend I).symm) (Set.range โ†‘I) (โ†‘((โ†‘i).extend I) x)
@[simp]
theorem tangentBundleCore_indexAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
(tangentBundleCore I M).indexAt x = achart H x
def tangentBundleCore {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
VectorBundleCore ๐•œ M E โ†‘(atlas H M)

Let M be a smooth manifold with corners with model I on (E, H). Then VectorBundleCore I M is the vector bundle core for the tangent bundle over M. It is indexed by the atlas of M, with fiber E and its change of coordinates from the chart i to the chart j at point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I โŠ† E at I (i x) : E.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem tangentBundleCore_baseSet {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (i : โ†‘(atlas H M)) :
    (tangentBundleCore I M).baseSet i = (โ†‘i).source
    theorem tangentBundleCore_coordChange_achart {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (x' : M) (z : M) :
    (tangentBundleCore I M).coordChange (achart H x) (achart H x') z = fderivWithin ๐•œ (โ†‘(extChartAt I x') โˆ˜ โ†‘(extChartAt I x).symm) (Set.range โ†‘I) (โ†‘(extChartAt I x) z)
    @[reducible, inline]
    abbrev tangentCoordChange {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (y : M) :
    M โ†’ E โ†’L[๐•œ] E

    In a manifold M, given two preferred charts indexed by x y : M, tangentCoordChange I x y is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values outside the intersection of the sources of the two charts.

    Note that this definition takes advantage of the fact that tangentBundleCore has the same base sets as the preferred charts of the base manifold.

    Equations
    Instances For
      theorem tangentCoordChange_def {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {y : M} {z : M} :
      tangentCoordChange I x y z = fderivWithin ๐•œ (โ†‘(extChartAt I y) โˆ˜ โ†‘(extChartAt I x).symm) (Set.range โ†‘I) (โ†‘(extChartAt I x) z)
      theorem tangentCoordChange_self {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {z : M} {v : E} (h : z โˆˆ (extChartAt I x).source) :
      (tangentCoordChange I x x z) v = v
      theorem tangentCoordChange_comp {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {w : M} {x : M} {y : M} {z : M} {v : E} (h : z โˆˆ (extChartAt I w).source โˆฉ (extChartAt I x).source โˆฉ (extChartAt I y).source) :
      (tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v
      theorem hasFDerivWithinAt_tangentCoordChange {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {y : M} {z : M} (h : z โˆˆ (extChartAt I x).source โˆฉ (extChartAt I y).source) :
      HasFDerivWithinAt (โ†‘(extChartAt I y) โˆ˜ โ†‘(extChartAt I x).symm) (tangentCoordChange I x y z) (Set.range โ†‘I) (โ†‘(extChartAt I x) z)
      theorem continuousOn_tangentCoordChange {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (y : M) :
      ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source โˆฉ (extChartAt I y).source)
      def TangentSpace {๐•œ : Type u_10} [NontriviallyNormedField ๐•œ] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_11} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_12} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (_x : M) :
      Type u_9

      The tangent space at a point of the manifold M. It is just E. We could use instead (tangentBundleCore I M).to_topological_vector_bundle_core.fiber x, but we use E to help the kernel.

      Equations
      Instances For
        instance instTopologicalAddGroupTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} :
        Equations
        • โ‹ฏ = โ‹ฏ
        @[reducible, inline]
        abbrev TangentBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
        Type (max u_6 u_2)

        The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of Bundle.TotalSpace to be able to put a suitable topology on it.

        Equations
        Instances For
          instance instModuleTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          Module ๐•œ (TangentSpace I x)
          Equations
          instance instInhabitedTangentSpace {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          Equations
          instance instTopologicalSpaceTangentBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
          Equations
          instance TangentSpace.fiberBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
          Equations
          instance TangentSpace.vectorBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
          VectorBundle ๐•œ E (TangentSpace I)
          Equations
          • โ‹ฏ = โ‹ฏ
          theorem TangentBundle.chartAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) :
          chartAt (ModelProd H E) p = ((tangentBundleCore I M).toFiberBundleCore.localTriv (achart H p.proj)).trans ((chartAt H p.proj).prod (PartialHomeomorph.refl E))
          theorem TangentBundle.chartAt_toPartialEquiv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) :
          (chartAt (ModelProd H E) p).toPartialEquiv = ((tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.proj)).trans ((chartAt H p.proj).prod (PartialEquiv.refl E))
          theorem TangentBundle.trivializationAt_eq_localTriv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          trivializationAt E (TangentSpace I) x = (tangentBundleCore I M).toFiberBundleCore.localTriv (achart H x)
          @[simp]
          theorem TangentBundle.trivializationAt_source {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          (trivializationAt E (TangentSpace I) x).source = Bundle.TotalSpace.proj โปยน' (chartAt H x).source
          @[simp]
          theorem TangentBundle.trivializationAt_target {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          (trivializationAt E (TangentSpace I) x).target = (chartAt H x).source ร—หข Set.univ
          @[simp]
          theorem TangentBundle.trivializationAt_baseSet {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) :
          (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source
          theorem TangentBundle.trivializationAt_apply {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (z : TangentBundle I M) :
          โ†‘(trivializationAt E (TangentSpace I) x) z = (z.proj, (fderivWithin ๐•œ (โ†‘((chartAt H x).extend I) โˆ˜ โ†‘((chartAt H z.proj).extend I).symm) (Set.range โ†‘I) (โ†‘((chartAt H z.proj).extend I) z.proj)) z.snd)
          @[simp]
          theorem TangentBundle.trivializationAt_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (x : M) (z : TangentBundle I M) :
          (โ†‘(trivializationAt E (TangentSpace I) x) z).1 = z.proj
          @[simp]
          theorem TangentBundle.mem_chart_source_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) (q : TangentBundle I M) :
          p โˆˆ (chartAt (ModelProd H E) q).source โ†” p.proj โˆˆ (chartAt H q.proj).source
          @[simp]
          theorem TangentBundle.mem_chart_target_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : H ร— E) (q : TangentBundle I M) :
          p โˆˆ (chartAt (ModelProd H E) q).target โ†” p.1 โˆˆ (chartAt H q.proj).target
          @[simp]
          theorem TangentBundle.coe_chartAt_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : TangentBundle I M) (q : TangentBundle I M) :
          (โ†‘(chartAt (ModelProd H E) q) p).1 = โ†‘(chartAt H q.proj) p.proj
          @[simp]
          theorem TangentBundle.coe_chartAt_symm_fst {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (p : H ร— E) (q : TangentBundle I M) :
          (โ†‘(chartAt (ModelProd H E) q).symm p).proj = โ†‘(chartAt H q.proj).symm p.1
          @[simp]
          theorem TangentBundle.trivializationAt_continuousLinearMapAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {bโ‚€ : M} {b : M} (hb : b โˆˆ (trivializationAt E (TangentSpace I) bโ‚€).baseSet) :
          Trivialization.continuousLinearMapAt ๐•œ (trivializationAt E (TangentSpace I) bโ‚€) b = (tangentBundleCore I M).coordChange (achart H b) (achart H bโ‚€) b
          @[simp]
          theorem TangentBundle.trivializationAt_symmL {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {bโ‚€ : M} {b : M} (hb : b โˆˆ (trivializationAt E (TangentSpace I) bโ‚€).baseSet) :
          Trivialization.symmL ๐•œ (trivializationAt E (TangentSpace I) bโ‚€) b = (tangentBundleCore I M).coordChange (achart H bโ‚€) (achart H b) b
          @[simp]
          theorem TangentBundle.coordChange_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) (x : F) :
          (tangentBundleCore (modelWithCornersSelf ๐•œ F) F).coordChange (achart F b) (achart F b') x = 1
          @[simp]
          theorem TangentBundle.symmL_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) :
          @[simp]
          theorem TangentBundle.continuousLinearMapAt_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (b : F) (b' : F) :
          instance tangentBundleCore.isSmooth {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
          (tangentBundleCore I M).IsSmooth I
          Equations
          • โ‹ฏ = โ‹ฏ
          instance TangentBundle.smoothVectorBundle {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] :
          Equations
          • โ‹ฏ = โ‹ฏ

          The tangent bundle to the model space #

          @[simp]
          theorem tangentBundle_model_space_chartAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :
          (chartAt (ModelProd H E) p).toPartialEquiv = (Bundle.TotalSpace.toProd H E).toPartialEquiv

          In the tangent bundle to the model space, the charts are just the canonical identification between a product type and a sigma type, a.k.a. TotalSpace.toProd.

          @[simp]
          theorem tangentBundle_model_space_coe_chartAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :
          โ†‘(chartAt (ModelProd H E) p) = โ‡‘(Bundle.TotalSpace.toProd H E)
          @[simp]
          theorem tangentBundle_model_space_coe_chartAt_symm {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (p : TangentBundle I H) :
          โ†‘(chartAt (ModelProd H E) p).symm = โ‡‘(Bundle.TotalSpace.toProd H E).symm
          theorem tangentBundleCore_coordChange_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) (x : H) (x' : H) (z : H) :
          (tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id ๐•œ E
          def tangentBundleModelSpaceHomeomorph {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :

          The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism

          Equations
          Instances For
            @[simp]
            theorem tangentBundleModelSpaceHomeomorph_coe {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :
            @[simp]
            theorem tangentBundleModelSpaceHomeomorph_coe_symm {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (H : Type u_4) [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) :
            theorem inCoordinates_tangent_bundle_core_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') (xโ‚€ : H) (x : H) (yโ‚€ : H') (y : H') (ฯ• : E โ†’L[๐•œ] E') :
            ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') xโ‚€ x yโ‚€ y ฯ• = ฯ•

            The map in_coordinates for the tangent bundle is trivial on the model spaces

            def inTangentCoordinates {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {N : Type u_9} (f : N โ†’ M) (g : N โ†’ M') (ฯ• : N โ†’ E โ†’L[๐•œ] E') :
            N โ†’ N โ†’ E โ†’L[๐•œ] E'

            When ฯ• x is a continuous linear map that changes vectors in charts around f x to vectors in charts around g x, inTangentCoordinates I I' f g ฯ• xโ‚€ x is a coordinate change of this continuous linear map that makes sense from charts around f xโ‚€ to charts around g xโ‚€ by composing it with appropriate coordinate changes. Note that the type of ฯ• is more accurately ฮ  x : N, TangentSpace I (f x) โ†’L[๐•œ] TangentSpace I' (g x). We are unfolding TangentSpace in this type so that Lean recognizes that the type of ฯ• doesn't actually depend on f or g.

            This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.

            Equations
            Instances For
              theorem inTangentCoordinates_model_space {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {N : Type u_9} (f : N โ†’ H) (g : N โ†’ H') (ฯ• : N โ†’ E โ†’L[๐•œ] E') (xโ‚€ : N) :
              inTangentCoordinates I I' f g ฯ• xโ‚€ = ฯ•
              theorem inTangentCoordinates_eq {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners ๐•œ E H) {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ๐•œ E' H') {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {N : Type u_9} (f : N โ†’ M) (g : N โ†’ M') (ฯ• : N โ†’ E โ†’L[๐•œ] E') {xโ‚€ : N} {x : N} (hx : f x โˆˆ (chartAt H (f xโ‚€)).source) (hy : g x โˆˆ (chartAt H' (g xโ‚€)).source) :
              inTangentCoordinates I I' f g ฯ• xโ‚€ x = ((tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g xโ‚€)) (g x)).comp ((ฯ• x).comp ((tangentBundleCore I M).coordChange (achart H (f xโ‚€)) (achart H (f x)) (f x)))