Mathlib.Geometry.Manifold.IsManifold.Basic

Module docstring

{"# C^n manifolds (possibly with boundary or corners)

A C^n manifold is a manifold modelled on a normed vector space, or a subset like a half-space (to get manifolds with boundaries) for which the changes of coordinates are C^n maps. We define a model with corners as a map I : H → E embedding nicely the topological space H in the vector space E (or more precisely as a structure containing all the relevant properties). Given such a model with corners I on (E, H), we define the groupoid of local homeomorphisms of H which are C^n when read in E (for any regularity n : WithTop ℕ∞). With this groupoid at hand and the general machinery of charted spaces, we thus get the notion of C^n manifold with respect to any model with corners I on (E, H).

Some texts assume manifolds to be Hausdorff and second countable. We (in mathlib) assume neither, but add these assumptions later as needed. (Quite a few results still do not require them.)

Main definitions

ModelWithCorners 𝕜 E H : a structure containing information on the way a space H embeds in a model vector space E over the field 𝕜. This is all that is needed to define a C^n manifold with model space H, and model vector space E.
modelWithCornersSelf 𝕜 E : trivial model with corners structure on the space E embedded in itself by the identity.
contDiffGroupoid n I : when I is a model with corners on (𝕜, E, H), this is the groupoid of partial homeos of H which are of class C^n over the normed field 𝕜, when read in E.
IsManifold I n M : a type class saying that the charted space M, modelled on the space H, has C^n changes of coordinates with respect to the model with corners I on (𝕜, E, H). This type class is just a shortcut for HasGroupoid M (contDiffGroupoid n I).

We define a few constructions of smooth manifolds: * every empty type is a smooth manifold * the product of two smooth manifolds * the disjoint union of two manifolds (over the same charted space)

As specific examples of models with corners, we define (in Geometry.Manifold.Instances.Real) * modelWithCornersEuclideanHalfSpace n : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n) for the model space used to define n-dimensional real manifolds without boundary (with notation 𝓡 n in the locale Manifold) * modelWithCornersEuclideanHalfSpace n : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n) for the model space used to define n-dimensional real manifolds with boundary (with notation 𝓡∂ n in the locale Manifold) * modelWithCornersEuclideanQuadrant n : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n) for the model space used to define n-dimensional real manifolds with corners

With these definitions at hand, to invoke an n-dimensional C^∞ real manifold without boundary, one could use

variable {n : ℕ} {M : Type*} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M].

However, this is not the recommended way: a theorem proved using this assumption would not apply for instance to the tangent space of such a manifold, which is modelled on (EuclideanSpace ℝ (Fin n)) × (EuclideanSpace ℝ (Fin n)) and not on EuclideanSpace ℝ (Fin (2 * n))! In the same way, it would not apply to product manifolds, modelled on (EuclideanSpace ℝ (Fin n)) × (EuclideanSpace ℝ (Fin m)). The right invocation does not focus on one specific construction, but on all constructions sharing the right properties, like

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {I : ModelWithCorners ℝ E E} [I.Boundaryless] {M : Type*} [TopologicalSpace M] [ChartedSpace E M] [IsManifold I ∞ M]

Here, I.Boundaryless is a typeclass property ensuring that there is no boundary (this is for instance the case for modelWithCornersSelf, or products of these). Note that one could consider as a natural assumption to only use the trivial model with corners modelWithCornersSelf ℝ E, but again in product manifolds the natural model with corners will not be this one but the product one (and they are not defeq as (fun p : E × F ↦ (p.1, p.2)) is not defeq to the identity). So, it is important to use the above incantation to maximize the applicability of theorems.

Even better, if the result should apply in a parallel way to smooth manifolds and to analytic manifolds, the last typeclass should be replaced with [IsManifold I n M] for n : WithTop ℕ∞.

We also define TangentSpace I (x : M) as a type synonym of E, and TangentBundle I M as a type synonym for Π (x : M), TangentSpace I x (in the form of an abbrev of Bundle.TotalSpace E (TangentSpace I : M → Type _)). Apart from basic typeclasses on TangentSpace I x, nothing is proved about them in this file, but it is useful to have them available as definitions early on to get a clean import structure below. The smooth bundle structure is defined in VectorBundle.Tangent, while the definition is used to talk about manifold derivatives in MFDeriv.Basic, and neither file needs import the other.

Implementation notes

We want to talk about manifolds modelled on a vector space, but also on manifolds with boundary, modelled on a half space (or even manifolds with corners). For the latter examples, we still want to define smooth functions, tangent bundles, and so on. As smooth functions are well defined on vector spaces or subsets of these, one could take for model space a subtype of a vector space. With the drawback that the whole vector space itself (which is the most basic example) is not directly a subtype of itself: the inclusion of univ : Set E in Set E would show up in the definition, instead of id.

A good abstraction covering both cases it to have a vector space E (with basic example the Euclidean space), a model space H (with basic example the upper half space), and an embedding of H into E (which can be the identity for H = E, or Subtype.val for manifolds with corners). We say that the pair (E, H) with their embedding is a model with corners, and we encompass all the relevant properties (in particular the fact that the image of H in E should have unique differentials) in the definition of ModelWithCorners.

I have considered using the model with corners I as a typeclass argument, possibly outParam, to get lighter notations later on, but it did not turn out right, as on E × F there are two natural model with corners, the trivial (identity) one, and the product one, and they are not defeq and one needs to indicate to Lean which one we want to use. This means that when talking on objects on manifolds one will most often need to specify the model with corners one is using. For instance, the tangent bundle will be TangentBundle I M and the derivative will be mfderiv I I' f, instead of the more natural notations TangentBundle 𝕜 M and mfderiv 𝕜 f (the field has to be explicit anyway, as some manifolds could be considered both as real and complex manifolds). ","### Models with corners. ","### C^n functions on models with corners ","### C^n manifolds (possibly with boundary or corners) "}

ModelWithCorners structure

(𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] extends
    PartialEquiv H E

Full source

/-- A structure containing information on the way a space `H` embeds in a
model vector space `E` over the field `𝕜`. This is all what is needed to
define a `C^n` manifold with model space `H`, and model vector space `E`.

We require two conditions `uniqueDiffOn'` and `target_subset_closure_interior`, which
are satisfied in the relevant cases (where `range I = univ` or a half space or a quadrant) and
useful for technical reasons. The former makes sure that manifold derivatives are uniquely
defined, the latter ensures that for `C^2` maps the second derivatives are symmetric even for points
on the boundary, as these are limit points of interior points where symmetry holds. If further
conditions turn out to be useful, they can be added here.
-/
@[ext]
structure ModelWithCorners (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] extends
    PartialEquiv H E where
  source_eq : source = univ
  uniqueDiffOn' : UniqueDiffOn 𝕜 toPartialEquiv.target
  target_subset_closure_interior : toPartialEquiv.target ⊆ closure (interior toPartialEquiv.target)
  continuous_toFun : Continuous toFun := by continuity
  continuous_invFun : Continuous invFun := by continuity

Model with Corners

Informal description

A model with corners is a structure that describes how a topological space $H$ embeds into a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$. It consists of a partial equivalence (a local homeomorphism) between $H$ and $E$, along with additional properties ensuring that the embedding behaves well for defining $C^n$ manifolds. Specifically, it requires that the embedding satisfies `uniqueDiffOn'` (ensuring unique derivatives) and `target_subset_closure_interior` (ensuring symmetry of second derivatives even at boundary points). This structure is fundamental for defining manifolds with boundaries or corners, where $H$ could be a half-space or a quadrant in $E$.

modelWithCornersSelf definition

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E

Full source

/-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace. -/
def modelWithCornersSelf (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ModelWithCorners 𝕜 E E where
  toPartialEquiv := PartialEquiv.refl E
  source_eq := rfl
  uniqueDiffOn' := uniqueDiffOn_univ
  target_subset_closure_interior := by simp
  continuous_toFun := continuous_id
  continuous_invFun := continuous_id

Trivial model with corners on a normed vector space

Informal description

The trivial model with corners structure on a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, where the embedding is the identity map from $E$ to itself. This structure is denoted as $\mathcal{I}(\mathbb{K}, E)$ in the `Manifold` namespace.

Manifold.term𝓘(_,_) definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped[Manifold] notation "𝓘(" 𝕜 ", " E ")" => modelWithCornersSelf 𝕜 E

Notation for trivial model with corners

Informal description

The notation `𝓘(𝕜, E)` represents the trivial model with corners structure on a normed vector space `E` over a nontrivially normed field `𝕜`, where the embedding is the identity map from `E` to itself. This is equivalent to `modelWithCornersSelf 𝕜 E`.

Manifold.term𝓘(_) definition

: Lean.ParserDescr✝

Full source

/-- A normed field is a model with corners. -/
scoped[Manifold] notation "𝓘(" 𝕜 ")" => modelWithCornersSelf 𝕜 𝕜

Trivial model with corners for a normed field

Informal description

The notation `𝓘(𝕜)` represents the trivial model with corners structure on a normed field `𝕜`, where the space is embedded in itself via the identity map. This serves as the simplest case of a model with corners, where the model space `H` and the vector space `E` are both equal to `𝕜`.

ModelWithCorners.toFun' definition

(e : ModelWithCorners 𝕜 E H) : H → E

Full source

/-- Coercion of a model with corners to a function. We don't use `e.toFun` because it is actually
`e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`. While we may want to
switch to this behavior later, doing it mid-port will break a lot of proofs. -/
@[coe] def toFun' (e : ModelWithCorners 𝕜 E H) : H → E := e.toFun

Embedding function of a model with corners

Informal description

Given a model with corners $I$ on $(𝕜, E, H)$, the function maps a point $x$ in the model space $H$ to its image in the normed vector space $E$ under the embedding defined by $I$.

ModelWithCorners.instCoeFunForall instance

: CoeFun (ModelWithCorners 𝕜 E H) fun _ => H → E

Full source

instance : CoeFun (ModelWithCorners 𝕜 E H) fun _ => H → E := ⟨toFun'⟩

Model with Corners as a Function

Informal description

For any model with corners $I$ on $(\mathbb{K}, E, H)$, the structure $I$ can be treated as a function from the topological space $H$ to the normed vector space $E$.

ModelWithCorners.symm definition

: PartialEquiv E H

Full source

/-- The inverse to a model with corners, only registered as a `PartialEquiv`. -/
protected def symm : PartialEquiv E H :=
  I.toPartialEquiv.symm

Inverse model with corners

Informal description

The inverse of the model with corners `I`, represented as a partial equivalence from the normed vector space `E` back to the topological space `H`. This partial equivalence is obtained by taking the symmetric version of the partial equivalence associated with `I`.

ModelWithCorners.Simps.apply definition

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*)
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : H → E

Full source

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections. -/
def Simps.apply (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : H → E :=
  I

Embedding function of a model with corners

Informal description

Given a model with corners $I$ on $(\mathbb{K}, E, H)$, where $\mathbb{K}$ is a nontrivially normed field, $E$ is a normed vector space over $\mathbb{K}$, and $H$ is a topological space, the function maps a point $x$ in $H$ to its image in $E$ under the embedding defined by $I$.

ModelWithCorners.Simps.symm_apply definition

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*)
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : E → H

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : E → H :=
  I.symm

Inverse embedding of model with corners

Informal description

The function maps an element $x$ in the normed vector space $E$ to its corresponding element in the topological space $H$ under the inverse of the model with corners $I$.

ModelWithCorners.toPartialEquiv_coe theorem

: (I.toPartialEquiv : H → E) = I

Full source

@[simp, mfld_simps]
theorem toPartialEquiv_coe : (I.toPartialEquiv : H → E) = I :=
  rfl

Equality of Model Embedding and Partial Equivalence Function

Informal description

For a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, the underlying partial equivalence's embedding function from $H$ to $E$ coincides with $I$ itself as a function. In other words, the map $I : H \to E$ is equal to the embedding function defined by the partial equivalence associated with $I$.

ModelWithCorners.mk_coe theorem

 (e : PartialEquiv H E) (a b c d d') :
  ((ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E)

Full source

@[simp, mfld_simps]
theorem mk_coe (e : PartialEquiv H E) (a b c d d') :
    ((ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E) :=
  rfl

Embedding Function Equality in ModelWithCorners Construction

Informal description

Let $H$ and $E$ be types with $E$ being a normed vector space over a nontrivially normed field $\mathbb{K}$. Given a partial equivalence $e$ between $H$ and $E$ (with source in $H$ and target in $E$), and additional properties $a, b, c, d, d'$, the embedding function of the constructed model with corners $I := \text{ModelWithCorners.mk}~e~a~b~c~d~d'$ equals the underlying function of the partial equivalence $e$, i.e., $I = e$ as functions from $H$ to $E$.

ModelWithCorners.toPartialEquiv_coe_symm theorem

: (I.toPartialEquiv.symm : E → H) = I.symm

Full source

@[simp, mfld_simps]
theorem toPartialEquiv_coe_symm : (I.toPartialEquiv.symm : E → H) = I.symm :=
  rfl

Equality of Inverse Embedding Functions in Model with Corners

Informal description

For a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, the underlying function of the inverse partial equivalence $I^{-1}$ equals the inverse embedding function $I^{-1} : E \to H$.

ModelWithCorners.mk_symm theorem

(e : PartialEquiv H E) (a b c d d') : (ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H).symm = e.symm

Full source

@[simp, mfld_simps]
theorem mk_symm (e : PartialEquiv H E) (a b c d d') :
    (ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H).symm = e.symm :=
  rfl

Inverse of Constructed Model with Corners Equals Inverse Partial Equivalence

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ be a normed vector space over $\mathbb{K}$, and $H$ be a topological space. Given a partial equivalence $e$ between $H$ and $E$ (represented as `PartialEquiv H E`) and additional properties $a, b, c, d, d'$, the inverse of the model with corners constructed from $e$ equals the inverse of $e$. In other words, for the model with corners $I = \text{ModelWithCorners.mk}\ e\ a\ b\ c\ d\ d'$, we have $I^{-1} = e^{-1}$.

ModelWithCorners.continuous theorem

: Continuous I

Full source

@[continuity]
protected theorem continuous : Continuous I :=
  I.continuous_toFun

Continuity of the Model with Corners Embedding

Informal description

The embedding function $I : H \to E$ of a model with corners is continuous.

ModelWithCorners.continuousAt theorem

{x} : ContinuousAt I x

Full source

protected theorem continuousAt {x} : ContinuousAt I x :=
  I.continuous.continuousAt

Continuity of Model with Corners Embedding at a Point

Informal description

For any model with corners $I \colon H \to E$ and any point $x \in H$, the embedding $I$ is continuous at $x$.

ModelWithCorners.continuousWithinAt theorem

{s x} : ContinuousWithinAt I s x

Full source

protected theorem continuousWithinAt {s x} : ContinuousWithinAt I s x :=
  I.continuousAt.continuousWithinAt

Continuity of Model with Corners Embedding Within a Subset at a Point

Informal description

For any model with corners $I \colon H \to E$ between topological spaces, any subset $s \subseteq H$, and any point $x \in H$, the embedding $I$ is continuous within $s$ at $x$.

ModelWithCorners.continuous_symm theorem

: Continuous I.symm

Full source

@[continuity]
theorem continuous_symm : Continuous I.symm :=
  I.continuous_invFun

Continuity of the Inverse Model with Corners

Informal description

The inverse map $I^{-1} : E \to H$ of the model with corners $I : H \to E$ is continuous.

ModelWithCorners.continuousAt_symm theorem

{x} : ContinuousAt I.symm x

Full source

theorem continuousAt_symm {x} : ContinuousAt I.symm x :=
  I.continuous_symm.continuousAt

Continuity of the Inverse Model with Corners at a Point

Informal description

For any model with corners $I : H \to E$ and any point $x$ in the codomain $E$, the inverse map $I^{-1}$ is continuous at $x$.

ModelWithCorners.continuousWithinAt_symm theorem

{s x} : ContinuousWithinAt I.symm s x

Full source

theorem continuousWithinAt_symm {s x} : ContinuousWithinAt I.symm s x :=
  I.continuous_symm.continuousWithinAt

Continuity of Inverse Model with Corners Within Subset at Point

Informal description

Let $I : H \to E$ be a model with corners embedding a topological space $H$ into a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$. For any subset $s \subseteq E$ and any point $x \in E$, the inverse map $I^{-1} : E \to H$ is continuous within $s$ at $x$.

ModelWithCorners.continuousOn_symm theorem

{s} : ContinuousOn I.symm s

Full source

theorem continuousOn_symm {s} : ContinuousOn I.symm s :=
  I.continuous_symm.continuousOn

Continuity of the Inverse Model with Corners on Subsets

Informal description

For any subset $s$ of the target space $E$, the inverse map $I^{-1}$ of the model with corners $I \colon H \to E$ is continuous on $s$.

ModelWithCorners.target_eq theorem

: I.target = range (I : H → E)

Full source

@[simp, mfld_simps]
theorem target_eq : I.target = range (I : H → E) := by
  rw [← image_univ, ← I.source_eq]
  exact I.image_source_eq_target.symm

Target Equals Range for Model with Corners

Informal description

For a model with corners $I \colon H \to E$, the target set of $I$ is equal to the range of the embedding function $I \colon H \to E$, i.e., $I.\text{target} = \text{range}(I)$.

ModelWithCorners.uniqueDiffOn theorem

: UniqueDiffOn 𝕜 (range I)

Full source

protected theorem uniqueDiffOn : UniqueDiffOn 𝕜 (range I) :=
  I.target_eq ▸ I.uniqueDiffOn'

Uniqueness of Derivatives on the Range of a Model with Corners

Informal description

For a model with corners $I \colon H \to E$ over a nontrivially normed field $\mathbb{K}$, the range of $I$ in $E$ has the property that at every point in this range, the derivative (if it exists) is unique. In other words, the range $\text{range}(I)$ is a subset of $E$ where the notion of differentiability is well-defined in the sense that tangent directions are uniquely determined.

ModelWithCorners.range_subset_closure_interior theorem

: range I ⊆ closure (interior (range I))

Full source

theorem range_subset_closure_interior : rangerange I ⊆ closure (interior (range I)) := by
  rw [← I.target_eq]
  exact I.target_subset_closure_interior

Range of Model with Corners is Contained in Closure of Interior

Informal description

For a model with corners $I \colon H \to E$, the range of $I$ is contained in the closure of its interior, i.e., $\text{range}(I) \subseteq \overline{\text{interior}(\text{range}(I))}$.

ModelWithCorners.left_inv theorem

(x : H) : I.symm (I x) = x

Full source

@[simp, mfld_simps]
protected theorem left_inv (x : H) : I.symm (I x) = x := by refine I.left_inv' ?_; simp

Left Inverse Property of Model with Corners

Informal description

For any model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, and for any point $x \in H$, the inverse map $I^{-1}$ of $I$ satisfies $I^{-1}(I(x)) = x$.

ModelWithCorners.leftInverse theorem

: LeftInverse I.symm I

Full source

protected theorem leftInverse : LeftInverse I.symm I :=
  I.left_inv

Left Inverse Property of Model with Corners Embedding

Informal description

For a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, the inverse map $I^{-1}$ is a left inverse of $I$, meaning that $I^{-1} \circ I$ is the identity map on $H$.

ModelWithCorners.injective theorem

: Injective I

Full source

theorem injective : Injective I :=
  I.leftInverse.injective

Injectivity of the Model with Corners Embedding

Informal description

The embedding map $I : H \to E$ of a model with corners is injective.

ModelWithCorners.symm_comp_self theorem

: I.symm ∘ I = id

Full source

@[simp, mfld_simps]
theorem symm_comp_self : I.symm ∘ I = id :=
  I.leftInverse.comp_eq_id

Inverse Composition Yields Identity for Model with Corners

Informal description

For a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, the composition of the inverse map $I^{-1}$ with $I$ is equal to the identity map on $H$, i.e., $I^{-1} \circ I = \text{id}_H$.

ModelWithCorners.rightInvOn theorem

: RightInvOn I.symm I (range I)

Full source

protected theorem rightInvOn : RightInvOn I.symm I (range I) :=
  I.leftInverse.rightInvOn_range

Right Inverse Property of Model with Corners on its Range

Informal description

For a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$, the inverse map $I^{-1}$ is a right inverse of $I$ on the range of $I$, meaning that for every $x$ in the range of $I$, we have $I(I^{-1}(x)) = x$.

ModelWithCorners.right_inv theorem

{x : E} (hx : x ∈ range I) : I (I.symm x) = x

Full source

@[simp, mfld_simps]
protected theorem right_inv {x : E} (hx : x ∈ range I) : I (I.symm x) = x :=
  I.rightInvOn hx

Right Inverse Property of Model with Corners Embedding

Informal description

For any point $x$ in the range of the embedding $I : H \to E$ of a model with corners, applying $I$ to the inverse image $I^{-1}(x)$ yields back $x$, i.e., $I(I^{-1}(x)) = x$.

ModelWithCorners.preimage_image theorem

(s : Set H) : I ⁻¹' (I '' s) = s

Full source

theorem preimage_image (s : Set H) : I ⁻¹' (I '' s) = s :=
  I.injective.preimage_image s

Preimage-Image Identity for Model with Corners: $I^{-1}(I(s)) = s$

Informal description

For any model with corners $I : H \to E$ and any subset $s \subseteq H$, the preimage of the image of $s$ under $I$ equals $s$ itself, i.e., $I^{-1}(I(s)) = s$.

ModelWithCorners.image_eq theorem

(s : Set H) : I '' s = I.symm ⁻¹' s ∩ range I

Full source

protected theorem image_eq (s : Set H) : I '' s = I.symm ⁻¹' sI.symm ⁻¹' s ∩ range I := by
  refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_
  · rw [I.source_eq]; exact subset_univ _
  · rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]

Image-Preimage-Range Identity for Model with Corners

Informal description

For a model with corners $I \colon H \to E$ and any subset $s \subseteq H$, the image of $s$ under $I$ equals the intersection of the preimage of $s$ under the inverse map $I^{-1}$ with the range of $I$. In symbols: $$ I(s) = I^{-1}(s) \cap \text{range}(I). $$

ModelWithCorners.isClosedEmbedding theorem

: IsClosedEmbedding I

Full source

theorem isClosedEmbedding : IsClosedEmbedding I :=
  I.leftInverse.isClosedEmbedding I.continuous_symm I.continuous

Closed Embedding Property of Model with Corners

Informal description

The embedding map $I : H \to E$ of a model with corners is a closed embedding, meaning it is a continuous injective map with closed image in $E$ and induces the topology on $H$ from $E$.

ModelWithCorners.isClosed_range theorem

: IsClosed (range I)

Full source

theorem isClosed_range : IsClosed (range I) :=
  I.isClosedEmbedding.isClosed_range

Closed Range Property of Model with Corners Embedding

Informal description

The range of the embedding map $I : H \to E$ of a model with corners is a closed subset of the normed vector space $E$.

ModelWithCorners.range_eq_closure_interior theorem

: range I = closure (interior (range I))

Full source

theorem range_eq_closure_interior : range I = closure (interior (range I)) :=
  Subset.antisymm I.range_subset_closure_interior I.isClosed_range.closure_interior_subset

Range of Model with Corners Equals Closure of Interior

Informal description

For a model with corners $I \colon H \to E$, the range of $I$ equals the closure of its interior, i.e., $\text{range}(I) = \overline{\text{interior}(\text{range}(I))}$.

ModelWithCorners.map_nhds_eq theorem

(x : H) : map I (𝓝 x) = 𝓝[range I] I x

Full source

theorem map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] I x :=
  I.isClosedEmbedding.isEmbedding.map_nhds_eq x

Neighborhood Filter Preservation under Model with Corners Embedding

Informal description

For any point $x$ in the model space $H$, the pushforward of the neighborhood filter of $x$ under the embedding map $I \colon H \to E$ equals the neighborhood filter of $I(x)$ restricted to the range of $I$. In other words: $$ I_*(\mathcal{N}_x) = \mathcal{N}_{I(x)}|_{\text{range}(I)} $$ where $\mathcal{N}_x$ denotes the neighborhood filter at $x$ and $I_*$ denotes the pushforward under $I$.

ModelWithCorners.map_nhdsWithin_eq theorem

(s : Set H) (x : H) : map I (𝓝[s] x) = 𝓝[I '' s] I x

Full source

theorem map_nhdsWithin_eq (s : Set H) (x : H) : map I (𝓝[s] x) = 𝓝[I '' s] I x :=
  I.isClosedEmbedding.isEmbedding.map_nhdsWithin_eq s x

Neighborhood Filter Preservation Under Model with Corners Embedding

Informal description

Let $I : H \to E$ be a model with corners embedding a topological space $H$ into a normed vector space $E$. For any subset $s \subseteq H$ and any point $x \in H$, the image under $I$ of the neighborhood filter of $x$ within $s$ equals the neighborhood filter of $I(x)$ within the image $I(s)$ in $E$. In other words, $I_*(\mathcal{N}_s(x)) = \mathcal{N}_{I(s)}(I(x))$.

ModelWithCorners.image_mem_nhdsWithin theorem

{x : H} {s : Set H} (hs : s ∈ 𝓝 x) : I '' s ∈ 𝓝[range I] I x

Full source

theorem image_mem_nhdsWithin {x : H} {s : Set H} (hs : s ∈ 𝓝 x) : I '' sI '' s ∈ 𝓝[range I] I x :=
  I.map_nhds_eq x ▸ image_mem_map hs

Image of Neighborhood is Neighborhood in Model with Corners

Informal description

Let $I : H \to E$ be a model with corners embedding a topological space $H$ into a normed vector space $E$. For any point $x \in H$ and any neighborhood $s$ of $x$ in $H$, the image $I(s)$ is a neighborhood of $I(x)$ within the range of $I$ in $E$. In other words, if $s$ is a neighborhood of $x$, then $I(s)$ is a neighborhood of $I(x)$ in the subspace topology on $\text{range}(I)$.

ModelWithCorners.symm_map_nhdsWithin_image theorem

{x : H} {s : Set H} : map I.symm (𝓝[I '' s] I x) = 𝓝[s] x

Full source

theorem symm_map_nhdsWithin_image {x : H} {s : Set H} : map I.symm (𝓝[I '' s] I x) = 𝓝[s] x := by
  rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]

Inverse Model with Corners Preserves Neighborhood Filters: $(I^{-1})_*(\mathcal{N}_{I(s)}(I(x))) = \mathcal{N}_s(x)$

Informal description

Let $I : H \to E$ be a model with corners embedding a topological space $H$ into a normed vector space $E$. For any point $x \in H$ and any subset $s \subseteq H$, the preimage under $I^{-1}$ of the neighborhood filter of $I(x)$ within the image $I(s)$ equals the neighborhood filter of $x$ within $s$. In other words, $(I^{-1})_*(\mathcal{N}_{I(s)}(I(x))) = \mathcal{N}_s(x)$.

ModelWithCorners.symm_map_nhdsWithin_range theorem

(x : H) : map I.symm (𝓝[range I] I x) = 𝓝 x

Full source

theorem symm_map_nhdsWithin_range (x : H) : map I.symm (𝓝[range I] I x) = 𝓝 x := by
  rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]

Inverse Model with Corners Preserves Neighborhood Filters

Informal description

For any point $x$ in the model space $H$, the pushforward of the neighborhood filter of $I(x)$ restricted to the range of $I$ under the inverse map $I^{-1}$ equals the neighborhood filter of $x$ in $H$. In other words: $$ I^{-1}_*(\mathcal{N}_{I(x)}|_{\text{range}(I)}) = \mathcal{N}_x $$ where $\mathcal{N}_x$ denotes the neighborhood filter at $x$ and $I^{-1}_*$ denotes the pushforward under $I^{-1}$.

ModelWithCorners.uniqueDiffOn_preimage theorem

{s : Set H} (hs : IsOpen s) : UniqueDiffOn 𝕜 (I.symm ⁻¹' s ∩ range I)

Full source

theorem uniqueDiffOn_preimage {s : Set H} (hs : IsOpen s) :
    UniqueDiffOn 𝕜 (I.symm ⁻¹' sI.symm ⁻¹' s ∩ range I) := by
  rw [inter_comm]
  exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

Uniqueness of derivatives on preimage of open sets under model with corners

Informal description

Let $I : H \to E$ be a model with corners over a nontrivially normed field $\mathbb{K}$, where $E$ is a normed vector space and $H$ is a topological space. For any open subset $s \subseteq H$, the intersection of the preimage of $s$ under the inverse model $I^{-1}$ with the range of $I$ in $E$ has unique derivatives everywhere. In other words, the set $I^{-1}(s) \cap \text{range}(I) \subseteq E$ satisfies the property that at each of its points, derivatives (if they exist) are uniquely determined.

ModelWithCorners.uniqueDiffOn_preimage_source theorem

 {β : Type*} [TopologicalSpace β] {e : PartialHomeomorph H β} : UniqueDiffOn 𝕜 (I.symm ⁻¹' e.source ∩ range I)

Full source

theorem uniqueDiffOn_preimage_source {β : Type*} [TopologicalSpace β] {e : PartialHomeomorph H β} :
    UniqueDiffOn 𝕜 (I.symm ⁻¹' e.sourceI.symm ⁻¹' e.source ∩ range I) :=
  I.uniqueDiffOn_preimage e.open_source

Uniqueness of Derivatives on Preimage of Partial Homeomorphism Source under Model with Corners

Informal description

Let $I \colon H \to E$ be a model with corners over a nontrivially normed field $\mathbb{K}$, where $E$ is a normed vector space and $H$ is a topological space. For any partial homeomorphism $e$ from $H$ to another topological space $\beta$, the intersection of the preimage of $e$'s source under $I^{-1}$ with the range of $I$ in $E$ has unique derivatives everywhere. In other words, the set $I^{-1}(e.\text{source}) \cap \text{range}(I) \subseteq E$ satisfies the property that at each of its points, derivatives (if they exist) are uniquely determined.

ModelWithCorners.uniqueDiffWithinAt_image theorem

{x : H} : UniqueDiffWithinAt 𝕜 (range I) (I x)

Full source

theorem uniqueDiffWithinAt_image {x : H} : UniqueDiffWithinAt 𝕜 (range I) (I x) :=
  I.uniqueDiffOn _ (mem_range_self _)

Uniqueness of Derivatives at Points in the Range of a Model with Corners

Informal description

For any point $x$ in the model space $H$ of a model with corners $I \colon H \to E$ over a nontrivially normed field $\mathbb{K}$, the image $I(x)$ in the normed vector space $E$ has a unique derivative within the range of $I$. In other words, the tangent space at $I(x)$ is well-defined when considering directions within $\text{range}(I)$.

ModelWithCorners.symm_continuousWithinAt_comp_right_iff theorem

 {X} [TopologicalSpace X] {f : H → X} {s : Set H} {x : H} :
  ContinuousWithinAt (f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x) ↔ ContinuousWithinAt f s x

Full source

theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H → X} {s : Set H}
    {x : H} :
    ContinuousWithinAtContinuousWithinAt (f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x) ↔ ContinuousWithinAt f s x := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
    simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
      inter_univ] at this
    rwa [Function.comp_assoc, I.symm_comp_self] at this
  · rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm inter_subset_left

Equivalence of Continuity for Composition with Model with Corners Inverse

Informal description

Let $I \colon H \to E$ be a model with corners embedding a topological space $H$ into a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$. For any topological space $X$, function $f \colon H \to X$, subset $s \subseteq H$, and point $x \in H$, the composition $f \circ I^{-1}$ is continuous within $I^{-1}(s) \cap \text{range}(I)$ at $I(x)$ if and only if $f$ is continuous within $s$ at $x$.

ModelWithCorners.locallyCompactSpace theorem

[LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) : LocallyCompactSpace H

Full source

protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) :
    LocallyCompactSpace H := by
  have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x)s ∈ 𝓝 (I x) ∧ IsCompact s)
      fun s => I.symm '' (s ∩ range I) := fun x ↦ by
    rw [← I.symm_map_nhdsWithin_range]
    exact ((compact_basis_nhds (I x)).inf_principal _).map _
  refine .of_hasBasis this ?_
  rintro x s ⟨-, hsc⟩
  exact (hsc.inter_right I.isClosed_range).image I.continuous_symm

Local Compactness of Model Space via Model with Corners

Informal description

Let $E$ be a locally compact normed vector space over a nontrivially normed field $\mathbb{K}$, and let $I : H \to E$ be a model with corners embedding the topological space $H$ into $E$. Then $H$ is also locally compact.

ModelWithCorners.secondCountableTopology theorem

[SecondCountableTopology E] (I : ModelWithCorners 𝕜 E H) : SecondCountableTopology H

Full source

protected theorem secondCountableTopology [SecondCountableTopology E] (I : ModelWithCorners 𝕜 E H) :
    SecondCountableTopology H :=
  I.isClosedEmbedding.isEmbedding.secondCountableTopology

Second-Countability of Model Space via Model with Corners

Informal description

Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$ with a second-countable topology, and let $I : H \to E$ be a model with corners embedding the topological space $H$ into $E$. Then $H$ inherits a second-countable topology from $E$.

ModelWithCorners.t1Space theorem

(M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M

Full source

/-- Every manifold is a Fréchet space (T1 space) -- regardless of whether it is
Hausdorff. -/
protected theorem t1Space (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M := by
  have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
  exact ChartedSpace.t1Space H M

Charted spaces are T₁ spaces

Informal description

Let $M$ be a topological space equipped with a charted space structure over a model space $H$ (which is embedded in a normed vector space $E$ via a model with corners). Then $M$ is a T₁ space (Fréchet space), meaning every singleton set in $M$ is closed.

modelWithCornersSelf_partialEquiv theorem

: 𝓘(𝕜, E).toPartialEquiv = PartialEquiv.refl E

Full source

/-- In the trivial model with corners, the associated `PartialEquiv` is the identity. -/
@[simp, mfld_simps]
theorem modelWithCornersSelf_partialEquiv : 𝓘(𝕜, E).toPartialEquiv = PartialEquiv.refl E :=
  rfl

Partial Equivalence Relation for Trivial Model with Corners is Identity

Informal description

For the trivial model with corners $\mathcal{I}(\mathbb{K}, E)$ on a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, the associated partial equivalence relation is the identity partial equivalence on $E$.

modelWithCornersSelf_coe theorem

: (𝓘(𝕜, E) : E → E) = id

Full source

@[simp, mfld_simps]
theorem modelWithCornersSelf_coe : (𝓘(𝕜, E) : E → E) = id :=
  rfl

Trivial Model Embedding is Identity

Informal description

The embedding function of the trivial model with corners $\mathcal{I}(\mathbb{K}, E)$ from a normed vector space $E$ to itself is equal to the identity function, i.e., $\mathcal{I}(\mathbb{K}, E)(x) = x$ for all $x \in E$.

modelWithCornersSelf_coe_symm theorem

: (𝓘(𝕜, E).symm : E → E) = id

Full source

@[simp, mfld_simps]
theorem modelWithCornersSelf_coe_symm : (𝓘(𝕜, E).symm : E → E) = id :=
  rfl

Inverse of Trivial Model with Corners is Identity

Informal description

For the trivial model with corners $\mathcal{I}(\mathbb{K}, E)$ on a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, the inverse embedding map $\mathcal{I}(\mathbb{K}, E)^{-1} : E \to E$ is equal to the identity function.

ModelWithCorners.prod definition

 {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') : ModelWithCorners 𝕜 (E × E') (ModelProd H H')

Full source

/-- Given two model_with_corners `I` on `(E, H)` and `I'` on `(E', H')`, we define the model with
corners `I.prod I'` on `(E × E', ModelProd H H')`. This appears in particular for the manifold
structure on the tangent bundle to a manifold modelled on `(E, H)`: it will be modelled on
`(E × E, H × E)`. See note [Manifold type tags] for explanation about `ModelProd H H'`
vs `H × H'`. -/
@[simps -isSimp]
def ModelWithCorners.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) {E' : Type v'} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
    {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') :
    ModelWithCorners 𝕜 (E × E') (ModelProd H H') :=
  { I.toPartialEquiv.prod I'.toPartialEquiv with
    toFun := fun x => (I x.1, I' x.2)
    invFun := fun x => (I.symm x.1, I'.symm x.2)
    source := { x | x.1 ∈ I.source ∧ x.2 ∈ I'.source }
    source_eq := by simp only [setOf_true, mfld_simps]
    uniqueDiffOn' := I.uniqueDiffOn'.prod I'.uniqueDiffOn'
    target_subset_closure_interior := by
      simp only [PartialEquiv.prod_target, target_eq, interior_prod_eq, closure_prod_eq]
      exact Set.prod_mono I.range_subset_closure_interior I'.range_subset_closure_interior
    continuous_toFun := I.continuous_toFun.prodMap I'.continuous_toFun
    continuous_invFun := I.continuous_invFun.prodMap I'.continuous_invFun }

Product of models with corners

Informal description

Given two models with corners $I$ on $(E, H)$ and $I'$ on $(E', H')$, their product $I \times I'$ is a model with corners on $(E \times E', H \times H')$. The embedding map sends $(x_1, x_2) \in H \times H'$ to $(I(x_1), I'(x_2)) \in E \times E'$, and the inverse map sends $(y_1, y_2) \in E \times E'$ to $(I^{-1}(y_1), I'^{-1}(y_2)) \in H \times H'$. The source of the product model is the set of pairs where each component is in the source of the respective model. This construction preserves the unique differentiability properties and continuity of the original models.

ModelWithCorners.pi definition

 {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι] {E : ι → Type w} [∀ i, NormedAddCommGroup (E i)]
  [∀ i, NormedSpace 𝕜 (E i)] {H : ι → Type u'} [∀ i, TopologicalSpace (H i)] (I : ∀ i, ModelWithCorners 𝕜 (E i) (H i)) :
  ModelWithCorners 𝕜 (∀ i, E i) (ModelPi H)

Full source

/-- Given a finite family of `ModelWithCorners` `I i` on `(E i, H i)`, we define the model with
corners `pi I` on `(Π i, E i, ModelPi H)`. See note [Manifold type tags] for explanation about
`ModelPi H`. -/
def ModelWithCorners.pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι]
    {E : ι → Type w} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] {H : ι → Type u'}
    [∀ i, TopologicalSpace (H i)] (I : ∀ i, ModelWithCorners 𝕜 (E i) (H i)) :
    ModelWithCorners 𝕜 (∀ i, E i) (ModelPi H) where
  toPartialEquiv := PartialEquiv.pi fun i => (I i).toPartialEquiv
  source_eq := by simp only [pi_univ, mfld_simps]
  uniqueDiffOn' := UniqueDiffOn.pi ι E _ _ fun i _ => (I i).uniqueDiffOn'
  target_subset_closure_interior := by
    simp only [PartialEquiv.pi_target, target_eq, finite_univ, interior_pi_set, closure_pi_set]
    exact Set.pi_mono (fun i _ ↦ (I i).range_subset_closure_interior)
  continuous_toFun := continuous_pi fun i => (I i).continuous.comp (continuous_apply i)
  continuous_invFun := continuous_pi fun i => (I i).continuous_symm.comp (continuous_apply i)

Product model with corners

Informal description

Given a finite index set $\iota$ and for each $i \in \iota$, a model with corners $I_i$ embedding a topological space $H_i$ into a normed vector space $E_i$ over a nontrivially normed field $\mathbb{K}$, the product model with corners $\prod_i I_i$ embeds the product space $\prod_i H_i$ into the product normed space $\prod_i E_i$. Specifically: - The embedding is defined componentwise via the partial equivalences $I_i$. - The source of the product embedding is the entire product space $\prod_i H_i$. - The target satisfies $\prod_i \text{range}(I_i) \subseteq \text{closure}(\prod_i \text{interior}(\text{range}(I_i)))$. - The embedding and its inverse are continuous with respect to the product topology.

ModelWithCorners.tangent abbrev

 {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : ModelWithCorners 𝕜 (E × E) (ModelProd H E)

Full source

/-- Special case of product model with corners, which is trivial on the second factor. This shows up
as the model to tangent bundles. -/
abbrev ModelWithCorners.tangent {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) : ModelWithCorners 𝕜 (E × E) (ModelProd H E) :=
  I.prod 𝓘(𝕜, E)

Tangent Model with Corners Construction

Informal description

Given a model with corners $I$ embedding a topological space $H$ into a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, the tangent model with corners $I_{\text{tang}}$ is a model embedding $H \times E$ into $E \times E$. This construction is used to define the tangent bundle of a manifold modeled on $(E, H)$ with respect to $I$.

modelWithCorners_prod_toPartialEquiv theorem

: (I.prod J).toPartialEquiv = I.toPartialEquiv.prod J.toPartialEquiv

Full source

@[simp, mfld_simps]
theorem modelWithCorners_prod_toPartialEquiv :
    (I.prod J).toPartialEquiv = I.toPartialEquiv.prod J.toPartialEquiv :=
  rfl

Product of Models with Corners Preserves Partial Equivalence

Informal description

For any two models with corners $I$ and $J$, the partial equivalence associated to their product $I \times J$ is equal to the product of the partial equivalences associated to $I$ and $J$. In other words, $(I \times J).\text{toPartialEquiv} = I.\text{toPartialEquiv} \times J.\text{toPartialEquiv}$.

modelWithCorners_prod_coe theorem

(I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') : (I.prod I' : _ × _ → _ × _) = Prod.map I I'

Full source

@[simp, mfld_simps]
theorem modelWithCorners_prod_coe (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') :
    (I.prod I' : _ × _ → _ × _) = Prod.map I I' :=
  rfl

Product of Model Embeddings Equals Product Map

Informal description

Let $I$ and $I'$ be models with corners on $(E, H)$ and $(E', H')$ respectively, over a nontrivially normed field $\mathbb{K}$. Then the embedding function of the product model $I \times I'$ is equal to the product map of the embedding functions of $I$ and $I'$, i.e., $(I \times I')(x_1, x_2) = (I(x_1), I'(x_2))$ for all $(x_1, x_2) \in H \times H'$.

modelWithCorners_prod_coe_symm theorem

 (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') :
  ((I.prod I').symm : _ × _ → _ × _) = Prod.map I.symm I'.symm

Full source

@[simp, mfld_simps]
theorem modelWithCorners_prod_coe_symm (I : ModelWithCorners 𝕜 E H)
    (I' : ModelWithCorners 𝕜 E' H') :
    ((I.prod I').symm : _ × _ → _ × _) = Prod.map I.symm I'.symm :=
  rfl

Inverse of Product Model with Corners Equals Product of Inverses

Informal description

Let $I$ and $I'$ be models with corners on $(E, H)$ and $(E', H')$ respectively, where $E$ and $E'$ are normed spaces over a nontrivially normed field $\mathbb{K}$. Then the inverse of the product model $I \times I'$ is equal to the product of the inverses, i.e., $(I \times I')^{-1} = I^{-1} \times I'^{-1}$ as maps from $E \times E'$ to $H \times H'$.

modelWithCornersSelf_prod theorem

: 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)

Full source

/-- This lemma should be erased, or at least burn in hell, as it uses bad defeq: the left model
with corners is for `E times F`, the right one for `ModelProd E F`, and there's a good reason
we are distinguishing them. -/
theorem modelWithCornersSelf_prod : 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F) := by ext1 <;> simp

Trivial Model with Corners on Product Space Equals Product of Trivial Models

Informal description

The trivial model with corners on the product space $E \times F$ is equal to the product of the trivial models with corners on $E$ and $F$, i.e., \[ \mathcal{I}(\mathbb{K}, E \times F) = \mathcal{I}(\mathbb{K}, E) \times \mathcal{I}(\mathbb{K}, F). \]

ModelWithCorners.range_prod theorem

: range (I.prod J) = range I ×ˢ range J

Full source

theorem ModelWithCorners.range_prod : range (I.prod J) = range I ×ˢ range J := by
  simp_rw [← ModelWithCorners.target_eq]; rfl

Range of Product Model Equals Product of Ranges

Informal description

For any two models with corners $I : H \to E$ and $J : H' \to E'$, the range of their product model $I \times J : H \times H' \to E \times E'$ is equal to the Cartesian product of their individual ranges, i.e., \[ \text{range}(I \times J) = \text{range}(I) \times \text{range}(J). \]

ModelWithCorners.Boundaryless structure

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)

Full source

/-- Property ensuring that the model with corners `I` defines manifolds without boundary. This
differs from the more general `BoundarylessManifold`, which requires every point on the manifold
to be an interior point. -/
class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) : Prop where
  range_eq_univ : range I = univ

Boundaryless model with corners

Informal description

A model with corners $ I $ is called *boundaryless* if the embedding $ I : H \to E $ is surjective, meaning that the image of $ H $ under $ I $ is the entire space $ E $. This ensures that the manifold defined using $ I $ has no boundary.

ModelWithCorners.range_eq_univ theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : range I = univ

Full source

theorem ModelWithCorners.range_eq_univ {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] :
    range I = univ := ModelWithCorners.Boundaryless.range_eq_univ

Range of Boundaryless Model with Corners Equals Entire Space

Informal description

For a boundaryless model with corners $I$ embedding a topological space $H$ into a normed vector space $E$ over a nontrivially normed field $\mathbb{K}$, the range of the embedding $I$ is equal to the entire space $E$. In other words, $I$ is surjective.

ModelWithCorners.toHomeomorph definition

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : H ≃ₜ E

Full source

/-- If `I` is a `ModelWithCorners.Boundaryless` model, then it is a homeomorphism. -/
@[simps +simpRhs]
def ModelWithCorners.toHomeomorph {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] : H ≃ₜ E where
  __ := I
  left_inv := I.left_inv
  right_inv _ := I.right_inv <| I.range_eq_univ.symm ▸ mem_univ _

Homeomorphism induced by a boundaryless model with corners

Informal description

Given a boundaryless model with corners $ I : H \to E $ (where $ H $ is a topological space and $ E $ is a normed vector space over a nontrivially normed field $ \mathbb{K} $), the map $ I $ is a homeomorphism between $ H $ and $ E $. This means $ I $ is a continuous bijection with a continuous inverse, preserving the topological structure of $ H $ and $ E $.

modelWithCornersSelf_boundaryless instance

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
  (modelWithCornersSelf 𝕜 E).Boundaryless

Full source

/-- The trivial model with corners has no boundary -/
instance modelWithCornersSelf_boundaryless (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : (modelWithCornersSelf 𝕜 E).Boundaryless :=
  ⟨by simp⟩

Trivial Model with Corners is Boundaryless

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed vector space $E$ over $\mathbb{K}$, the trivial model with corners structure on $E$ (where the embedding is the identity map) is boundaryless. This means that the identity embedding of $E$ into itself is surjective, and thus the manifold modeled on $E$ has no boundary.

ModelWithCorners.range_eq_univ_prod instance

 {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] {E' : Type v'} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') [I'.Boundaryless] :
  (I.prod I').Boundaryless

Full source

/-- If two model with corners are boundaryless, their product also is -/
instance ModelWithCorners.range_eq_univ_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type w} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) [I.Boundaryless] {E' : Type v'} [NormedAddCommGroup E']
    [NormedSpace 𝕜 E'] {H' : Type w'} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
    [I'.Boundaryless] : (I.prod I').Boundaryless := by
  constructor
  dsimp [ModelWithCorners.prod, ModelProd]
  rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]

Product of Boundaryless Models with Corners is Boundaryless

Informal description

For any boundaryless models with corners $I$ on $(E, H)$ and $I'$ on $(E', H')$, their product $I \times I'$ is also boundaryless. This means that the embedding $(x_1, x_2) \mapsto (I(x_1), I'(x_2))$ from $H \times H'$ to $E \times E'$ is surjective.

contDiffPregroupoid definition

: Pregroupoid H

Full source

/-- Given a model with corners `(E, H)`, we define the pregroupoid of `C^n` transformations of `H`
as the maps that are `C^n` when read in `E` through `I`. -/
def contDiffPregroupoid : Pregroupoid H where
  property f s := ContDiffOn 𝕜 n (I ∘ f ∘ I.symm) (I.symm ⁻¹' sI.symm ⁻¹' s ∩ range I)
  comp {f g u v} hf hg _ _ _ := by
    have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
    simp only [this]
    refine hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_
    rintro x ⟨hx1, _⟩
    simp only [mfld_simps] at hx1 ⊢
    exact hx1.2
  id_mem := by
    apply ContDiffOn.congr contDiff_id.contDiffOn
    rintro x ⟨_, hx2⟩
    rcases mem_range.1 hx2 with ⟨y, hy⟩
    rw [← hy]
    simp only [mfld_simps]
  locality {f u} _ H := by
    apply contDiffOn_of_locally_contDiffOn
    rintro y ⟨hy1, hy2⟩
    rcases mem_range.1 hy2 with ⟨x, hx⟩
    rw [← hx] at hy1 ⊢
    simp only [mfld_simps] at hy1 ⊢
    rcases H x hy1 with ⟨v, v_open, xv, hv⟩
    have : I.symm ⁻¹' (u ∩ v)I.symm ⁻¹' (u ∩ v) ∩ range I = I.symm ⁻¹' uI.symm ⁻¹' u ∩ range II.symm ⁻¹' u ∩ range I ∩ I.symm ⁻¹' v := by
      rw [preimage_inter, inter_assoc, inter_assoc]
      congr 1
      rw [inter_comm]
    rw [this] at hv
    exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
  congr {f g u} _ fg hf := by
    apply hf.congr
    rintro y ⟨hy1, hy2⟩
    rcases mem_range.1 hy2 with ⟨x, hx⟩
    rw [← hx] at hy1 ⊢
    simp only [mfld_simps] at hy1 ⊢
    rw [fg _ hy1]

Pregroupoid of $C^n$ transformations with respect to a model with corners

Informal description

The pregroupoid of $C^n$ transformations on a model space $H$ with respect to a model with corners $I : H \to E$ consists of local homeomorphisms $f$ of $H$ such that, when composed with $I$ and its inverse, the resulting map $I \circ f \circ I^{-1}$ is $C^n$ on the intersection of $I^{-1}(\text{domain of } f)$ with the range of $I$. This pregroupoid satisfies the following properties: 1. **Composition**: If $f$ and $g$ are $C^n$ in this sense, then their composition $g \circ f$ is also $C^n$. 2. **Identity**: The identity map on $H$ is $C^n$. 3. **Locality**: A map $f$ is $C^n$ if it is locally $C^n$ around every point in its domain. 4. **Congruence**: If $f$ and $g$ agree on their common domain, and $f$ is $C^n$, then $g$ is also $C^n$.

contDiffGroupoid definition

: StructureGroupoid H

Full source

/-- Given a model with corners `(E, H)`, we define the groupoid of invertible `C^n` transformations
of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/
def contDiffGroupoid : StructureGroupoid H :=
  Pregroupoid.groupoid (contDiffPregroupoid n I)

Groupoid of $C^n$ transformations with respect to a model with corners

Informal description

The groupoid of $C^n$ transformations on a model space $H$ with respect to a model with corners $I : H \to E$ consists of all local homeomorphisms of $H$ that are $C^n$ when composed with $I$ and its inverse. Specifically, a local homeomorphism $f$ of $H$ belongs to this groupoid if the map $I \circ f \circ I^{-1}$ is $C^n$ on the intersection of $I^{-1}(\text{domain of } f)$ with the range of $I$.

contDiffGroupoid_le theorem

(h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I

Full source

/-- Inclusion of the groupoid of `C^n` local diffeos in the groupoid of `C^m` local diffeos when
`m ≤ n` -/
theorem contDiffGroupoid_le (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I := by
  rw [contDiffGroupoid, contDiffGroupoid]
  apply groupoid_of_pregroupoid_le
  intro f s hfs
  exact ContDiffOn.of_le hfs h

Inclusion of $C^n$ Groupoid in $C^m$ Groupoid for $m \leq n$

Informal description

For any extended natural numbers $m$ and $n$ with $m \leq n$, the groupoid of $C^n$ transformations with respect to a model with corners $I$ is contained in the groupoid of $C^m$ transformations with respect to the same model with corners $I$.

contDiffGroupoid_zero_eq theorem

: contDiffGroupoid 0 I = continuousGroupoid H

Full source

/-- The groupoid of `0`-times continuously differentiable maps is just the groupoid of all
partial homeomorphisms -/
theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H := by
  apply le_antisymm le_top
  intro u _
  -- we have to check that every partial homeomorphism belongs to `contDiffGroupoid 0 I`,
  -- by unfolding its definition
  change u ∈ contDiffGroupoid 0 I
  rw [contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid]
  simp only [contDiffOn_zero]
  constructor
  · refine I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)
    exact (mapsTo_preimage _ _).mono_left inter_subset_left
  · refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
    exact (mapsTo_preimage _ _).mono_left inter_subset_left

$C^0$ Groupoid Equals Continuous Groupoid

Informal description

The groupoid of $C^0$ transformations with respect to a model with corners $I$ is equal to the groupoid of all continuous partial homeomorphisms on the model space $H$.

ContDiffGroupoid.mem_of_source_eq_empty theorem

(f : PartialHomeomorph H H) (hf : f.source = ∅) : f ∈ contDiffGroupoid n I

Full source

/-- Any change of coordinates with empty source belongs to `contDiffGroupoid`. -/
lemma ContDiffGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
    (hf : f.source = ∅) : f ∈ contDiffGroupoid n I := by
  constructor
  · intro x ⟨hx, _⟩
    rw [mem_preimage] at hx
    simp_all only [mem_empty_iff_false]
  · intro x ⟨hx, _⟩
    have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
    simp_all [hx]

Empty source implies membership in $C^n$ groupoid

Informal description

For any partial homeomorphism $f$ of the model space $H$ with empty source set (i.e., $f.\text{source} = \emptyset$), $f$ belongs to the $C^n$ groupoid with respect to the model with corners $I$.

ContinuousGroupoid.mem_of_source_eq_empty theorem

(f : PartialHomeomorph H H) (hf : f.source = ∅) : f ∈ continuousGroupoid H

Full source

/-- Any change of coordinates with empty source belongs to `continuousGroupoid`. -/
lemma ContinuousGroupoid.mem_of_source_eq_empty (f : PartialHomeomorph H H)
    (hf : f.source = ∅) : f ∈ continuousGroupoid H := by
  rw [← contDiffGroupoid_zero_eq (I := I)]
  exact ContDiffGroupoid.mem_of_source_eq_empty f hf

Partial homeomorphism with empty source is in the continuous groupoid

Informal description

For any partial homeomorphism $f$ of the model space $H$ with empty source set (i.e., $f.\text{source} = \emptyset$), $f$ belongs to the continuous groupoid of $H$.

ofSet_mem_contDiffGroupoid theorem

{s : Set H} (hs : IsOpen s) : PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I

Full source

/-- An identity partial homeomorphism belongs to the `C^n` groupoid. -/
theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
    PartialHomeomorph.ofSetPartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I := by
  rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
  suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' sI.symm ⁻¹' s ∩ range I) by
    simp [h, contDiffPregroupoid]
  have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn
  exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)

Identity Partial Homeomorphism on Open Set Belongs to $C^n$ Groupoid

Informal description

For any open subset $s$ of the model space $H$, the identity partial homeomorphism on $s$ belongs to the $C^n$ groupoid with respect to the model with corners $I : H \to E$.

symm_trans_mem_contDiffGroupoid theorem

(e : PartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I

Full source

/-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to
the `C^n` groupoid. -/
theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) :
    e.symm.trans e ∈ contDiffGroupoid n I :=
  haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
    PartialHomeomorph.symm_trans_self _
  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid e.open_target) this

Inverse-Transition Map of Partial Homeomorphism is $C^n$-Smooth

Informal description

Let $M$ be a manifold modeled on a space $H$ with respect to a model with corners $I : H \to E$. For any partial homeomorphism $e$ from $M$ to $H$, the composition of its inverse $e^{-1}$ with $e$ belongs to the $C^n$ groupoid associated with $I$. In other words, the transition map $e^{-1} \circ e$ is $C^n$-smooth when composed with the model with corners $I$.

contDiffGroupoid_prod theorem

 {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {e : PartialHomeomorph H H} {e' : PartialHomeomorph H' H'}
  (he : e ∈ contDiffGroupoid n I) (he' : e' ∈ contDiffGroupoid n I') : e.prod e' ∈ contDiffGroupoid n (I.prod I')

Full source

/-- The product of two `C^n` partial homeomorphisms is `C^n`. -/
theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
    {e : PartialHomeomorph H H} {e' : PartialHomeomorph H' H'} (he : e ∈ contDiffGroupoid n I)
    (he' : e' ∈ contDiffGroupoid n I') : e.prod e' ∈ contDiffGroupoid n (I.prod I') := by
  obtain ⟨he, he_symm⟩ := he
  obtain ⟨he', he'_symm⟩ := he'
  constructor <;> simp only [PartialEquiv.prod_source, PartialHomeomorph.prod_toPartialEquiv,
    contDiffPregroupoid]
  · have h3 := ContDiffOn.prodMap he he'
    rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
    rw [← (I.prod I').image_eq]
    exact h3
  · have h3 := ContDiffOn.prodMap he_symm he'_symm
    rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
    rw [← (I.prod I').image_eq]
    exact h3

Product of $C^n$ Partial Homeomorphisms is $C^n$ with Respect to Product Model

Informal description

Let $I : H \to E$ and $I' : H' \to E'$ be models with corners over a nontrivially normed field $\mathbb{K}$. If $e$ is a $C^n$ partial homeomorphism of $H$ with respect to $I$ and $e'$ is a $C^n$ partial homeomorphism of $H'$ with respect to $I'$, then their product $e \times e'$ is a $C^n$ partial homeomorphism of $H \times H'$ with respect to the product model with corners $I \times I'$.

instClosedUnderRestrictionContDiffGroupoid instance

: ClosedUnderRestriction (contDiffGroupoid n I)

Full source

/-- The `C^n` groupoid is closed under restriction. -/
instance : ClosedUnderRestriction (contDiffGroupoid n I) :=
  (closedUnderRestriction_iff_id_le _).mpr
    (by
      rw [StructureGroupoid.le_iff]
      rintro e ⟨s, hs, hes⟩
      apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes
      exact ofSet_mem_contDiffGroupoid hs)

Closure Under Restriction for $C^n$ Groupoid

Informal description

The groupoid of $C^n$ transformations with respect to a model with corners $I : H \to E$ is closed under restriction to open subsets. That is, for any partial homeomorphism $e$ in the groupoid and any open subset $s$ of the source of $e$, the restriction of $e$ to $s$ is also in the groupoid.

IsManifold structure

{𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*)
    [TopologicalSpace M] [ChartedSpace H M] : Prop
    extends HasGroupoid M (contDiffGroupoid n I)

Full source

/-- Typeclass defining manifolds with respect to a model with corners, over a
field `𝕜`. This definition includes the model with corners `I` (which might allow boundary, corners,
or not, so this class covers both manifolds with boundary and manifolds without boundary), and
a smoothness parameter `n : WithTop ℕ∞` (where `n = 0` means topological manifold, `n = ∞` means
smooth manifold and `n = ω` means analytic manifold). -/
class IsManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*)
    [TopologicalSpace M] [ChartedSpace H M] : Prop
    extends HasGroupoid M (contDiffGroupoid n I)

$C^n$ manifold with model with corners $I$

Informal description

A topological space $M$ is called a $C^n$ manifold with respect to a model with corners $I : H \to E$ if it is equipped with an atlas of charts mapping open subsets of $M$ to open subsets of $H$, and the transition maps between charts are $C^n$-smooth when viewed through the embedding $I$. Here, $\mathbb{K}$ is a nontrivially normed field, $E$ is a normed vector space over $\mathbb{K}$, and $H$ is a topological space embedded in $E$ via $I$. The regularity parameter $n$ can be: - $0$ for topological manifolds, - $\infty$ for smooth manifolds, - $\omega$ for analytic manifolds.

IsManifold.mk' theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
  [gr : HasGroupoid M (contDiffGroupoid n I)] : IsManifold I n M

Full source

/-- Building a `C^n` manifold from a `HasGroupoid` assumption. -/
theorem IsManifold.mk' {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
    (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
    [gr : HasGroupoid M (contDiffGroupoid n I)] : IsManifold I n M :=
  { gr with }

Construction of $C^n$ manifold from groupoid condition

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed vector space over $\mathbb{K}$, and $H$ a topological space equipped with a model with corners $I : H \to E$. Given a topological space $M$ with a charted space structure over $H$ and a regularity parameter $n \in \mathbb{N}_\infty$, if $M$ has the groupoid of $C^n$ transformations with respect to $I$, then $M$ is a $C^n$ manifold with model with corners $I$.

isManifold_of_contDiffOn theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
  (h :
    ∀ e e' : PartialHomeomorph M H,
      e ∈ atlas H M →
        e' ∈ atlas H M → ContDiffOn 𝕜 n (I ∘ e.symm ≫ₕ e' ∘ I.symm) (I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I)) :
  IsManifold I n M

Full source

theorem isManifold_of_contDiffOn {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*)
    [TopologicalSpace M] [ChartedSpace H M]
    (h : ∀ e e' : PartialHomeomorph M H, e ∈ atlas H M → e' ∈ atlas H M →
      ContDiffOn 𝕜 n (I ∘ e.symm ≫ₕ e' ∘ I.symm) (I.symm ⁻¹' (e.symm ≫ₕ e').sourceI.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I)) :
    IsManifold I n M where
  compatible := by
    haveI : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (h _ _)
    apply StructureGroupoid.compatible

$C^n$-manifold criterion via smoothness of transition maps

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed vector space over $\mathbb{K}$, and $H$ a topological space equipped with a model with corners $I : H \to E$. Given a topological space $M$ with a charted space structure over $H$ and a regularity parameter $n \in \mathbb{N}_\infty$, if for every pair of charts $e, e'$ in the atlas of $M$, the composition $I \circ e^{-1} \circ e' \circ I^{-1}$ is $C^n$-smooth on the intersection of $I^{-1}((e^{-1} \circ e').\text{source})$ with the range of $I$, then $M$ is a $C^n$ manifold with respect to the model with corners $I$.

instIsManifoldModelSpace instance

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} : IsManifold I n H

Full source

/-- For any model with corners, the model space is a `C^n` manifold -/
instance instIsManifoldModelSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
    {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} : IsManifold I n H :=
  { hasGroupoid_model_space _ _ with }

Model Spaces as $C^n$ Manifolds

Informal description

For any model with corners $I : H \to E$ over a nontrivially normed field $\mathbb{K}$ and any regularity $n \in \mathbb{N}_\infty$, the model space $H$ is a $C^n$ manifold with respect to $I$.

IsManifold.of_le theorem

{m n : WithTop ℕ∞} (hmn : m ≤ n) [IsManifold I n M] : IsManifold I m M

Full source

protected theorem of_le {m n : WithTop ℕ∞} (hmn : m ≤ n)
    [IsManifold I n M] : IsManifold I m M := by
  have : HasGroupoid M (contDiffGroupoid m I) :=
    hasGroupoid_of_le (G₁ := contDiffGroupoid n I) (by infer_instance)
      (contDiffGroupoid_le hmn)
  exact mk' I m M

$C^n$ manifolds are $C^m$ manifolds for $m \leq n$

Informal description

Let $M$ be a $C^n$ manifold with respect to a model with corners $I : H \to E$, where $n \in \mathbb{N}_\infty$. For any $m \in \mathbb{N}_\infty$ such that $m \leq n$, the manifold $M$ is also a $C^m$ manifold with respect to $I$.

ENat.LEInfty structure

(m : WithTop ℕ∞)

Full source

/-- A typeclass registering that a smoothness exponent is smaller than `∞`. Used to deduce that
some manifolds are `C^n` when they are `C^∞`. -/
class _root_.ENat.LEInfty (m : WithTop ℕ∞) where
  out : m ≤ ∞

Extended natural number less than or equal to infinity

Informal description

The typeclass `ENat.LEInfty` asserts that a given extended natural number `m : ℕ∞` is less than or equal to infinity. This is used to deduce that certain manifolds are `C^n` when they are known to be `C^∞`, by leveraging the fact that any finite smoothness exponent is automatically less than or equal to infinity.

IsManifold.instLEInftyCastWithTopENat instance

(n : ℕ) : LEInfty (n : WithTop ℕ∞)

Full source

instance (n : ℕ) : LEInfty (n : WithTop ℕ∞) := ⟨mod_cast le_top⟩

Finite Extended Natural Numbers are Bounded by Infinity

Informal description

For any natural number $n$, the extended natural number $n$ (viewed as an element of $\mathbb{N}_\infty$) is less than or equal to infinity.

IsManifold.instLEInftyOfNatWithTopENat instance

(n : ℕ) [n.AtLeastTwo] : LEInfty (no_index (OfNat.ofNat n) : WithTop ℕ∞)

Full source

instance (n : ℕ) [n.AtLeastTwo] : LEInfty (no_index (OfNat.ofNat n) : WithTop ℕ∞) :=
  inferInstanceAs (LEInfty (n : WithTop ℕ∞))

Finite Extended Natural Numbers ≥ 2 are Bounded by Infinity

Informal description

For any natural number $n \geq 2$, the extended natural number $n$ (viewed as an element of $\mathbb{N}_\infty$) is less than or equal to infinity.

IsManifold.instLEInftyOfNatWithTopENat_1 instance

: LEInfty (1 : WithTop ℕ∞)

Full source

instance : LEInfty (1 : WithTop ℕ∞) := inferInstanceAs (LEInfty ((1 : ℕ) : WithTop ℕ∞))

The Extended Natural Number 1 is Bounded by Infinity

Informal description

The extended natural number $1$ (viewed as an element of $\mathbb{N}_\infty$) is less than or equal to infinity.

IsManifold.instLEInftyOfNatWithTopENat_2 instance

: LEInfty (0 : WithTop ℕ∞)

Full source

instance : LEInfty (0 : WithTop ℕ∞) := inferInstanceAs (LEInfty ((0 : ℕ) : WithTop ℕ∞))

Zero is Bounded by Infinity in Extended Naturals

Informal description

The extended natural number $0$ is less than or equal to infinity in the type $\mathbb{N}_\infty$.

IsManifold.instOfSomeENatTopOfLEInfty instance

{a : WithTop ℕ∞} [IsManifold I ∞ M] [h : LEInfty a] : IsManifold I a M

Full source

instance {a : WithTop ℕ∞} [IsManifold I ∞ M] [h : LEInfty a] :
    IsManifold I a M :=
  IsManifold.of_le h.out

$C^\infty$ Manifolds are $C^a$ Manifolds for $a \leq \infty$

Informal description

For any extended natural number $a \in \mathbb{N}_\infty$ that is less than or equal to infinity, if a manifold $M$ is $C^\infty$-smooth with respect to a model with corners $I$, then $M$ is also $C^a$-smooth with respect to $I$.

IsManifold.instOfTopWithTopENat instance

{a : WithTop ℕ∞} [IsManifold I ω M] : IsManifold I a M

Full source

instance {a : WithTop ℕ∞} [IsManifold I ω M] :
    IsManifold I a M :=
  IsManifold.of_le le_top

Analytic Manifolds are $C^a$ Manifolds for All $a$

Informal description

For any extended natural number $a \in \mathbb{N}_\infty$, if a topological space $M$ is an analytic manifold (i.e., a $C^\omega$ manifold) with respect to a model with corners $I$, then $M$ is also a $C^a$ manifold with respect to $I$.

IsManifold.instOfNatWithTopENat instance

: IsManifold I 0 M

Full source

instance : IsManifold I 0 M := by
  suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M
  constructor
  intro e e' he he'
  rw [contDiffGroupoid_zero_eq]
  trivial

$C^n$ Manifolds are Topological Manifolds

Informal description

Every topological space $M$ that is a $C^n$ manifold with respect to a model with corners $I$ is also a $C^0$ manifold (i.e., a topological manifold) with respect to $I$.

IsManifold.instOfNatWithTopENat_1 instance

[IsManifold I 2 M] : IsManifold I 1 M

Full source

instance [IsManifold I 2 M] :
    IsManifold I 1 M :=
  IsManifold.of_le one_le_two

$C^2$ Manifolds are $C^1$ Manifolds

Informal description

For any $C^2$ manifold $M$ with respect to a model with corners $I$, $M$ is also a $C^1$ manifold with respect to $I$.

IsManifold.instOfNatWithTopENat_2 instance

[IsManifold I 3 M] : IsManifold I 2 M

Full source

instance [IsManifold I 3 M] : IsManifold I 2 M := IsManifold.of_le (n := 3) (by norm_cast)

$C^3$ manifolds are $C^2$ manifolds

Informal description

If $M$ is a $C^3$ manifold with respect to a model with corners $I$, then $M$ is also a $C^2$ manifold with respect to $I$.

IsManifold.maximalAtlas definition

Full source

/-- The maximal atlas of `M` for the `C^n` manifold with corners structure corresponding to the
model with corners `I`. -/
def maximalAtlas :=
  (contDiffGroupoid n I).maximalAtlas M

Maximal atlas for a $C^n$ manifold with corners

Informal description

The maximal atlas of a manifold $M$ with respect to a model with corners $I$ and regularity $n$ is the collection of all local homeomorphisms (charts) from open subsets of $M$ to the model space $H$ that are compatible with the $C^n$ structure defined by $I$. Specifically, it consists of all charts such that the transition maps between any two charts in the atlas are $C^n$ diffeomorphisms when composed with the embedding $I : H \to E$.

IsManifold.subset_maximalAtlas theorem

[IsManifold I n M] : atlas H M ⊆ maximalAtlas I n M

Full source

theorem subset_maximalAtlas [IsManifold I n M] : atlasatlas H M ⊆ maximalAtlas I n M :=
  StructureGroupoid.subset_maximalAtlas _

Atlas is Subset of Maximal Atlas for $C^n$ Manifold

Informal description

For any $C^n$ manifold $M$ with model with corners $I : H \to E$, the atlas of $M$ is contained in the maximal atlas associated with $I$ and regularity $n$. In other words, every chart in the given atlas of $M$ is also a member of the maximal atlas that defines the $C^n$ structure on $M$.

IsManifold.chart_mem_maximalAtlas theorem

[IsManifold I n M] (x : M) : chartAt H x ∈ maximalAtlas I n M

Full source

theorem chart_mem_maximalAtlas [IsManifold I n M] (x : M) :
    chartAtchartAt H x ∈ maximalAtlas I n M :=
  StructureGroupoid.chart_mem_maximalAtlas _ x

Charts Belong to the Maximal Atlas of a $C^n$ Manifold

Informal description

For any point $x$ in a $C^n$ manifold $M$ with model with corners $I : H \to E$, the chart at $x$ belongs to the maximal atlas of $M$ with respect to $I$ and regularity $n$.

IsManifold.compatible_of_mem_maximalAtlas theorem

 {e e' : PartialHomeomorph M H} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I n M) :
  e.symm.trans e' ∈ contDiffGroupoid n I

Full source

theorem compatible_of_mem_maximalAtlas {e e' : PartialHomeomorph M H} (he : e ∈ maximalAtlas I n M)
    (he' : e' ∈ maximalAtlas I n M) : e.symm.trans e' ∈ contDiffGroupoid n I :=
  StructureGroupoid.compatible_of_mem_maximalAtlas he he'

Transition maps between charts in a $C^n$ manifold are $C^n$ diffeomorphisms

Informal description

Let $M$ be a $C^n$ manifold with model with corners $I : H \to E$, and let $e, e'$ be two charts in the maximal atlas of $M$ with respect to $I$ and regularity $n$. Then the transition map $e^{-1} \circ e'$ belongs to the groupoid of $C^n$ transformations with respect to $I$.

IsManifold.maximalAtlas_subset_of_le theorem

{m n : WithTop ℕ∞} (h : m ≤ n) : maximalAtlas I n M ⊆ maximalAtlas I m M

Full source

lemma maximalAtlas_subset_of_le {m n : WithTop ℕ∞} (h : m ≤ n) :
    maximalAtlasmaximalAtlas I n M ⊆ maximalAtlas I m M :=
  StructureGroupoid.maximalAtlas_mono (contDiffGroupoid_le h)

Inclusion of Maximal Atlases for Decreasing Regularity: $\mathcal{A}_n \subseteq \mathcal{A}_m$ when $m \leq n$

Informal description

For any extended natural numbers $m$ and $n$ with $m \leq n$, the maximal atlas of $C^n$-compatible charts on a manifold $M$ with respect to a model with corners $I$ is contained in the maximal atlas of $C^m$-compatible charts.

IsManifold.empty instance

[IsEmpty M] : IsManifold I n M

Full source

/-- The empty set is a `C^n` manifold w.r.t. any charted space and model. -/
instance empty [IsEmpty M] : IsManifold I n M := by
  apply isManifold_of_contDiffOn
  intro e e' _ _ x hx
  set t := I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I
  -- Since `M` is empty, the condition about compatibility of transition maps is vacuous.
  have : (e.symm ≫ₕ e').source = ∅ := calc (e.symm ≫ₕ e').source
    _ = (e.symm.source) ∩ e.symm ⁻¹' e'.source := by rw [← PartialHomeomorph.trans_source]
    _ = (e.symm.source) ∩ e.symm ⁻¹' ∅ := by rw [eq_empty_of_isEmpty (e'.source)]
    _ = (e.symm.source) ∩ ∅ := by rw [preimage_empty]
    _ = ∅ := inter_empty e.symm.source
  have : t = ∅ := calc t
    _ = I.symm ⁻¹' (e.symm ≫ₕ e').sourceI.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I := by
      rw [← Subtype.preimage_val_eq_preimage_val_iff]
    _ = ∅∅ ∩ range I := by rw [this, preimage_empty]
    _ = ∅ := empty_inter (range I)
  apply (this ▸ hx).elim

Empty Types as $C^n$ Manifolds

Informal description

Every empty type is a $C^n$ manifold with respect to any model with corners $I$ and any regularity $n$.

IsManifold.of_discreteTopology theorem

[DiscreteTopology M] [Unique E] : IsManifold (modelWithCornersSelf 𝕜 E) n M

Full source

/-- A discrete space `M` is a smooth manifold over the trivial model on a trivial normed space. -/
theorem of_discreteTopology [DiscreteTopology M] [Unique E] :
    IsManifold (modelWithCornersSelf 𝕜 E) n M := by
  apply isManifold_of_contDiffOn _ _ _ (fun _ _ _ _ ↦ contDiff_of_subsingleton.contDiffOn)

Discrete spaces as smooth manifolds over trivial normed spaces

Informal description

Let $M$ be a topological space with the discrete topology and $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$ with a unique element. Then $M$ is a $C^n$ manifold with respect to the trivial model with corners on $E$.

IsManifold.prod instance

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type*}
  [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I n M] (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' n M'] :
  IsManifold (I.prod I') n (M × M')

Full source

/-- The product of two `C^n` manifolds is naturally a `C^n` manifold. -/
instance prod {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type*}
    [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type*} [TopologicalSpace H']
    {I' : ModelWithCorners 𝕜 E' H'} (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
    [IsManifold I n M] (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M']
    [IsManifold I' n M'] :
    IsManifold (I.prod I') n (M × M') where
  compatible := by
    rintro f g ⟨f1, hf1, f2, hf2, rfl⟩ ⟨g1, hg1, g2, hg2, rfl⟩
    rw [PartialHomeomorph.prod_symm, PartialHomeomorph.prod_trans]
    have h1 := (contDiffGroupoid n I).compatible hf1 hg1
    have h2 := (contDiffGroupoid n I').compatible hf2 hg2
    exact contDiffGroupoid_prod h1 h2

Product of $C^n$ Manifolds is a $C^n$ Manifold

Informal description

For any two $C^n$ manifolds $M$ and $M'$ modeled on spaces $H$ and $H'$ with respect to models with corners $I$ and $I'$ respectively, their product $M \times M'$ is naturally a $C^n$ manifold modeled on $H \times H'$ with respect to the product model with corners $I \times I'$.

IsManifold.disjointUnion instance

: IsManifold I n (M ⊕ M')

Full source

/-- The disjoint union of two `C^n` manifolds modelled on `(E, H)`
is a `C^n` manifold modeled on `(E, H)`. -/
instance disjointUnion : IsManifold I n (M ⊕ M') where
  compatible {e} e' he he' := by
    obtain (h | h) := isEmpty_or_nonempty H
    · exact ContDiffGroupoid.mem_of_source_eq_empty _ (eq_empty_of_isEmpty _)
    obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := ChartedSpace.mem_atlas_sum he
    · obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
      · rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]
        exact hM.compatible hf hf'
      · rw [hef, he'f']
        apply ContDiffGroupoid.mem_of_source_eq_empty
        ext x
        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all [hx₂], fun hx ↦ hx.elim⟩
    · -- Analogous argument to the first case: is there a way to deduplicate?
      obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
      · rw [hef, he'f']
        apply ContDiffGroupoid.mem_of_source_eq_empty
        ext x
        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all [hx₂], fun hx ↦ hx.elim⟩
      · rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inr]
        exact hM'.compatible hf hf'

Disjoint Union of $C^n$ Manifolds is a $C^n$ Manifold

Informal description

The disjoint union $M \sqcup M'$ of two $C^n$ manifolds modeled on the same space $H$ with respect to a model with corners $I : H \to E$ is again a $C^n$ manifold modeled on $H$ with respect to $I$.

PartialHomeomorph.isManifold_singleton theorem

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type*} [TopologicalSpace M]
  (e : PartialHomeomorph M H) (h : e.source = Set.univ) : @IsManifold 𝕜 _ E _ _ H _ I n M _ (e.singletonChartedSpace h)

Full source

theorem PartialHomeomorph.isManifold_singleton
    {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
    {M : Type*} [TopologicalSpace M] (e : PartialHomeomorph M H) (h : e.source = Set.univ) :
    @IsManifold 𝕜 _ E _ _ H _ I n M _ (e.singletonChartedSpace h) :=
  @IsManifold.mk' _ _ _ _ _ _ _ _ _ _ _ (id _) <|
    e.singleton_hasGroupoid h (contDiffGroupoid n I)

Singleton Partial Homeomorphism Induces $C^n$ Manifold Structure

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed vector space over $\mathbb{K}$, and $H$ a topological space equipped with a model with corners $I : H \to E$. Given a topological space $M$, a partial homeomorphism $e : M \to H$ with source equal to the entire space $M$ (i.e., $e.\text{source} = \text{univ}$), and a regularity parameter $n \in \mathbb{N}_\infty$, then $M$ equipped with the singleton charted space structure induced by $e$ is a $C^n$ manifold with model with corners $I$.

Topology.IsOpenEmbedding.isManifold_singleton theorem

 {𝕜 E H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type*} [TopologicalSpace M] [Nonempty M] {f : M → H}
  (h : IsOpenEmbedding f) : @IsManifold 𝕜 _ E _ _ H _ I n M _ h.singletonChartedSpace

Full source

theorem Topology.IsOpenEmbedding.isManifold_singleton {𝕜 E H : Type*}
    [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
    {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
    {M : Type*} [TopologicalSpace M] [Nonempty M] {f : M → H} (h : IsOpenEmbedding f) :
    @IsManifold 𝕜 _ E _ _ H _ I n M _ h.singletonChartedSpace :=
  (h.toPartialHomeomorph f).isManifold_singleton (by simp)

Open Embedding Induces $C^n$ Manifold Structure via Singleton Chart

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a normed vector space over $\mathbb{K}$, and $H$ a topological space equipped with a model with corners $I : H \to E$. Given a nonempty topological space $M$ and an open embedding $f : M \to H$, then $M$ equipped with the singleton charted space structure induced by $f$ is a $C^n$ manifold with respect to the model with corners $I$ for any regularity parameter $n \in \mathbb{N}_\infty$.

TopologicalSpace.Opens.instIsManifoldSubtypeMem instance

: IsManifold I n s

Full source

instance : IsManifold I n s :=
  { s.instHasGroupoid (contDiffGroupoid n I) with }

Open Subsets of $C^n$ Manifolds are $C^n$ Manifolds

Informal description

For any model with corners $I : H \to E$ and regularity $n$, an open subset $s$ of a $C^n$ manifold $M$ (with respect to $I$) is itself a $C^n$ manifold when equipped with the subspace topology and the restricted charts.

TangentSpace definition

 {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] (_x : M) :
  Type u

Full source

/-- The tangent space at a point of the manifold `M`. It is just `E`. We could use instead
`(tangentBundleCore I M).to_topological_vector_bundle_core.fiber x`, but we use `E` to help the
kernel.
-/
@[nolint unusedArguments]
def TangentSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] (_x : M) : Type u := E

Tangent space of a manifold at a point

Informal description

The tangent space at a point $x$ of a manifold $M$ modeled on a space $H$ with corners (via the model with corners $I : H \to E$) is defined to be the normed vector space $E$ itself. Here, $E$ is a normed space over a nontrivially normed field $\mathbb{K}$, and $H$ is a topological space embedded into $E$ via $I$.

instTopologicalSpaceTangentSpace instance

: TopologicalSpace (TangentSpace I x)

Full source

instance : TopologicalSpace (TangentSpace I x) := inferInstanceAs (TopologicalSpace E)

Topology on the Tangent Space of a Manifold

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$, the tangent space $\text{TangentSpace}\, I\, x$ at any point $x \in M$ is equipped with the topology induced from the normed vector space $E$.

instAddCommGroupTangentSpace instance

: AddCommGroup (TangentSpace I x)

Full source

instance : AddCommGroup (TangentSpace I x) := inferInstanceAs (AddCommGroup E)

Additive Commutative Group Structure on Tangent Spaces

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$, the tangent space at any point $x \in M$ is an additive commutative group. Here, $E$ is a normed vector space over a nontrivially normed field $\mathbb{K}$, and the tangent space $\text{TangentSpace}\, I\, x$ inherits its additive commutative group structure from $E$.

instIsTopologicalAddGroupTangentSpace instance

: IsTopologicalAddGroup (TangentSpace I x)

Full source

instance : IsTopologicalAddGroup (TangentSpace I x) := inferInstanceAs (IsTopologicalAddGroup E)

Tangent Spaces as Topological Additive Groups

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$, the tangent space $\text{TangentSpace}\, I\, x$ at any point $x \in M$ is a topological additive group. Here, $E$ is a normed vector space over a nontrivially normed field $\mathbb{K}$, and the tangent space inherits both its additive group structure and topology from $E$, with the addition operation being continuous with respect to this topology.

instModuleTangentSpace instance

: Module 𝕜 (TangentSpace I x)

Full source

instance : Module 𝕜 (TangentSpace I x) := inferInstanceAs (Module 𝕜 E)

Module Structure on Tangent Spaces of Manifolds

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$, the tangent space $\text{TangentSpace}\, I\, x$ at any point $x \in M$ is a module over the nontrivially normed field $\mathbb{K}$. Here, $E$ is a normed vector space over $\mathbb{K}$, and the module structure on the tangent space is inherited from $E$.

instInhabitedTangentSpace instance

: Inhabited (TangentSpace I x)

Full source

instance : Inhabited (TangentSpace I x) := ⟨0⟩

Tangent Spaces are Inhabited

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$, the tangent space at any point $x \in M$ is an inhabited type. Here, $E$ is a normed vector space over a nontrivially normed field $\mathbb{K}$, and the tangent space $\text{TangentSpace}\, I\, x$ is nonempty, inheriting its inhabitedness from $E$.

TangentBundle abbrev

Full source

/-- The tangent bundle to a manifold, as a Sigma type. Defined in terms of
`Bundle.TotalSpace` to be able to put a suitable topology on it. -/
abbrev TangentBundle := Bundle.TotalSpace E (TangentSpace I : M → Type _)

Tangent Bundle of a Manifold with Corners

Informal description

The tangent bundle of a manifold $M$ modeled on a space $H$ with corners (via the model with corners $I : H \to E$) is the total space of the bundle where the fiber over each point $x \in M$ is the tangent space $T_x M$, which is identified with the normed vector space $E$. More formally, the tangent bundle $T M$ is defined as the collection of all pairs $(x, v)$ where $x \in M$ and $v \in T_x M \cong E$.

instPathConnectedSpaceTangentSpaceReal instance

: PathConnectedSpace (TangentSpace I x)

Full source

instance : PathConnectedSpace (TangentSpace I x) := inferInstanceAs (PathConnectedSpace E)

Path-Connectedness of Tangent Spaces over Real Numbers

Informal description

For any manifold $M$ modeled on a space $H$ with corners via the model with corners $I : H \to E$ over the real numbers $\mathbb{R}$, the tangent space $\text{TangentSpace}\, I\, x$ at any point $x \in M$ is path-connected.