Theorems · Definition · global analysis

inTangentCoordinates

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        [IsManifold I 1 M] →
                                          [IsManifold I' 1 M'] →
                                            {N : Type u_9} → (N → M) → (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.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Tangent

Cited by

10 results in Mathlib

Foundations

Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpaceIsManifoldIsManifold