# mathlibdocumentation

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

• model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space n) for the model space used to define n-dimensional real manifolds with boundary
• model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_quadrant n) for the model space used to define n-dimensional real manifolds with corners

## Notations #

In the locale manifold, we introduce the notations

• 𝓡 n for the identity model with corners on euclidean_space ℝ (fin n)
• 𝓡∂ n for model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space n).

For instance, if a manifold M is boundaryless, smooth and modelled on euclidean_space ℝ (fin m), and N is smooth with boundary modelled on euclidean_half_space 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 smooth_manifold_with_corners.lean).

## 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)].

def euclidean_half_space (n : ) [has_zero (fin n)] :
Type

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
• = {x // 0 x 0}
Instances for euclidean_half_space
def euclidean_quadrant (n : ) :
Type

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

Equations
• = {x // ∀ (i : fin n), 0 x i}
Instances for euclidean_quadrant
@[protected, instance]
noncomputable def euclidean_half_space.topological_space {n : } [has_zero (fin n)] :
Equations
@[protected, instance]
noncomputable def euclidean_quadrant.topological_space {n : } :
Equations
@[protected, instance]
noncomputable def euclidean_half_space.inhabited {n : } [has_zero (fin n)] :
Equations
@[protected, instance]
noncomputable def euclidean_quadrant.inhabited {n : } :
Equations
theorem range_half_space (n : ) [has_zero (fin n)] :
set.range (λ (x : , x.val) = {y : (fin n) | 0 y 0}
theorem range_quadrant (n : ) :
set.range (λ (x : , x.val) = {y : (fin n) | ∀ (i : fin n), 0 y i}
noncomputable def model_with_corners_euclidean_half_space (n : ) [has_zero (fin n)] :

Definition of the model with corners (euclidean_space ℝ (fin n), euclidean_half_space n), used as a model for manifolds with boundary. In the locale manifold, use the shortcut 𝓡∂ n.

Equations
Instances for model_with_corners_euclidean_half_space
noncomputable def model_with_corners_euclidean_quadrant (n : ) :

Definition of the model with corners (euclidean_space ℝ (fin n), euclidean_quadrant n), used as a model for manifolds with corners

Equations
noncomputable def Icc_left_chart (x y : ) [fact (x < y)] :

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

Equations
noncomputable def Icc_right_chart (x y : ) [fact (x < y)] :

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

Equations
@[protected, instance]
noncomputable def Icc_manifold (x y : ) [fact (x < y)] :
(set.Icc x y)

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

Equations
@[protected, instance]
def Icc_smooth_manifold (x y : ) [fact (x < y)] :

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

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

theorem fact_zero_lt_one  :
fact (0 < 1)
@[protected, instance]
noncomputable def set.Icc.charted_space  :
(set.Icc 0 1)
Equations
@[protected, instance]