The local cover X' = ∐ Uᵢ → X of a triple

For any X, choose an open affine cover X = ⋃ Uᵢ and let X' := ∐ Uᵢ; then X' is affine and there is a smooth surjection g : X' → X (the proof of [Kol07, Proposition 37]). On manifolds: a countable cover by chart domains (second countability), X' their disjoint union (sigmaManifold), g the coproduct of the inclusions, a surjective coproduct of analytic open embeddings, and the triple on X' the pullback data of T along g, a local triple (each chart domain is a chart union with one piece, its own chart restricted; the disjoint union of chart unions is one). The inclusion of an open subset is an analytic open embedding (its local inverse the codomain restriction of the identity, analytic by Mathlib's ContMDiffAt.subtypeVal_comp_iff). The file also records that a closed submanifold of an open subset U, read in the bundled U, is a closed submanifold of the manifold U (IsClosedSubmanifoldOn.restrict).

The inclusion of an open subset is an analytic open embedding

noncomputable def Manifold.inclusionInv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) (x : ↥U) : M.carrier → (M.restrict U).carrier

The local inverse of the inclusion U → M at a point of U: the codomain restriction of the identity on U, an arbitrary point off U.

Equations

• Manifold.inclusionInv M U x y = if h : y ∈ U then ⟨y, h⟩ else x

theorem Manifold.inclusionInv_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) (x : ↥U) {y : M.carrier} (hy : y ∈ U) : inclusionInv M U x y = ⟨y, hy⟩

theorem Manifold.val_inclusionInv_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) (x : ↥U) {y : M.carrier} (hy : y ∈ U) : (M.inclusion U) (inclusionInv M U x y) = y

noncomputable def Manifold.inclusionPartialDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) (x : ↥U) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (M.restrict U).carrier M.carrier ⊤

The inclusion of an open subset as an analytic isomorphism onto it.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.isLocalDiffeomorph_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(M.inclusion U)

The inclusion of an open subset is a local analytic isomorphism.

theorem Manifold.isAnalyticOpenEmbedding_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : IsAnalyticOpenEmbedding (M.inclusion U)

The inclusion of an open subset is an analytic open embedding.

theorem Manifold.range_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : Set.range ⇑(M.inclusion U) = ↑U

A chart domain is a chart union with one piece

def Manifold.chartDomain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (x : M.carrier) : TopologicalSpace.Opens M.carrier

The chart domain of a point, as an open subset.

Equations

• Manifold.chartDomain x = { carrier := (chartAt E x).source, is_open' := ⋯ }

theorem Manifold.mem_chartDomain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (x : M.carrier) : x ∈ chartDomain x

theorem Manifold.isCountableChartUnion_restrict_chartDomain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (x : M.carrier) : (M.restrict (chartDomain x)).IsCountableChartUnion

A chart domain, as a manifold, is a countable chart union with one piece — its own chart restricted (Mathlib's chart of the open subset at the point).

The local cover

theorem Manifold.exists_countable_chartDomain_cover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} : ∃ (t : Set M.carrier), t.Countable ∧ ⋃ x ∈ t, ↑(chartDomain x) = Set.univ

A countable set of points whose chart domains cover M (second countability).

Closed submanifolds of an open subset, read in the bundled open subset

theorem Manifold.image_inclusionInv_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (U : TopologicalSpace.Opens M.carrier) (p : (M.restrict U).carrier) (Y : Set M.carrier) : ↑(inclusionPartialDiffeomorph M U p).symm.toPartialEquiv '' (Y ∩ (inclusionPartialDiffeomorph M U p).symm.source) = ⇑(M.inclusion U) ⁻¹' Y ∩ (inclusionPartialDiffeomorph M U p).symm.target

The inverse of the inclusion of U maps a subset of U onto its preimage in the bundled U.

theorem Manifold.IsClosedSubmanifoldOn.restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (U : TopologicalSpace.Opens M.carrier) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifoldOn ψ₀ (↑U) Y c) : IsClosedSubmanifold ψ₀ (⇑(M.inclusion U) ⁻¹' Y) c

A closed submanifold of the open subset U (IsClosedSubmanifoldOn) is a closed submanifold of the manifold U — its adapted charts transported along the inverse of the inclusion (transportChart).