An analytic space from an open cover by analytic pieces

A Hausdorff K-local-ringed space Y with a countable open cover (W i) such that every open subspace Y | W i is K-isomorphic to an analytic K-space is an analytic K-space (AnalyticSpace.ofOpenCover): in the definition of [Hir64, Ch. 0, §1, pp. 119–120], clause (i) is local and transports along the isomorphisms, clause (ii), countability at infinity, is inherited from countably many σ-compact open subsets, and clause (iii), Hausdorffness, is assumed. This is how the space glued from local complexifications, or from local resolutions, receives its analytic structure (gluedAnalytic, Hironaka.AnalyticSpace.Glue.KSpace): the pieces are the glued open subsets ι_i(Y_i), isomorphic to the Y_i, and the Hausdorffness comes from Hironaka.AnalyticSpace.Glue.Topology.

Conventions. Y.restrictOpen W is the open subspace; the local models are transported with restrictOpenIso and restrictOpen_restrictOpen_iso ((Y | W) | U ≅ Y | imageOpens W U, Hironaka.AnalyticSpace.OpenSubspaceLemmas). A single piece W = ⊤ gives Y ≅ Z an analytic space; Y = ∅ with ι empty gives the empty analytic space.

noncomputable def AnalyticSpace.ofOpenCover {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) [T2Space ↑↑Y.toPresheafedSpace] {ι : Type u} [Countable ι] (W : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hcov : ⋃ (i : ι), ↑(W i) = Set.univ) (Z : ι → AnalyticSpace K) (e : (i : ι) → (Y.restrictOpen (W i)).KIso (Z i).toKLocallyRingedSpace) : AnalyticSpace K

An analytic K-space structure on a Hausdorff K-space with a countable open cover by opens K-isomorphic to analytic spaces.

Equations

• AnalyticSpace.ofOpenCover Y W hcov Z e = { toKLocallyRingedSpace := Y, locallyModel := ⋯, t2 := ⋯, sigmaCompact := ⋯ }