Disjoint unions of manifolds as coproducts of analytic spaces

Consequences of the coproduct construction of Hironaka/AnalyticSpace/Sigma.lean and Hironaka/AnalyticSpace/SigmaLemmas.lean, and of the disjoint union of analytic manifolds (sigmaManifold, sigmaMk of Hironaka/Manifold/SigmaManifold.lean), restated here for reference; nothing but the root aggregator imports this module.

• The coproduct sigma X in An/K: its underlying K-local-ringed space and locally ringed space are the coproducts of the summands', it is Hausdorff and σ-compact, and the cofan (sigma X, sigmaι X) is a colimit cocone (nonempty_isColimit_sigmaCofan). Once hasCoproduct is known, Mathlib's ∐ X exists in An/K and sigma X ≅ ∐ X canonically (IsColimit.coconePointUniqueUpToIso), but not by rfl: ∐ X is a Classical.choice, sigma X the explicit construction.
• The space of a disjoint union of manifolds is the coproduct of the spaces of the summands (toSpace_sigma, toSpace_sigma_hom): in the charts of Σ i, M i (the charts of the M i lifted along the open embeddings Sigma.mk i) the inclusion of a summand reads as the identity, so Sp(Sigma.mk i) is an open immersion, and the descent ∐ Sp(M i) ⟶ Sp(Σ i, M i) of these open immersions with disjoint images covering the union is an isomorphism by isIso_sigmaDesc_of_isOpenImmersion (toSpaceSigmaIso, in Hironaka/AnalyticSpace/Manifold/).
• A non-singular analytic K-space is the countable disjoint union of pure-dimensional manifolds (nonsingular_eq_sigma_dim): the strata X_d = {x | dim 𝒪_{X,x} = d} are open, pairwise disjoint, cover X, and each is K-isomorphic to the space of a manifold modelled on K^d (stratumManifold, stratumSigmaIso, in Hironaka/AnalyticSpace/Manifold/), so the same criterion gives X ≅ ∐ d, Sp(X_d) with the points of local dimension d the points of the d-th summand. This exhibits Hironaka's non-singular analytic K-spaces [Hir64, Ch. 0, §1, p. 121] as disjoint unions of manifolds of the several dimensions (the decomposition itself is stratumSigmaIso).

The coproduct in An/K

theorem AnalyticSpace.sigma_toLocallyRingedSpace {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : (sigma X).toLocallyRingedSpace = AlgebraicGeometry.LocallyRingedSpace.coproduct (KLocallyRingedSpace.coprodDiagram fun (i : ι) => (X i).toKLocallyRingedSpace)

theorem AnalyticSpace.sigma_t2Space {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : T2Space ↑↑(sigma X).toPresheafedSpace

theorem AnalyticSpace.sigma_sigmaCompactSpace {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : SigmaCompactSpace ↑↑(sigma X).toPresheafedSpace

theorem AnalyticSpace.nonempty_isColimit_sigmaCofan {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (sigma X) (sigmaι X)))

Disjoint unions of manifolds and the strata of a non-singular space

theorem AnalyticSpace.toSpace_sigma {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) : ∃ (e : toSpace ψ (Manifold.sigmaManifold M) ≅ sigma fun (i : ι) => toSpace ψ (M i)), ∀ (i : ι) (x : (M i).carrier), ↑e.hom ⟨i, x⟩ = ↑(sigmaι (fun (i : ι) => toSpace ψ (M i)) i) x

theorem AnalyticSpace.toSpace_sigma_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) : ∃ (e : toSpace ψ (Manifold.sigmaManifold M) ≅ sigma fun (i : ι) => toSpace ψ (M i)), ∀ (i : ι), CategoryTheory.CategoryStruct.comp (toSpaceHom ψ (Manifold.sigmaMk M i)) e.hom = sigmaι (fun (i : ι) => toSpace ψ (M i)) i

theorem AnalyticSpace.nonsingular_eq_sigma_dim {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) : ∃ (M : (d : ℕ) → AnalyticManifold K (Fin d → K)) (e : X ≅ sigma fun (d : ℕ) => toSpace (ContinuousLinearEquiv.refl K (Fin d → K)) (M d)), ∀ (d : ℕ) (x : ↑↑X.toPresheafedSpace), ringKrullDim ↑(X.presheaf.stalk x) = ↑d ↔ ∃ (m : (M d).carrier), ↑e.hom x = ↑(sigmaι (fun (d : ℕ) => toSpace (ContinuousLinearEquiv.refl K (Fin d → K)) (M d)) d) m