A K-space is the gluing of any open cover of itself

For a K-space Y and a family of open subsets U : J → Opens Y, the K-gluing data coverData Y U (Hironaka.AnalyticSpace.Glue.Data) has pieces Y | U i, open subsets W i j = (U i)⁻¹ (U j) and the identity transitions (the two double restrictions (Y | U i) | W i j and (Y | U j) | W j i are both the trace of U i ⊓ U j, so they are canonically K-isomorphic over Y: coverT). Its glued K-space maps to Y (gluedCoverDesc, the universal property of the multicoequalizer), and when the U i cover Y this map is an open immersion with full range, hence a K-isomorphism (coverIso), with ιK i ≫ coverIso.hom = ofRestrict Y (U i). This is how the complexified space X(ℂ) is presented as a glued space in the gluing of local complexifications (Hironaka.AnalyticSpace.Glue.Morphism), so that a morphism out of it is assembled from morphisms on the pieces by the universal property.

Conventions. Every identity between the transitions is proved by cancelling the monomorphic inclusions into Y (hom_ext_of_comp_eq): all the maps of coverData are the identity of Y on points. The descent morphism is an open immersion by Mathlib's LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (an open embedding of the base with isomorphic stalk maps, both read off from ι i ≫ gluedCoverDesc = ofRestrict). One open subset U = ⊤ gives the glued space Y | ⊤, isomorphic to Y (restrictOpenTopIso); the empty family gives the empty glued space, which covers Y only if Y is empty. Not in the sources.

def AnalyticSpace.Glue.coverW {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : TopologicalSpace.Opens ↑↑(Y.restrictOpen (U i)).toPresheafedSpace

The open of the piece Y | U i glued to Y | U j: the trace of U j.

Equations

• AnalyticSpace.Glue.coverW Y U i j = (TopologicalSpace.Opens.map (↑(Y.ofRestrict (U i))).base).obj (U j)

theorem AnalyticSpace.Glue.mem_coverW {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {i j : J} {x : ↑↑(Y.restrictOpen (U i)).toPresheafedSpace} : x ∈ coverW Y U i j ↔ ↑x ∈ U j

theorem AnalyticSpace.Glue.range_toFun_incl₂_coverW {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : Set.range (KLocallyRingedSpace.Hom.toFun (incl₂ Y (U i) (coverW Y U i j))) = ↑(U i) ∩ ↑(U j)

noncomputable def AnalyticSpace.Glue.coverT {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : (Y.restrictOpen (U i)).restrictOpen (coverW Y U i j) ⟶ (Y.restrictOpen (U j)).restrictOpen (coverW Y U j i)

The identity transition between the two traces of U i ⊓ U j.

Equations

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

theorem AnalyticSpace.Glue.coverT_comp_incl₂ {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : CategoryTheory.CategoryStruct.comp (coverT Y U i j) (incl₂ Y (U j) (coverW Y U j i)) = incl₂ Y (U i) (coverW Y U i j)

theorem AnalyticSpace.Glue.toFun_coverT {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) (x : ↑↑((Y.restrictOpen (U i)).restrictOpen (coverW Y U i j)).toPresheafedSpace) : ↑↑(KLocallyRingedSpace.Hom.toFun (coverT Y U i j) x) = ↑↑x

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.coverCore {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : KGlueCore K

The K-gluing core of an open cover: pieces Y | U i, identity transitions.

Equations

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

theorem AnalyticSpace.Glue.coverCore_t {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : (coverCore Y U).t i j = coverT Y U i j

theorem AnalyticSpace.Glue.coverCore_tRes_comp_incl₂ {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j k : J) : CategoryTheory.CategoryStruct.comp ((coverCore Y U).tRes i j k) (incl₂ Y (U j) (coverW Y U j k ⊓ coverW Y U j i)) = incl₂ Y (U i) (coverW Y U i j ⊓ coverW Y U i k)

The restricted transitions of the cover core are the identity of Y on points: they commute with the inclusions into Y.

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.coverData {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : KGlueData K

The K-gluing data of an open cover.

Equations

• AnalyticSpace.Glue.coverData Y U = { toKGlueCore := AnalyticSpace.Glue.coverCore Y U, cocycle := ⋯ }

The descent to Y

theorem AnalyticSpace.Glue.coverData_compat {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i j : J) : CategoryTheory.CategoryStruct.comp ((coverData Y U).f i j) ↑(Y.ofRestrict (U i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑((coverData Y U).t i j)) ((coverData Y U).f j i)) ↑(Y.ofRestrict (U j))

noncomputable def AnalyticSpace.Glue.gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : (coverData Y U).gluedK ⟶ Y

The descent of the inclusions Y | U i ⟶ Y to the glued K-space of the cover.

Equations

• AnalyticSpace.Glue.gluedCoverDesc Y U = (AnalyticSpace.Glue.coverData Y U).descK (fun (i : (AnalyticSpace.Glue.coverData Y U).J) => Y.ofRestrict (U i)) ⋯

theorem AnalyticSpace.Glue.ιK_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i : J) : CategoryTheory.CategoryStruct.comp ((coverData Y U).ιK i) (gluedCoverDesc Y U) = Y.ofRestrict (U i)

theorem AnalyticSpace.Glue.toFun_gluedCoverDesc_ιK {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (i : J) (y : ↑↑(Y.restrictOpen (U i)).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U) (KLocallyRingedSpace.Hom.toFun ((coverData Y U).ιK i) y) = ↑y

theorem AnalyticSpace.Glue.gluedCoverDesc_injective {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : Function.Injective (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U))

theorem AnalyticSpace.Glue.gluedCoverDesc_surjective {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : J), y ∈ U i) : Function.Surjective (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U))

theorem AnalyticSpace.Glue.isOpenMap_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : IsOpenMap (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U))

theorem AnalyticSpace.Glue.continuous_toFun_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : Continuous (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U))

theorem AnalyticSpace.Glue.isOpenEmbedding_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : Topology.IsOpenEmbedding (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U))

theorem AnalyticSpace.Glue.isIso_stalkMap_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (z : ↑(coverData Y U).glued.toTopCat) : CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(gluedCoverDesc Y U)) z)

instance AnalyticSpace.Glue.isOpenImmersion_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(gluedCoverDesc Y U)

theorem AnalyticSpace.Glue.range_toFun_gluedCoverDesc {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : J), y ∈ U i) : Set.range (KLocallyRingedSpace.Hom.toFun (gluedCoverDesc Y U)) = Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.id Y))

noncomputable def AnalyticSpace.Glue.coverIso {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : J), y ∈ U i) : (coverData Y U).gluedK.KIso Y

A K-space is K-isomorphic to the glued K-space of any open cover of itself.

Equations

• AnalyticSpace.Glue.coverIso Y U hU = AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq (AnalyticSpace.Glue.gluedCoverDesc Y U) (CategoryTheory.CategoryStruct.id Y) ⋯

theorem AnalyticSpace.Glue.coverIso_hom {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : J), y ∈ U i) : (coverIso Y U hU).hom = gluedCoverDesc Y U

theorem AnalyticSpace.Glue.ιK_comp_coverIso_hom {K : Type} [RCLike K] (Y : KLocallyRingedSpace K) {J : Type u} (U : J → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hU : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (i : J), y ∈ U i) (i : J) : CategoryTheory.CategoryStruct.comp ((coverData Y U).ιK i) (coverIso Y U hU).hom = Y.ofRestrict (U i)