Countable disjoint unions of analytic K-spaces

The coproduct of a countable family of analytic K-spaces, in the category ℜ/K of K-local-ringed spaces and in An/K [Hir64, Ch. 0, §1]. Not in the sources as a stated result; the construction is Mathlib's coproduct of locally ringed spaces with the K-structure supplied through the adjunction between global sections and Spec.

• K-structures as morphisms to Spec K. Hironaka's K-structure K →+* Γ(X, 𝒪_X) of a K-local-ringed space is, under the adjunction Γ ⊣ Spec (ΓSpec.locallyRingedSpaceAdjunction), a morphism of locally ringed spaces X ⟶ Spec K (toSpecK; the field lifted to Type u, specK); a morphism of locally ringed spaces is a K-morphism exactly when it is a morphism over Spec K (Hom.comp_toSpecK, Hom.ofSpecK), and a morphism X ⟶ Spec K makes X a K-local-ringed space (ofSpecKHom, toSpecK_ofSpecKHom). This is the device by which the coproduct's constants are obtained: no global section of the colimit presheaf is built by hand.
• Coproducts in ℜ/K (KLocallyRingedSpace.coprod X for X : ι → KLocallyRingedSpace K, ι countable): the underlying locally ringed space is Mathlib's coproduct LocallyRingedSpace.coproduct of the underlying spaces (smallness of ι from countability), the K-structure the adjunct of the descent of the components' morphisms to Spec K; the injections coprodι and the descent coprodDesc are K-morphisms (coprodι_coprodDesc, coprod_hom_ext: the universal property). The injections are open immersions (Mathlib's sigma_ι_isOpenImmersion), jointly surjective (exists_coprodι_toFun_eq) with pairwise disjoint images (coprodι_toFun_ne, by descending to a two-point space); hence the coproduct of Hausdorff spaces is Hausdorff (t2Space_coprod) and the countable coproduct of σ-compact spaces is σ-compact (sigmaCompactSpace_coprod).
• Coproducts in An/K (AnalyticSpace.sigma X for X : ι → AnalyticSpace K, ι countable): the coproduct in ℜ/K with Hironaka's clauses — (i) the local-model clause componentwise (a point of the coproduct lies in the image of one summand, whose local model is transported along the open immersion by isoOfRangeEq), (ii) σ-compactness for countable ι (Hironaka's countability at infinity: the coproduct of an uncountable family is not σ-compact, which is why the index type is countable), (iii) Hausdorff. sigmaι, sigmaDesc are the coproduct's injections and descent in An/K (whose morphisms are those of ℜ/K).

The carrier of the coproduct is Mathlib's colimit, homeomorphic to — not equal to — the Σ-type Σ i, X i; statements about the coproduct are therefore made at the level of points through the injections. The index type lives in an arbitrary universe v (the strata of a non-singular space are indexed by ℕ); Countable ι supplies Small.{u} ι. The universal property and the isomorphism criterion for descents are in Hironaka/AnalyticSpace/SigmaLemmas.lean; the disjoint union of manifolds and the decomposition of a non-singular space into pure-dimensional strata are in Hironaka/AnalyticSpace/SigmaCoproductLemmas.lean.

K-structures as morphisms to Spec K

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.specK (K : Type) [RCLike K] : AlgebraicGeometry.LocallyRingedSpace

Spec K as a locally ringed space in universe u (the field lifted to Type u; an abbreviation so that the adjunction's lemmas apply to it verbatim).

Equations

• AnalyticSpace.KLocallyRingedSpace.specK K = AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op ↧(ULift.{?u.1, 0} K))

def AnalyticSpace.KLocallyRingedSpace.algebraMapULift {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : ↧(ULift.{u, 0} K) ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X.toLocallyRingedSpace)

The K-structure of X as a morphism of rings ULift K ⟶ Γ(X, 𝒪_X) in CommRingCat.

Equations

• X.algebraMapULift = CommRingCat.ofHom (X.algebraMap.comp ULift.ringEquiv.toRingHom)

noncomputable def AnalyticSpace.KLocallyRingedSpace.toSpecK {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : X.toLocallyRingedSpace ⟶ specK K

The structural morphism X ⟶ Spec K of a K-local-ringed space [Hir64, Ch. 0, §1, p. 121], the adjunct of its K-structure under Γ ⊣ Spec.

Equations

• X.toSpecK = (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace (Opposite.op ↧(ULift.{?u.1, 0} K))) X.algebraMapULift.op

theorem AnalyticSpace.KLocallyRingedSpace.homEquiv_symm_toSpecK {K : Type} [RCLike K] (X : KLocallyRingedSpace K) : (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace (Opposite.op ↧(ULift.{u, 0} K))).symm X.toSpecK = X.algebraMapULift.op

theorem AnalyticSpace.KLocallyRingedSpace.Hom.comp_toSpecK {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (↑f) Y.toSpecK = X.toSpecK

A K-morphism is a morphism over Spec K.

def AnalyticSpace.KLocallyRingedSpace.Hom.ofSpecK {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace) (hf : CategoryTheory.CategoryStruct.comp f Y.toSpecK = X.toSpecK) : X ⟶ Y

A morphism of locally ringed spaces over Spec K is a K-morphism.

Equations

• AnalyticSpace.KLocallyRingedSpace.Hom.ofSpecK f hf = ⟨f, ⋯⟩

@[simp]

theorem AnalyticSpace.KLocallyRingedSpace.Hom.ofSpecK_val {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace) (hf : CategoryTheory.CategoryStruct.comp f Y.toSpecK = X.toSpecK) : ↑(ofSpecK f hf) = f

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofSpecKHom {K : Type} [RCLike K] (X : AlgebraicGeometry.LocallyRingedSpace) (Φ : X ⟶ specK K) : KLocallyRingedSpace K

A morphism of locally ringed spaces X ⟶ Spec K makes X a K-local-ringed space: the K-structure is its adjunct (the ring-homomorphism form of a morphism to Spec K).

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.toSpecK_ofSpecKHom {K : Type} [RCLike K] (X : AlgebraicGeometry.LocallyRingedSpace) (Φ : X ⟶ specK K) : (ofSpecKHom X Φ).toSpecK = Φ

Coproducts in ℜ/K

@[reducible, inline]

abbrev AnalyticSpace.KLocallyRingedSpace.coprodDiagram {K : Type} [RCLike K] {ι : Type v} (X : ι → KLocallyRingedSpace K) : CategoryTheory.Functor (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace

The diagram of the underlying locally ringed spaces of a family of K-local-ringed spaces.

Equations

• AnalyticSpace.KLocallyRingedSpace.coprodDiagram X = CategoryTheory.Discrete.functor fun (i : ι) => (X i).toLocallyRingedSpace

noncomputable def AnalyticSpace.KLocallyRingedSpace.coprodToSpecK {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) : AlgebraicGeometry.LocallyRingedSpace.coproduct (coprodDiagram X) ⟶ specK K

The structural morphism of the coproduct to Spec K: the descent of the components'.

Equations

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

noncomputable def AnalyticSpace.KLocallyRingedSpace.coprod {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) : KLocallyRingedSpace K

The coproduct of a countable family of K-local-ringed spaces: Mathlib's coproduct LocallyRingedSpace.coproduct of the underlying locally ringed spaces, with the K-structure the adjunct of the descent of the components' structural morphisms to Spec K.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.coprod_toLocallyRingedSpace {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) : (coprod X).toLocallyRingedSpace = AlgebraicGeometry.LocallyRingedSpace.coproduct (coprodDiagram X)

theorem AnalyticSpace.KLocallyRingedSpace.coprod_toSpecK {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) : (coprod X).toSpecK = coprodToSpecK X

@[reducible, inline]

noncomputable abbrev AnalyticSpace.KLocallyRingedSpace.coprodιLRS {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (i : ι) : (X i).toLocallyRingedSpace ⟶ (coprod X).toLocallyRingedSpace

The injection of the i-th summand as a morphism of locally ringed spaces: the leg of Mathlib's coproduct cofan.

Equations

• AnalyticSpace.KLocallyRingedSpace.coprodιLRS X i = (AlgebraicGeometry.LocallyRingedSpace.coproductCofan (AnalyticSpace.KLocallyRingedSpace.coprodDiagram X)).ι.app { as := i }

theorem AnalyticSpace.KLocallyRingedSpace.coprodιLRS_comp_toSpecK {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (i : ι) : CategoryTheory.CategoryStruct.comp (coprodιLRS X i) (coprod X).toSpecK = (X i).toSpecK

noncomputable def AnalyticSpace.KLocallyRingedSpace.coprodι {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (i : ι) : X i ⟶ coprod X

The injection of the i-th summand into the coproduct, a K-morphism.

Equations

• AnalyticSpace.KLocallyRingedSpace.coprodι X i = AnalyticSpace.KLocallyRingedSpace.Hom.ofSpecK (AnalyticSpace.KLocallyRingedSpace.coprodιLRS X i) ⋯

theorem AnalyticSpace.KLocallyRingedSpace.coprodι_val {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (i : ι) : ↑(coprodι X i) = coprodιLRS X i

noncomputable def AnalyticSpace.KLocallyRingedSpace.coprodDesc {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → KLocallyRingedSpace K} {Y : KLocallyRingedSpace K} (f : (i : ι) → X i ⟶ Y) : coprod X ⟶ Y

The descent of a family of K-morphisms out of the summands, a K-morphism out of the coproduct.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.coprodDesc_val {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → KLocallyRingedSpace K} {Y : KLocallyRingedSpace K} (f : (i : ι) → X i ⟶ Y) : ↑(coprodDesc f) = (AlgebraicGeometry.LocallyRingedSpace.coproductCofanIsColimit (coprodDiagram X)).desc (CategoryTheory.Limits.Cofan.mk Y.toLocallyRingedSpace fun (i : ι) => ↑(f i))

theorem AnalyticSpace.KLocallyRingedSpace.coprodι_coprodDesc {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → KLocallyRingedSpace K} {Y : KLocallyRingedSpace K} (f : (i : ι) → X i ⟶ Y) (i : ι) : CategoryTheory.CategoryStruct.comp (coprodι X i) (coprodDesc f) = f i

The descent factors the injections (the coproduct's universal property, existence).

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

Two K-morphisms out of the coproduct agreeing on every summand are equal (the coproduct's universal property, uniqueness).

The injections as open immersions; points of the coproduct

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

The injections of a coproduct are open immersions (Mathlib's sigma_ι_isOpenImmersion).

theorem AnalyticSpace.KLocallyRingedSpace.Hom.isOpenEmbedding_toFun {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (a : A ⟶ B) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑a] : Topology.IsOpenEmbedding (toFun a)

The underlying map of an open immersion of K-local-ringed spaces is an open embedding.

theorem AnalyticSpace.KLocallyRingedSpace.exists_coprodι_toFun_eq {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (x : ↑↑(coprod X).toPresheafedSpace) : ∃ (i : ι) (a : ↑↑(X i).toPresheafedSpace), Hom.toFun (coprodι X i) a = x

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

theorem AnalyticSpace.KLocallyRingedSpace.coprodι_toFun_injective {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) (i : ι) : Function.Injective (Hom.toFun (coprodι X i))

The injections are injective on points.

def AnalyticSpace.KLocallyRingedSpace.propCocone {K : Type} [RCLike K] {ι : Type v} (X : ι → KLocallyRingedSpace K) (i₀ : ι) : CategoryTheory.Limits.Cocone (((coprodDiagram X).comp AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace).comp (AlgebraicGeometry.SheafedSpace.forget CommRingCat))

(Implementation) The cocone over the underlying spaces with vertex the space of propositions, sending the j-th summand to the proposition j = i₀.

Equations

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

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

The images of distinct summands are disjoint (descend to the two-point space distinguishing the i-th summand from the others; the space of propositions carries the Sierpiński topology, but only constant maps into it are used).

Hausdorff and σ-compact

theorem AnalyticSpace.KLocallyRingedSpace.t2Space_coprod {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) [∀ (i : ι), T2Space ↑↑(X i).toPresheafedSpace] : T2Space ↑↑(coprod X).toPresheafedSpace

The coproduct of Hausdorff spaces is Hausdorff (points in one summand are separated there, points in distinct summands by the summands' disjoint open images).

theorem AnalyticSpace.KLocallyRingedSpace.sigmaCompactSpace_coprod {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → KLocallyRingedSpace K) [∀ (i : ι), SigmaCompactSpace ↑↑(X i).toPresheafedSpace] : SigmaCompactSpace ↑↑(coprod X).toPresheafedSpace

The countable coproduct of σ-compact spaces is σ-compact (a countable union of the σ-compact images of the summands): Hironaka's countability at infinity.

Coproducts in An/K

noncomputable def AnalyticSpace.sigma {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : AnalyticSpace K

The coproduct of a countable family of analytic K-spaces [Hir64, Ch. 0, §1]: the coproduct in ℜ/K of the underlying K-local-ringed spaces, with Hironaka's clauses — (i) the local-model clause componentwise, (ii) σ-compact for countable ι, (iii) Hausdorff.

Equations

• AnalyticSpace.sigma X = { toKLocallyRingedSpace := AnalyticSpace.KLocallyRingedSpace.coprod fun (i : ι) => (X i).toKLocallyRingedSpace, locallyModel := ⋯, t2 := ⋯, sigmaCompact := ⋯ }

theorem AnalyticSpace.sigma_toKLocallyRingedSpace {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) : (sigma X).toKLocallyRingedSpace = KLocallyRingedSpace.coprod fun (i : ι) => (X i).toKLocallyRingedSpace

noncomputable def AnalyticSpace.sigmaι {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) (i : ι) : X i ⟶ sigma X

The injection of the i-th summand into the coproduct in An/K.

Equations

• AnalyticSpace.sigmaι X i = AnalyticSpace.KLocallyRingedSpace.coprodι (fun (i : ι) => (X i).toKLocallyRingedSpace) i

noncomputable def AnalyticSpace.sigmaDesc {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} (f : (i : ι) → X i ⟶ Y) : sigma X ⟶ Y

The descent of a family of morphisms out of the summands, in An/K.

Equations

• AnalyticSpace.sigmaDesc f = AnalyticSpace.KLocallyRingedSpace.coprodDesc f

theorem AnalyticSpace.sigmaι_def {K : Type} [RCLike K] {ι : Type v} [Countable ι] (X : ι → AnalyticSpace K) (i : ι) : sigmaι X i = KLocallyRingedSpace.coprodι (fun (i : ι) => (X i).toKLocallyRingedSpace) i

theorem AnalyticSpace.sigmaDesc_def {K : Type} [RCLike K] {ι : Type v} [Countable ι] {X : ι → AnalyticSpace K} {Y : AnalyticSpace K} (f : (i : ι) → X i ⟶ Y) : sigmaDesc f = KLocallyRingedSpace.coprodDesc f