mathlib3 documentation

geometry.manifold.instances.real

Constructing examples of manifolds over ℝ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)] :

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}

Instances for euclidean_half_space

def euclidean_quadrant (n : ℕ) :

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}

Instances for euclidean_quadrant

@[protected, instance]

noncomputable def euclidean_half_space.topological_space {n : ℕ} [has_zero (fin n)] :

topological_space (euclidean_half_space n)

Equations

euclidean_half_space.topological_space = subtype.topological_space

@[protected, instance]

noncomputable def euclidean_quadrant.topological_space {n : ℕ} :

topological_space (euclidean_quadrant n)

Equations

euclidean_quadrant.topological_space = subtype.topological_space

@[protected, instance]

noncomputable def euclidean_half_space.inhabited {n : ℕ} [has_zero (fin n)] :

inhabited (euclidean_half_space n)

Equations

euclidean_half_space.inhabited = {default := ⟨0, _⟩}

@[protected, instance]

noncomputable def euclidean_quadrant.inhabited {n : ℕ} :

inhabited (euclidean_quadrant n)

Equations

euclidean_quadrant.inhabited = {default := ⟨0, _⟩}

theorem range_half_space (n : ℕ) [has_zero (fin n)] :

set.range (λ (x : euclidean_half_space n), x.val) = {y : euclidean_space ℝ (fin n) | 0 ≤ y 0}

theorem range_quadrant (n : ℕ) :

set.range (λ (x : euclidean_quadrant n), x.val) = {y : euclidean_space ℝ (fin n) | ∀ (i : fin n), 0 ≤ y i}

noncomputable def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] :

model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space 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

model_with_corners_euclidean_half_space n = {to_local_equiv := {to_fun := subtype.val (λ (x : euclidean_space ℝ (fin n)), 0 ≤ x 0), inv_fun := λ (x : euclidean_space ℝ (fin n)), ⟨function.update x 0 (linear_order.max (x 0) 0), _⟩, source := set.univ (euclidean_half_space n), target := {x : euclidean_space ℝ (fin n) | 0 ≤ x 0}, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, source_eq := _, unique_diff' := _, continuous_to_fun := _, continuous_inv_fun := _}

Instances for model_with_corners_euclidean_half_space

noncomputable def model_with_corners_euclidean_quadrant (n : ℕ) :

model_with_corners ℝ (euclidean_space ℝ (fin n)) (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

model_with_corners_euclidean_quadrant n = {to_local_equiv := {to_fun := subtype.val (λ (x : euclidean_space ℝ (fin n)), ∀ (i : fin n), 0 ≤ x i), inv_fun := λ (x : euclidean_space ℝ (fin n)), ⟨λ (i : fin n), linear_order.max (x i) 0, _⟩, source := set.univ (euclidean_quadrant n), target := {x : euclidean_space ℝ (fin n) | ∀ (i : fin n), 0 ≤ x i}, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, source_eq := _, unique_diff' := _, continuous_to_fun := _, continuous_inv_fun := _}

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

local_homeomorph ↥(set.Icc x y) (euclidean_half_space 1)

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), ⟨linear_order.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 := _}

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

local_homeomorph ↥(set.Icc x y) (euclidean_half_space 1)

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), ⟨linear_order.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 := _}

@[protected, instance]

noncomputable def Icc_manifold (x y : ℝ) [fact (x < y)] :

charted_space (euclidean_half_space 1) ↥(set.Icc x y)

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 := _}

@[protected, instance]

def Icc_smooth_manifold (x y : ℝ) [fact (x < y)] :

smooth_manifold_with_corners (model_with_corners_euclidean_half_space 1) ↥(set.Icc x y)

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

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

@[protected, instance]

noncomputable def set.Icc.charted_space :

charted_space (euclidean_half_space 1) ↥(set.Icc 0 1)

Equations

set.Icc.charted_space = Icc_manifold 0 1

@[protected, instance]

def set.Icc.smooth_manifold_with_corners :

smooth_manifold_with_corners (model_with_corners_euclidean_half_space 1) ↥(set.Icc 0 1)