Documentation

Mathlib.Geometry.Manifold.Instances.Real

Constructing examples of manifolds over ℝ #

We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless or with boundary or with corners. As a concrete example, we construct explicitly the manifold with boundary structure on the real interval [x, y].

More specifically, we introduce

Notations #

In the locale Manifold, we introduce the notations

For instance, if a manifold M is boundaryless, smooth and modelled on EuclideanSpace ℝ (Fin m), and N is smooth with boundary modelled on EuclideanHalfSpace n, and f : M β†’ N is a smooth map, then the derivative of f can be written simply as mfderiv (𝓑 m) (π“‘βˆ‚ n) f (as to why the model with corners can not be implicit, see the discussion in Geometry.Manifold.SmoothManifoldWithCorners).

Implementation notes #

The manifold structure on the interval [x, y] = Icc x y requires the assumption x < y as a typeclass. We provide it as [Fact (x < y)].

The half-space in ℝ^n, used to model manifolds with boundary. We only define it when 1 ≀ n, as the definition only makes sense in this case.

Equations
Instances For

    The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative coordinates.

    Equations
    Instances For
      Equations
      • instTopologicalSpaceEuclideanHalfSpace = instTopologicalSpaceSubtype
      Equations
      • instTopologicalSpaceEuclideanQuadrant = instTopologicalSpaceSubtype
      Equations
      • instInhabitedEuclideanHalfSpace = { default := ⟨0, β‹―βŸ© }
      Equations
      • instInhabitedEuclideanQuadrant = { default := ⟨0, β‹―βŸ© }
      theorem EuclideanQuadrant.ext_iff {n : β„•} {x : EuclideanQuadrant n} {y : EuclideanQuadrant n} :
      x = y ↔ ↑x = ↑y
      theorem EuclideanQuadrant.ext {n : β„•} (x : EuclideanQuadrant n) (y : EuclideanQuadrant n) (h : ↑x = ↑y) :
      x = y
      theorem EuclideanHalfSpace.ext_iff {n : β„•} [NeZero n] {x : EuclideanHalfSpace n} {y : EuclideanHalfSpace n} :
      x = y ↔ ↑x = ↑y
      theorem EuclideanHalfSpace.ext {n : β„•} [NeZero n] (x : EuclideanHalfSpace n) (y : EuclideanHalfSpace n) (h : ↑x = ↑y) :
      x = y
      theorem range_euclideanHalfSpace (n : β„•) [NeZero n] :
      (Set.range fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≀ y 0}
      @[deprecated range_euclideanHalfSpace]
      theorem range_half_space (n : β„•) [NeZero n] :
      (Set.range fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≀ y 0}

      Alias of range_euclideanHalfSpace.

      @[simp]
      theorem interior_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      interior {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a < y i}
      @[simp]
      theorem closure_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      closure {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i}
      @[simp]
      theorem frontier_halfspace {n : β„•} (p : ENNReal) (a : ℝ) (i : Fin n) :
      frontier {y : PiLp p fun (x : Fin n) => ℝ | a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | a = y i}
      theorem range_euclideanQuadrant (n : β„•) :
      (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | βˆ€ (i : Fin n), 0 ≀ y i}
      @[deprecated range_euclideanQuadrant]
      theorem range_quadrant (n : β„•) :
      (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | βˆ€ (i : Fin n), 0 ≀ y i}

      Alias of range_euclideanQuadrant.

      Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n), used as a model for manifolds with boundary. In the locale Manifold, use the shortcut π“‘βˆ‚ n.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanQuadrant n), used as a model for manifolds with corners

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The model space used to define n-dimensional real manifolds without boundary.

          Equations
          Instances For

            The model space used to define n-dimensional real manifolds with boundary.

            Equations
            Instances For
              def IccLeftChart (x : ℝ) (y : ℝ) [h : Fact (x < y)] :

              The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in EuclideanHalfSpace 1.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def IccRightChart (x : ℝ) (y : ℝ) [h : Fact (x < y)] :

                The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in EuclideanHalfSpace 1.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  instance IccManifold (x : ℝ) (y : ℝ) [h : Fact (x < y)] :

                  Charted space structure on [x, y], using only two charts taking values in EuclideanHalfSpace 1.

                  Equations
                  • One or more equations did not get rendered due to their size.

                  The manifold structure on [x, y] is smooth.

                  Equations
                  • β‹― = β‹―

                  Register the manifold structure on Icc 0 1, and also its zero and one.