Disjoint unions of manifolds indexed by a type

Mathlib has the disjoint union of two manifolds (ChartedSpace.sum, IsManifold.disjointUnion) but not of a family. The Hironaka library forms countable disjoint unions Σ i, M i of manifolds modelled on one space (the coproducts of analytic manifolds and of analytic spaces); this module adds the family version, mirroring Mathlib's binary one: the charts of Σ i, M i are the charts of the M i lifted along the open embeddings Sigma.mk i (ChartedSpace.sigma), and Σ i, M i is a C^n manifold when every M i is (IsManifold.sigma), chart changes between different summands having empty domain. The bundled disjoint union of a countable family of analytic manifolds is Manifold.sigmaManifold.

@[instance_reducible]

noncomputable def ChartedSpace.sigmaOfNonempty {ι : 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] : ChartedSpace H ((i : ι) × M i)

The disjoint union of a family of charted spaces modelled on a nonempty H is a charted space modelled on H: the charts are the charts of the M i, lifted along the open embeddings Sigma.mk i.

Equations

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

@[instance_reducible]

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

The disjoint union Σ i, M i of charted spaces modelled on H is a charted space modelled on H (for H empty every M i is empty, and so is the union).

Equations

• ChartedSpace.sigma M = if h : Nonempty H then ChartedSpace.sigmaOfNonempty M else have hM := ⋯; have this := ⋯; ChartedSpace.empty H ((i : ι) × M i)

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

instance IsManifold.sigma {𝕜 : 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)] [hM : ∀ (i : ι), IsManifold I n (M i)] : IsManifold I n ((i : ι) × M i)

The disjoint union Σ i, M i of a family of C^n manifolds modelled on (E, H) is a C^n manifold modelled on (E, H): chart changes within one M i are those of M i, and chart changes between different summands have empty domain.