Documentation

TauCeti.Geometry.Manifold.LocalDiffeomorph.OpenSubset

Partial diffeomorphisms and open subsets #

Mathlib's OpenPartialHomeomorph.restrOpen shrinks the source of an open partial homeomorphism to its intersection with an open set. This file provides the same operation for Mathlib's PartialDiffeomorph: the restriction is still C^n in both directions, because both of its domains are subsets of the original ones. It is used to make charts small, for example to make finitely many charts centred at distinct points pairwise disjoint.

A partial diffeomorphism is also a diffeomorphism between its source and its target, each an open subset carrying the charts Mathlib restricts to it. This is the analogue for partial diffeomorphisms of Mathlib's OpenPartialHomeomorph.toHomeomorphSourceTarget, and lets results about diffeomorphisms be applied to a partial diffeomorphism on its domain.

The file also records that the inclusion of an open subset, with the charts Mathlib restricts to it, is a local diffeomorphism. Structures defined through charts, such as orientations, can then be compared on an open subset and on the ambient manifold. An open subset equal to the whole manifold is diffeomorphic to it through its inclusion. A partial diffeomorphism out of an open subset can be carried, near any point of its source, to the ambient manifold.

Main declarations #

PartialDiffeomorph.restrOpen: the restriction of a partial diffeomorphism to an open set.
PartialDiffeomorph.contMDiffOn_toOpenPartialHomeomorph_restrOpen and its symm version: the restrictions of the underlying open partial homeomorphism to an open set are smooth.
PartialDiffeomorph.toDiffeomorphSourceTarget: a partial diffeomorphism as a diffeomorphism between its open source and its open target.
Diffeomorph.ofTop: an open subset equal to ⊤ is diffeomorphic to the ambient manifold.
TauCeti.isLocalDiffeomorph_subtype_val: the inclusion of an open subset is a C^n local diffeomorphism.
PartialDiffeomorph.exists_ambient_of_opens: a partial diffeomorphism out of an open subset agrees near a point of its source with a partial diffeomorphism out of the ambient manifold.

def PartialDiffeomorph.restrOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) (s : Set M) (hs : IsOpen s) :

PartialDiffeomorph I J M N n

The restriction of a partial diffeomorphism to an open set s: its source is Φ.source ∩ s, and its target is the image of that set.

Instances For

theorem PartialDiffeomorph.restrOpen_toPartialEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {s : Set M} (hs : IsOpen s) :

(Φ.restrOpen s hs).toPartialEquiv = Φ.restr s

The underlying partial equivalence of the restriction is the restriction of the underlying partial equivalence.

@[simp]

theorem PartialDiffeomorph.restrOpen_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {s : Set M} (hs : IsOpen s) :

(Φ.restrOpen s hs).source = Φ.source ∩ s

The source of the restriction to s is Φ.source ∩ s.

@[simp]

theorem PartialDiffeomorph.restrOpen_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {s : Set M} (hs : IsOpen s) :

(Φ.restrOpen s hs).target = Φ.target ∩ ↑Φ.symm ⁻¹' s

The target of the restriction to s consists of the points of Φ.target whose preimage lies in s.

@[simp]

theorem PartialDiffeomorph.coe_restrOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {s : Set M} (hs : IsOpen s) :

↑(Φ.restrOpen s hs).toPartialEquiv = ↑Φ.toPartialEquiv

The restriction has the same forward map.

@[simp]

theorem PartialDiffeomorph.coe_restrOpen_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {s : Set M} (hs : IsOpen s) :

↑(Φ.restrOpen s hs).symm = ↑Φ.symm

The restriction has the same inverse map.

theorem PartialDiffeomorph.toOpenPartialHomeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) :

Φ.toOpenPartialHomeomorph.source = Φ.source

The open partial homeomorphism of a partial diffeomorphism has its source.

theorem PartialDiffeomorph.toOpenPartialHomeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) :

Φ.toOpenPartialHomeomorph.target = Φ.target

The open partial homeomorphism of a partial diffeomorphism has its target.

@[simp]

theorem PartialDiffeomorph.coe_toOpenPartialHomeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) :

↑Φ.toOpenPartialHomeomorph.symm = ↑Φ.symm.toPartialEquiv

The inverse of the open partial homeomorphism of a partial diffeomorphism is the inverse function of the partial diffeomorphism.

theorem PartialDiffeomorph.contMDiffOn_toOpenPartialHomeomorph_restrOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {V : Set M} (hV : IsOpen V) :

ContMDiffOn I J n (↑(Φ.toOpenPartialHomeomorph.restrOpen V hV)) (Φ.toOpenPartialHomeomorph.restrOpen V hV).source

Restricting the open partial homeomorphism of a partial diffeomorphism to an open set keeps it smooth on its source.

theorem PartialDiffeomorph.contMDiffOn_toOpenPartialHomeomorph_restrOpen_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) {V : Set M} (hV : IsOpen V) :

ContMDiffOn J I n (↑(Φ.toOpenPartialHomeomorph.restrOpen V hV).symm) (Φ.toOpenPartialHomeomorph.restrOpen V hV).target

The inverse of the restriction of the open partial homeomorphism of a partial diffeomorphism to an open set is smooth on the target of the restriction.

def PartialDiffeomorph.toDiffeomorphSourceTarget {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) :

Diffeomorph I J (↥{ carrier := Φ.source, is_open' := ⋯ }) (↥{ carrier := Φ.target, is_open' := ⋯ }) n

A partial diffeomorphism is a diffeomorphism between its source and its target, as open subsets of M and N.

Instances For

@[simp]

theorem PartialDiffeomorph.toDiffeomorphSourceTarget_apply_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) (x : ↥{ carrier := Φ.source, is_open' := ⋯ }) :

↑(Φ.toDiffeomorphSourceTarget x) = ↑Φ.toPartialEquiv ↑x

The diffeomorphism PartialDiffeomorph.toDiffeomorphSourceTarget evaluates as the partial diffeomorphism.

@[simp]

theorem PartialDiffeomorph.toDiffeomorphSourceTarget_symm_apply_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] (Φ : PartialDiffeomorph I J M N n) (x : ↥{ carrier := Φ.target, is_open' := ⋯ }) :

↑(Φ.toDiffeomorphSourceTarget.symm x) = ↑Φ.symm.toPartialEquiv ↑x

The inverse of PartialDiffeomorph.toDiffeomorphSourceTarget evaluates as the inverse of the partial diffeomorphism.

def Diffeomorph.ofTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (U : TopologicalSpace.Opens M) (hU : U = ⊤) :

Diffeomorph I I (↥U) M n

An open subset U of M equal to ⊤ is C^n diffeomorphic to M through its inclusion.

Instances For

@[simp]

theorem Diffeomorph.ofTop_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} {hU : U = ⊤} (x : ↥U) :

(ofTop U hU) x = ↑x

The diffeomorphism Diffeomorph.ofTop is the inclusion.

theorem Diffeomorph.coe_ofTop {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} {hU : U = ⊤} :

⇑(ofTop U hU) = Subtype.val

The diffeomorphism Diffeomorph.ofTop is the inclusion, as a function.

@[simp]

theorem Diffeomorph.coe_ofTop_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} {hU : U = ⊤} (x : M) :

↑((ofTop U hU).symm x) = x

The inverse of Diffeomorph.ofTop sends a point to itself, viewed in U.

theorem TauCeti.isLocalDiffeomorph_subtype_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} :

IsLocalDiffeomorph I I n Subtype.val

The inclusion of an open subset U of M, charted by the restrictions of the charts of M, is a C^n local diffeomorphism.

theorem PartialDiffeomorph.exists_ambient_of_opens {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {n : WithTop ℕ∞} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {U : TopologicalSpace.Opens M} (Φ : PartialDiffeomorph I J (↥U) N n) {x : ↥U} (hx : x ∈ Φ.source) :

∃ (e : PartialDiffeomorph I J M N n), ↑x ∈ e.source ∧ e.source ⊆ ↑U ∧ ↑e.toPartialEquiv ↑x = ↑Φ.toPartialEquiv x ∧ e.target ⊆ Φ.target ∧ ∀ z ∈ e.target, ↑e.symm.toPartialEquiv z = ↑(↑Φ.symm.toPartialEquiv z)

Carrying a partial diffeomorphism out of an open subset to the ambient manifold. If Φ is a C^n partial diffeomorphism out of an open subset U of M and x ∈ Φ.source, then there is a C^n partial diffeomorphism e out of M whose source contains x and lies in U, which agrees with Φ at x, whose target lies in that of Φ, and whose inverse is the inverse of Φ followed by the inclusion of U.