The space of a disjoint union of manifolds is the coproduct

The functor Sp sends the disjoint union Σ i, M i of a countable family of analytic manifolds (the bundled manifold sigmaManifold M, Hironaka.Manifold.SigmaManifold) to the coproduct AnalyticSpace.sigma (fun i => Sp(M i)) of analytic spaces, compatibly with the inclusions of the summands.

• contMDiffAt_sigmaMk_comp_iff: a map into a summand is C^n iff its composite with the inclusion Sigma.mk i into the disjoint union is: in the lifted charts of the disjoint union (ChartedSpace.sigma_chartAt) the inclusion reads as the identity, so both sides unfold to the same ContDiffWithinAt (the family version of Mathlib's ContMDiff.inl, in both directions).
• isOpenImmersion_ofManifoldHom_sigmaMk: Sp(Sigma.mk i) is an open immersion: the base map is the open embedding Sigma.mk i, and an analytic function on an open subset of the image of M i is the same as an analytic function on the corresponding open subset of M i (the argument of isOpenImmersion_ofManifoldHom_val for open submanifolds, with the lemma above in place of Mathlib's liftPropWithinAt_subtypeVal_comp_iff).
• toSpaceSigmaIso ψ M : Sp(Σ i, M i) ≅ ∐ i, Sp(M i): the inverse of the descent sigmaDesc (fun i => Sp(Sigma.mk i)), an isomorphism by isIso_sigmaDesc_of_isOpenImmersion because the Sp(Sigma.mk i) are open immersions with pairwise disjoint images covering Sp(Σ i, M i); it is compatible with the injections (toSpaceHom_sigmaMk_comp_toSpaceSigmaIso_hom, and on points toFun_toSpaceSigmaIso_hom_mk).

A non-singular analytic space is the disjoint union of its pure-dimensional strata, each the space of a manifold [Hir64, Ch. 0, §1, p. 121]; this module and Hironaka.AnalyticSpace.Manifold.SigmaStratum make the two descriptions of such a space, as one manifold whose components may have different dimensions and as a coproduct of spaces, interchangeable. The isomorphism toSpaceSigmaIso is used in Hironaka.AnalyticSpace.SigmaCoproductLemmas; the analyticity criterion contMDiff_sigmaMk_comp_iff and the chart formula extChartAt_sigma_mk are used for the resolution functor on a disjoint union (Hironaka.Manifold.FiniteSuccession.Functor.SigmaDesc, Hironaka.Manifold.FiniteSuccession.Functor.SigmaTriple) and in the gluing of local resolutions (Hironaka.Resolution.Analytic.Kol07Thm45.PadIdeal, Hironaka.Resolution.Analytic.Kol07Thm45.PieceAmbientIncl).

Analyticity through the inclusion of a summand

theorem extChartAt_sigma_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {ι : Type u_7} {M : ι → Type u_8} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] [Nonempty H] {i : ι} (x y : M i) : ↑(extChartAt I ⟨i, x⟩) ⟨i, y⟩ = ↑(extChartAt I x) y

The extended chart of the disjoint union at a point of the i-th summand, evaluated on that summand, is the extended chart of the summand.

theorem contMDiffAt_sigmaMk_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {P : Type u_6} [TopologicalSpace P] [ChartedSpace H' P] {ι : Type u_7} {M : ι → Type u_8} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {i : ι} {h : P → M i} {p : P} : ContMDiffAt J I n (Sigma.mk i ∘ h) p ↔ ContMDiffAt J I n h p

A map into a summand is C^n at a point iff its composite with the inclusion into the disjoint union is: in the lifted charts the inclusion is the identity (the family version of Mathlib's ContMDiff.inl, in both directions).

theorem contMDiff_sigmaMk_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {P : Type u_6} [TopologicalSpace P] [ChartedSpace H' P] {ι : Type u_7} {M : ι → Type u_8} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace H (M i)] {i : ι} {h : P → M i} : ContMDiff J I n (Sigma.mk i ∘ h) ↔ ContMDiff J I n h

A map into a summand is C^n iff its composite with the inclusion is.

Sp(Sigma.mk i) is an open immersion

instance AnalyticSpace.isOpenImmersion_ofManifoldHom_sigmaMk {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {ι : Type u} {M : ι → Type u} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace E (M i)] (i : ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(KLocallyRingedSpace.ofManifoldHom (Sigma.mk i) ⋯)

Sp of the inclusion of a summand into the disjoint union is an open immersion: the base map is the open embedding Sigma.mk i, and analytic functions on an open subset of the image correspond to analytic functions on the corresponding open subset of the summand (the argument of isOpenImmersion_ofManifoldHom_val).

Sp(Σ i, M i) ≅ ∐ Sp(M i)

instance AnalyticSpace.isOpenImmersion_toSpaceHom_sigmaMk {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) (i : ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(toSpaceHom ψ (Manifold.sigmaMk M i))

Sp of the inclusion of a summand, as a morphism of analytic spaces, is an open immersion.

noncomputable def AnalyticSpace.sigmaToSpaceDesc {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) : (sigma fun (i : ι) => toSpace ψ (M i)) ⟶ toSpace ψ (Manifold.sigmaManifold M)

The descent ∐ Sp(M i) ⟶ Sp(Σ i, M i) of the Sp(Sigma.mk i).

Equations

• AnalyticSpace.sigmaToSpaceDesc ψ M = AnalyticSpace.sigmaDesc fun (i : ι) => AnalyticSpace.toSpaceHom ψ (Manifold.sigmaMk M i)

theorem AnalyticSpace.isIso_sigmaToSpaceDesc {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) : CategoryTheory.IsIso (sigmaToSpaceDesc ψ M)

The descent is an isomorphism: the Sp(Sigma.mk i) are open immersions with pairwise disjoint images covering the disjoint union (isIso_sigmaDesc_of_isOpenImmersion).

noncomputable def AnalyticSpace.toSpaceSigmaIso {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) : toSpace ψ (Manifold.sigmaManifold M) ≅ sigma fun (i : ι) => toSpace ψ (M i)

Sp of a countable disjoint union of analytic manifolds is the coproduct of the spaces of the summands: the inverse of the descent of the Sp(Sigma.mk i).

Equations

• AnalyticSpace.toSpaceSigmaIso ψ M = (CategoryTheory.asIso (AnalyticSpace.sigmaToSpaceDesc ψ M)).symm

theorem AnalyticSpace.toSpaceHom_sigmaMk_comp_toSpaceSigmaIso_hom {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) (i : ι) : CategoryTheory.CategoryStruct.comp (toSpaceHom ψ (Manifold.sigmaMk M i)) (toSpaceSigmaIso ψ M).hom = sigmaι (fun (i : ι) => toSpace ψ (M i)) i

The isomorphism is compatible with the injections: Sp(Sigma.mk i) composed with it is the i-th injection of the coproduct.

theorem AnalyticSpace.toFun_toSpaceSigmaIso_hom_mk {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {ι : Type u} [Countable ι] (M : ι → AnalyticManifold K E) (i : ι) (x : (M i).carrier) : KLocallyRingedSpace.Hom.toFun (toSpaceSigmaIso ψ M).hom ⟨i, x⟩ = KLocallyRingedSpace.Hom.toFun (sigmaι (fun (i : ι) => toSpace ψ (M i)) i) x

On points, the isomorphism carries ⟨i, x⟩ to the image of x under the i-th injection.