Documentation

Atlas.GeometryOfManifolds.code.ManifoldIntegration

A smooth manifold $M$ is compact and oriented: it carries a compact topology together with an (abstractly recorded) orientation, the standard hypothesis under which Stokes-type integration is defined.

Instances

    Projects out the underlying CompactSpace structure of a compact oriented manifold.

    For a compact oriented smooth manifold $(M, I)$, this produces the Stokes-style integration data on its differential form space: the integration map $\int_M : \Omega^{\dim M}(M) \to \mathbb{R}$ and associated pairings used to formulate Stokes' theorem.

    Instances For
      noncomputable def manifoldDim {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] [IsManifold I (↑) M] [IsCompactOrientedManifold I M] :

      The dimension $\dim M$ of the manifold $M$, as recorded by its Stokes integration data.

      Instances For
        noncomputable def manifoldIntegrate {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] [IsManifold I (↑) M] [IsCompactOrientedManifold I M] :
        ManifoldΩ I M (manifoldDim I M)

        The top-degree integration map $\int_M : \Omega^{\dim M}(M) \to \mathbb{R}$ on a compact oriented smooth manifold.

        Instances For
          noncomputable def manifold_period_pairing {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] [IsManifold I (↑) M] [IsCompactOrientedManifold I M] (p : ) :
          ManifoldΩ I M pManifoldΩ I M p

          The period pairing $\Omega^p(M) \times \Omega^p(M) \to \mathbb{R}$ induced by integration on $M$, generalising $\langle \alpha, \beta \rangle = \int_M \alpha \wedge \star \beta$.

          Instances For