The disjoint union of a countable family of analytic manifolds

sigmaManifold M : AnalyticManifold K E, for a countable family M : ι → AnalyticManifold K E with ι : Type u (the universe of the manifolds, so that the Σ-type lives there too): the Σ-type with the charted-space and manifold structure ChartedSpace.sigma, IsManifold.sigma (the chart at p is the chart of the summand at p.2, lifted along Sigma.mk p.1: ChartedSpace.sigma_chartAt), Hausdorff by Mathlib's Sigma.t2Space and second countable for a countable index. The inclusion Sigma.mk i of a summand is C^n (ContMDiff.sigmaMk, the family version of Mathlib's ContMDiff.inl: in the lifted charts it is the identity), and sigmaMk M i is the bundled analytic map M i → sigmaManifold M.

This bundle is the coproduct of analytic manifolds modelled on E; the coproduct in the category of analytic spaces is formed from it (Hironaka/AnalyticSpace/Manifold/Sigma.lean), and the gluing arguments of the Hironaka library use it to assemble a manifold from a countable family of pieces.

theorem ChartedSpace.sigma_chartAt {ι : Type u_1} {H : Type u_2} [TopologicalSpace H] (M : ι → Type u_3) [(i : ι) → TopologicalSpace (M i)] [cm : (i : ι) → ChartedSpace H (M i)] [Nonempty H] (p : (i : ι) × M i) : chartAt H p = (ChartedSpace.chartAt p.snd).lift_openEmbedding ⋯

theorem ContMDiff.sigmaMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] (i : ι) : ContMDiff I I n (Sigma.mk i)

The inclusion of a summand into the disjoint union Σ i, M i (with the charted-space structure ChartedSpace.sigma) is C^n: in the lifted charts it is the identity. The family version of Mathlib's ContMDiff.inl.

noncomputable def Manifold.sigmaManifold {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) : AnalyticManifold K E

The disjoint union of a countable family of analytic manifolds as a bundled analytic manifold: the Σ-type with the charted-space and manifold structure ChartedSpace.sigma, IsManifold.sigma, Hausdorff (Sigma.t2Space) and second countable (countable index).

Equations

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

theorem Manifold.sigmaManifold_carrier {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) : (sigmaManifold M).carrier = ((i : ι) × (M i).carrier)

noncomputable def Manifold.sigmaMk {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) (i : ι) : AnalyticMap (M i) (sigmaManifold M)

The inclusion of the i-th summand as an analytic map.

Equations

• Manifold.sigmaMk M i = ⟨fun (x : (M i).carrier) => ⟨i, x⟩, ⋯⟩

theorem Manifold.sigmaMk_apply {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) (i : ι) (x : (M i).carrier) : (sigmaMk M i) x = ⟨i, x⟩