Chart domains transport along analytic open embeddings; countable chart unions

An analytic open embedding ι : N → M (a local analytic isomorphism that is injective) is an analytic isomorphism onto its open range: IsAnalyticOpenEmbedding.toPartialDiffeomorph (source univ, target range ι, inverse Function.invFun ι, analytic because it agrees near every point of the range with the inverse of a local inverse of ι). Along it a chart of N transports to a chart of M with source the image (transportChart), so a countable disjoint union of countable chart unions is a countable chart union (isCountableChartUnion_of_cover), whence the local triples of [Kol07, Proposition 37] are closed under countable disjoint unions (closedUnderSigma_isLocal, clause (2)(ii) of [Kol07, Theorem 105]; [Kol07, Warning 38]) and the disjoint union of chart unions is one (isCountableChartUnion_sigma).

theorem Manifold.IsAnalyticOpenEmbedding.isOpenEmbedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {ι : AnalyticMap N M} (hι : IsAnalyticOpenEmbedding ι) : Topology.IsOpenEmbedding ⇑ι

theorem Manifold.IsAnalyticOpenEmbedding.isOpen_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {ι : AnalyticMap N M} (hι : IsAnalyticOpenEmbedding ι) : IsOpen (Set.range ⇑ι)

theorem Manifold.IsAnalyticOpenEmbedding.contMDiffAt_invFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {ι : AnalyticMap N M} (hι : IsAnalyticOpenEmbedding ι) [Nonempty N.carrier] {y : M.carrier} (hy : y ∈ Set.range ⇑ι) : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (Function.invFun ⇑ι) y

Near a point of the range, Function.invFun ι is the inverse of a local inverse of ι.

noncomputable def Manifold.IsAnalyticOpenEmbedding.toPartialDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {ι : AnalyticMap N M} (hι : IsAnalyticOpenEmbedding ι) [Nonempty N.carrier] : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤

An analytic open embedding as an analytic isomorphism onto its range.

Equations

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

theorem Manifold.IsAnalyticOpenEmbedding.exists_chart_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} {ι : AnalyticMap N M} (hι : IsAnalyticOpenEmbedding ι) [Nonempty N.carrier] {φ : OpenPartialHomeomorph N.carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N.carrier) : ∃ χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier, χ.source = ⇑ι '' φ.source

A chart of N transports along the embedding to a chart of M with source the image of its source (transportChart).

theorem Manifold.isClopen_range_of_cover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) (hdisj : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) (i : σ) : IsClopen (Set.range ⇑(ι i))

A family of analytic open embeddings with pairwise disjoint ranges covering M: each range is clopen (its complement is the union of the other ranges).

theorem AnalyticManifold.isCountableChartUnion_of_cover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), Manifold.IsAnalyticOpenEmbedding (ι i)) (hdisj : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) (hN : ∀ (i : σ), (N i).IsCountableChartUnion) : M.IsCountableChartUnion

[Kol07, Warning 38], Proposition 37: a manifold covered by a countable family of analytic open embeddings with pairwise disjoint ranges, each from a countable chart union, is a countable chart union — the pieces are the images of the pieces, clopen because the ranges are clopen, with the charts transported along the embeddings.

theorem Manifold.pairwise_disjoint_range_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(sigmaMk N i)) (Set.range ⇑(sigmaMk N j))

theorem Manifold.iUnion_range_sigmaMk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) : ⋃ (i : σ), Set.range ⇑(sigmaMk N i) = Set.univ

theorem Manifold.AnalyticTriple.closedUnderSigma_isLocal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : ClosedUnderSigma fun {M : AnalyticManifold 𝕜 E} => IsLocal

[Kol07, Warning 38] ([Kol07, Theorem 105, (2)(ii)] for the classes of [Kol07, Proposition 37]): the local triples are closed under countable disjoint unions.

theorem AnalyticManifold.isCountableChartUnion_sigma {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : Type u} [Countable σ] (N : σ → AnalyticManifold 𝕜 E) (hN : ∀ (i : σ), (N i).IsCountableChartUnion) : (Manifold.sigmaManifold N).IsCountableChartUnion

[Kol07, Warning 38]: a countable disjoint union of countable chart unions is a countable chart union.