Disjoint unions of charted spaces

The disjoint union Σ i, M i of a family of charted spaces on a common model H is charted on H: each copy Sigma.mk i '' M i is open, and the chart at ⟨i, x⟩ is the chart of M i at x read on that copy. This is the indexed form of Mathlib's binary disjoint union ChartedSpace.sum, and is how a manifold with several boundary components, such as a link exterior, has its boundary presented as one charted space.

Main definitions

• ChartedSpace.sigma: the charted space structure on Σ i, M i.

Main results

• ChartedSpace.sigma_chartAt: the chart at ⟨i, x⟩ is the chart of M i at x, lifted along the open embedding Sigma.mk i.
• ChartedSpace.sigma_chartAt_mk_apply: on the copy of M i it agrees with the chart of M i.
• ChartedSpace.mem_atlas_sigma: the atlas consists of lifted charts of the components.
• IsManifold.sigma: the disjoint union of C^n manifolds is a C^n manifold.

The construction follows Mathlib's ChartedSpace.sumOfNonempty and ChartedSpace.sum in Mathlib.Geometry.Manifold.ChartedSpace. The compatibility proof follows Mathlib's IsManifold.disjointUnion.

@[instance_reducible]

noncomputable def ChartedSpace.sigmaOfNonempty {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] [Nonempty H] : ChartedSpace H ((i : ι) × M i)

The disjoint union of a family of charted spaces modelled on a nonempty space H is a charted space over H: the chart at ⟨i, x⟩ is the chart of M i at x, lifted along Sigma.mk i.

@[instance_reducible]

noncomputable instance ChartedSpace.sigma {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] : ChartedSpace H ((i : ι) × M i)

The disjoint union of a family of charted spaces on a common model is charted on that model. When the model is empty, so is every component, and the structure is the empty one.

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

The chart of a disjoint union at ⟨i, x⟩ is the chart of M i at x, lifted along the open embedding Sigma.mk i.

@[simp]

theorem ChartedSpace.sigma_chartAt_mk_apply {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {i : ι} {x y : M i} : ↑(chartAt H ⟨i, x⟩) ⟨i, y⟩ = ↑(chartAt H x) y

On the copy of M i, the chart of a disjoint union at ⟨i, x⟩ is the chart of M i at x.

@[simp]

theorem ChartedSpace.sigma_chartAt_source {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {i : ι} {x : M i} : (chartAt H ⟨i, x⟩).source = Sigma.mk i '' (chartAt H x).source

The source of the chart of a disjoint union at ⟨i, x⟩ is the copy of the source of the chart of M i at x.

@[simp]

theorem ChartedSpace.sigma_chartAt_target {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {i : ι} {x : M i} : (chartAt H ⟨i, x⟩).target = (chartAt H x).target

The target of the chart of a disjoint union at ⟨i, x⟩ is the target of the chart of M i at x.

theorem ChartedSpace.mem_atlas_sigma {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] [h : Nonempty H] {e : OpenPartialHomeomorph ((i : ι) × M i) H} : e ∈ atlas H ((i : ι) × M i) ↔ ∃ (i : ι), ∃ f ∈ atlas H (M i), e = f.lift_openEmbedding ⋯

The atlas of a disjoint union consists of the charts in the atlases of the components, each lifted along the corresponding open embedding Sigma.mk i.

instance IsManifold.sigma {H : Type u_1} [TopologicalSpace H] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} [∀ (i : ι), IsManifold I n (M i)] : IsManifold I n ((i : ι) × M i)

A disjoint union of C^n manifolds on a common model is a C^n manifold on that model.