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
modelWithCornersEuclideanHalfSpace n : ModelWithCorners β (EuclideanSpace β (Fin n)) (EuclideanHalfSpace n)
for the model space used to definen
-dimensional real manifolds with boundarymodelWithCornersEuclideanQuadrant n : ModelWithCorners β (EuclideanSpace β (Fin n)) (EuclideanQuadrant n)
for the model space used to definen
-dimensional real manifolds with corners
Notations #
In the locale Manifold
, we introduce the notations
π‘ n
for the identity model with corners onEuclideanSpace β (Fin n)
π‘β n
formodelWithCornersEuclideanHalfSpace n
.
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
- EuclideanHalfSpace n = { x : EuclideanSpace β (Fin n) // 0 β€ x 0 }
Instances For
The quadrant in β^n
, used to model manifolds with corners, made of all vectors with nonnegative
coordinates.
Equations
- EuclideanQuadrant n = { x : EuclideanSpace β (Fin n) // β (i : Fin n), 0 β€ x i }
Instances For
Equations
- instTopologicalSpaceEuclideanHalfSpace = instTopologicalSpaceSubtype
Equations
- instTopologicalSpaceEuclideanQuadrant = instTopologicalSpaceSubtype
Equations
- instInhabitedEuclideanHalfSpace = { default := β¨0, β―β© }
Equations
- instInhabitedEuclideanQuadrant = { default := β¨0, β―β© }
Alias of range_euclideanHalfSpace
.
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
- Manifold.termπ‘_ = Lean.ParserDescr.node `Manifold.termπ‘_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π‘ ") (Lean.ParserDescr.cat `term 0))
Instances For
Pretty printer defined by notation3
command.
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 with boundary.
Equations
- Manifold.Β«termπ‘β_Β» = Lean.ParserDescr.node `Manifold.Β«termπ‘β_Β» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π‘β ") (Lean.ParserDescr.cat `term 0))
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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.
Register the manifold structure on Icc 0 1
. These are merely special cases of
IccChartedSpace
and Icc_smoothManifoldWithCorners
.
Equations
- instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc = inferInstance