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], and prove that its boundary is indeed {x,y} whenever x < y. As a corollary, a product M Γ— [x, y] with a manifold M without boundary has boundary M Γ— {x, y}.

More specifically, we introduce

Notation #

In the scope 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 cannot be implicit, see the discussion in Geometry.Manifold.IsManifold).

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
      Equations
      theorem EuclideanQuadrant.ext {n : β„•} (x y : EuclideanQuadrant n) (h : ↑x = ↑y) :
      x = y
      theorem EuclideanQuadrant.ext_iff {n : β„•} {x y : EuclideanQuadrant n} :
      x = y ↔ ↑x = ↑y
      theorem EuclideanHalfSpace.ext {n : β„•} [NeZero n] (x y : EuclideanHalfSpace n) (h : ↑x = ↑y) :
      x = y
      theorem EuclideanHalfSpace.ext_iff {n : β„•} [NeZero n] {x y : EuclideanHalfSpace n} :
      x = y ↔ ↑x = ↑y
      @[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 closure_open_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 interior_euclideanQuadrant (n : β„•) (p : ENNReal) (a : ℝ) :
      interior {y : PiLp p fun (x : Fin n) => ℝ | βˆ€ (i : Fin n), a ≀ y i} = {y : PiLp p fun (x : Fin n) => ℝ | βˆ€ (i : Fin n), a < y i}

      Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n), used as a model for manifolds with boundary. In the scope 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
                theorem Fact.Manifold.instLeReal {x y : ℝ} [hxy : Fact (x < y)] :
                theorem iccLeftChart_extend_zero {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} :
                ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) p 0 = ↑p - x
                theorem IccLeftChart_extend_interior_pos {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} (hp : x < ↑p ∧ ↑p < y) :
                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 instIccChartedSpace (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.
                  @[simp]
                  theorem Icc_chartedSpaceChartAt {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} :
                  theorem Icc_chartedSpaceChartAt_of_le_top {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} (h : ↑z < y) :
                  theorem Icc_chartedSpaceChartAt_of_top_le {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} (h : y ≀ ↑z) :
                  theorem Icc_isInteriorPoint_interior {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} (hp : x < ↑p ∧ ↑p < y) :

                  A product M Γ— [x,y] for M boundaryless has boundary M Γ— {x, y}.

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

                  Register the manifold structure on Icc 0 1. These are merely special cases of instIccChartedSpace and instIsManifoldIcc.