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 definen-dimensional real manifolds with boundarymodel_with_corners ℝ (euclidean_space (fin n)) (euclidean_quadrant n)for the model space used to definen-dimensional real manifolds with corners
Notations
In the locale manifold, we introduce the notations
𝓡 nfor the identity model with corners oneuclidean_space (fin n)𝓡∂ nformodel_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)].
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
- euclidean_half_space n = {x // 0 ≤ x 0}
The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative
coordinates.
Equations
- euclidean_quadrant n = {x // ∀ (i : fin n), 0 ≤ x i}
Equations
- euclidean_half_space.inhabited = {default := ⟨0, _⟩}
Equations
- euclidean_quadrant.inhabited = {default := ⟨0, _⟩}
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
- model_with_corners_euclidean_half_space n = {to_local_equiv := {to_fun := λ (x : euclidean_half_space n), x.val, inv_fun := λ (x : euclidean_space (fin n)), ⟨λ (i : fin n), dite (i = 0) (λ (h : i = 0), max (x i) 0) (λ (h : ¬i = 0), x i), _⟩, source := set.univ (euclidean_half_space n), target := set.range (λ (x : euclidean_half_space n), x.val), map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, source_eq := _, unique_diff' := _, continuous_to_fun := _, continuous_inv_fun := _}
Definition of the model with corners (euclidean_space (fin n), euclidean_quadrant n), used as a
model for manifolds with corners
Equations
- model_with_corners_euclidean_quadrant n = {to_local_equiv := {to_fun := λ (x : euclidean_quadrant n), x.val, inv_fun := λ (x : euclidean_space (fin n)), ⟨λ (i : fin n), max (x i) 0, _⟩, source := set.univ (euclidean_quadrant n), target := set.range (λ (x : euclidean_quadrant n), x.val), map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, source_eq := _, unique_diff' := _, continuous_to_fun := _, continuous_inv_fun := _}
The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in
euclidean_half_space 1.
Equations
- Icc_left_chart x y = {to_local_equiv := {to_fun := λ (z : ↥(set.Icc x y)), ⟨λ (i : fin 1), z.val - x, _⟩, inv_fun := λ (z : euclidean_half_space 1), ⟨min (z.val 0 + x) y, _⟩, source := {z : ↥(set.Icc x y) | z.val < y}, target := {z : euclidean_half_space 1 | z.val 0 < y - x}, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in
euclidean_half_space 1.
Equations
- Icc_right_chart x y = {to_local_equiv := {to_fun := λ (z : ↥(set.Icc x y)), ⟨λ (i : fin 1), y - z.val, _⟩, inv_fun := λ (z : euclidean_half_space 1), ⟨max (y - z.val 0) x, _⟩, source := {z : ↥(set.Icc x y) | x < z.val}, target := {z : euclidean_half_space 1 | z.val 0 < y - x}, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
Charted space structure on [x, y], using only two charts taking values in euclidean_half_space 1.
Equations
- Icc_manifold x y = {atlas := {Icc_left_chart x y, Icc_right_chart x y}, chart_at := λ (z : ↥(set.Icc x y)), ite (z.val < y) (Icc_left_chart x y) (Icc_right_chart x y), mem_chart_source := _, chart_mem_atlas := _}
The manifold structure on [x, y] is smooth.
Equations
Register the manifold structure on Icc 0 1, and also its zero and one.