The coproduct of analytic maps out of a disjoint union

For an open cover X = ⋃ Uᵢ, the disjoint union X' := ∐ Uᵢ comes with a smooth surjection g : X' → X (the proof of [Kol07, Proposition 37]). On the disjoint union of analytic manifolds (ChartedSpace.sigma, IsManifold.sigma, sigmaManifold): the coproduct fun p => f p.1 p.2 of a family of C^n maps f i : M i → P is C^n (the family version of Mathlib's ContMDiff.sumElim: in the lifted charts of the disjoint union the coproduct reads as f i, extChartAt_sigma_mk), and it is surjective iff the ranges of the f i cover (surjective_sigmaDesc_iff). That the coproduct of local diffeomorphisms is a local diffeomorphism is Hironaka.Manifold.FiniteSuccession.Functor.SigmaLocalDiffeo.

theorem extChartAt_sigma_mk_symm {𝕜 : 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 : M i) (z : E) : ↑(extChartAt I ⟨i, x⟩).symm z = ⟨i, ↑(extChartAt I x).symm z⟩

The inverse of the extended chart of the disjoint union at ⟨i, x⟩ lands in the i-th piece, through the inverse of the piece's extended chart.

theorem ContMDiff.sigmaDesc {𝕜 : 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)] {f : (i : ι) → M i → P} (hf : ∀ (i : ι), ContMDiff I J n (f i)) : ContMDiff I J n fun (p : (i : ι) × M i) => f p.fst p.snd

The coproduct of a family of C^n maps out of the pieces is C^n on the disjoint union — in the lifted charts it reads as the piece's map.

theorem surjective_sigmaDesc_iff {ι : Type u_1} {M : ι → Type u_2} {P : Type u_3} (f : (i : ι) → M i → P) : (Function.Surjective fun (p : (i : ι) × M i) => f p.fst p.snd) ↔ ⋃ (i : ι), Set.range (f i) = Set.univ

[Kol07, Proposition 37] ("there is a smooth surjection g : X' → X"): the coproduct of the f i is surjective iff their ranges cover.