Documentation

Atlas.GeometryOfManifolds.code.CotangentBundleBridge

def CotangentBundle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] :
Type (max u_1 u_3)

The cotangent bundle $T^*M$ as the disjoint union $\bigsqcup_{x \in M} T^*_x M$ of cotangent spaces.

Instances For

    The bundle projection $\pi : T^*M \to M$, $(x, \xi) \mapsto x$.

    Instances For

      Builds a cotangent vector at $x \in M$ from a covector $\xi \in T^*_x M$.

      Instances For
        @[simp]
        theorem CotangentBundle.proj_mk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] (x : M) (ξ : TangentSpace I x →ₗ[] ) :
        proj I M (mk I M x ξ) = x

        Projection of a built cotangent vector returns its basepoint.

        @[implicit_reducible]

        The natural topology on $T^*M$ making the projection continuous (axiomatized).

        @[implicit_reducible]

        $T^*M$ inherits a charted space structure with model $H \times E$ (axiomatized).

        $T^*M$ is a smooth manifold with model $I \times \mathrm{id}_E$ (axiomatized).

        @[reducible, inline]
        noncomputable abbrev cotangentBundleModel {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {H : Type u} [TopologicalSpace H] (I : ModelWithCorners E H) :

        The model-with-corners for $T^*M$, namely $I \times \mathrm{id}_E$.

        Instances For
          @[reducible, inline]
          noncomputable abbrev CotangentBundleΩ {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {H : Type u} [TopologicalSpace H] (I : ModelWithCorners E H) (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (p : ) :

          The space of differential $p$-forms on the cotangent bundle $T^*M$.

          Instances For
            @[reducible, inline]
            noncomputable abbrev CotangentBundleVF {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {H : Type u} [TopologicalSpace H] (I : ModelWithCorners E H) (M : Type u) [TopologicalSpace M] [ChartedSpace H M] :

            The space of vector fields on the cotangent bundle $T^*M$.

            Instances For
              @[reducible]

              The DifferentialFormSpace structure on $T^*M$, induced from its manifold structure.

              Instances For
                @[implicit_reducible]

                Instance witness for the differential form space structure on the cotangent bundle.

                noncomputable def liouvilleForm {E : Type u} [NormedAddCommGroup E] [NormedSpace E] {H : Type u} [TopologicalSpace H] (I : ModelWithCorners E H) (M : Type u) [TopologicalSpace M] [ChartedSpace H M] :

                The canonical (Liouville/tautological) $1$-form $\theta$ on $T^*M$, defined locally by $\theta_{(x,\xi)} = \xi \circ d\pi$.

                Instances For

                  The canonical symplectic form $-d\theta$ on $T^*M$ is nondegenerate as a pairing on vector fields.

                  The cotangent bundle $T^*M$ equipped with its canonical symplectic structure $\omega_0 = d\theta$.

                  Instances For

                    The zero section $M \hookrightarrow T^*M$, $x \mapsto (x, 0)$, as a DFS-morphism.

                    Instances For

                      The Liouville form pulls back to zero along the zero section: $0^*\theta = 0$.

                      @[implicit_reducible]

                      Assembles all the data above into a CotangentBundleDFS structure for $T^*M$.

                      @[reducible, inline]

                      Convenience abbreviation for the CotangentBundleDFS structure of $T^*M$.

                      Instances For
                        noncomputable def cotangentOmega {EI : Type u} [NormedAddCommGroup EI] [NormedSpace EI] [FiniteDimensional EI] [Nontrivial EI] {HI : Type u} [TopologicalSpace HI] (I : ModelWithCorners EI HI) (M : Type u) [TopologicalSpace M] [ChartedSpace HI M] [IsManifold I (↑) M] :

                        The canonical symplectic $2$-form $\omega_0$ on $T^*M$.

                        Instances For
                          noncomputable def cotangentLiouville {EI : Type u} [NormedAddCommGroup EI] [NormedSpace EI] [FiniteDimensional EI] [Nontrivial EI] {HI : Type u} [TopologicalSpace HI] (I : ModelWithCorners EI HI) (M : Type u) [TopologicalSpace M] [ChartedSpace HI M] [IsManifold I (↑) M] :

                          The canonical Liouville $1$-form $\theta$ on $T^*M$.

                          Instances For

                            The canonical symplectic form on $T^*M$ is exact, $\omega_0 = d\theta$.