The coproduct in An/K: universal property and the isomorphism criterion

The facts about AnalyticSpace.sigma read off the construction of Hironaka/AnalyticSpace/Sigma.lean (the morphisms of An/K being those of ℜ/K), and the colimit structure of the cofan (sigma X, sigmaι X) (isColimitSigmaCofan, hasCoproduct): An/K has the coproduct of every countable family.

isIso_sigmaDesc_of_isOpenImmersion is the tool for identifying a space with a coproduct: the descent sigmaDesc f of a family of open immersions f i : X i ⟶ Y with pairwise disjoint images covering Y is an isomorphism — its base map is a bijective open map, hence a homeomorphism, and its stalk maps are isomorphisms because sigmaι X i ≫ sigmaDesc f = f i with both sigmaι X i and f i open immersions (the criterion isIso_of_isIso_base_of_stalkMap_bijective of Hironaka/AnalyticSpace/IsoCriterion.lean). This is how Sp(Σ i, M i) ≅ ∐ Sp(M i) (toSpaceSigmaIso, Hironaka/AnalyticSpace/Manifold/Sigma.lean) and the decomposition of a non-singular space into its pure-dimensional strata (stratumSigmaIso, Hironaka/AnalyticSpace/Manifold/SigmaStratum.lean) are proved; both are restated in Hironaka/AnalyticSpace/SigmaCoproductLemmas.lean.

instance AnalyticSpace.isOpenImmersion_sigmaι {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) (i : ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(sigmaι X i)

The injections of the coproduct in An/K are open immersions.

theorem AnalyticSpace.sigmaι_toFun_injective {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) (i : ι) : Function.Injective ↑(sigmaι X i)

The injections are injective on points.

theorem AnalyticSpace.sigmaι_toFun_ne {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) {i j : ι} (hij : i ≠ j) (a : ↑↑(X i).toPresheafedSpace) (b : ↑↑(X j).toPresheafedSpace) : ↑(sigmaι X i) a ≠ ↑(sigmaι X j) b

The images of distinct summands are disjoint.

theorem AnalyticSpace.exists_sigmaι_toFun_eq {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) (x : ↑↑(sigma X).toPresheafedSpace) : ∃ (i : ι) (a : ↑↑(X i).toPresheafedSpace), ↑(sigmaι X i) a = x

Every point of the coproduct lies in the image of a summand.

theorem AnalyticSpace.sigmaι_sigmaDesc {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} (f : (i : ι) → X i ⟶ Y) (i : ι) : CategoryTheory.CategoryStruct.comp (sigmaι X i) (sigmaDesc f) = f i

The descent factors the injections.

theorem AnalyticSpace.sigma_hom_ext {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} {g h : sigma X ⟶ Y} (H : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (sigmaι X i) g = CategoryTheory.CategoryStruct.comp (sigmaι X i) h) : g = h

A morphism out of the coproduct is determined by its restrictions to the summands.

theorem AnalyticSpace.toFun_sigmaDesc_toFun_sigmaι {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} (f : (i : ι) → X i ⟶ Y) (i : ι) (a : ↑↑(X i).toPresheafedSpace) : ↑(sigmaDesc f) (↑(sigmaι X i) a) = ↑(f i) a

The underlying map of the descent on the image of the i-th summand is the underlying map of f i.

noncomputable def AnalyticSpace.isColimitSigmaCofan {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (sigma X) (sigmaι X))

The cofan (sigma X, sigmaι X) is a colimit cocone: the coproduct of X in the category An/K.

Equations

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

theorem AnalyticSpace.hasCoproduct {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : CategoryTheory.Limits.HasCoproduct X

An/K has the coproduct of every countable family.

The isomorphism criterion for descents

theorem AnalyticSpace.isIso_of_isIso_toKLocallyRingedSpace {K : Type} [RCLike K] {Y Z : AnalyticSpace K} (f : Y ⟶ Z) (h : CategoryTheory.IsIso f) : CategoryTheory.IsIso f

A morphism of An/K which is an isomorphism in ℜ/K is an isomorphism (the morphisms and compositions are the same).

theorem AnalyticSpace.isIso_sigmaDesc_of_isOpenImmersion {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} (f : (i : ι) → X i ⟶ Y) [∀ (i : ι), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(f i)] (hdisj : ∀ (i j : ι), i ≠ j → ∀ (a : ↑↑(X i).toPresheafedSpace) (b : ↑↑(X j).toPresheafedSpace), ↑(f i) a ≠ ↑(f j) b) (hcover : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : ι) (a : ↑↑(X i).toPresheafedSpace), ↑(f i) a = y) : CategoryTheory.IsIso (sigmaDesc f)

The descent of a family of open immersions with pairwise disjoint images covering the target is an isomorphism. The base map is a bijective open map, hence a homeomorphism; the stalk maps are isomorphisms since sigmaι X i ≫ sigmaDesc f = f i with sigmaι X i and f i open immersions.