Gluing morphisms of locally ringed spaces along an open cover

Morphisms of locally ringed spaces g i : X | Uᵢ → W defined on the members of an open cover of X and agreeing on the overlaps X | (Uᵢ ⊓ Uⱼ) glue to a morphism X → W restricting to the g i — the existence half of the locality of morphisms (Hironaka/AnalyticSpace/HomLocal.lean is the uniqueness half). Hironaka's universal mapping property (**) of a monoidal transformation [Hir64, Ch. 0, §2] needs it: the lift of a test pair (Y', f') into the blow-up is constructed on the members of an open cover of Y' (over the complement of the centre and in each blow-up chart) and glued; the pieces agree on the overlaps by uniqueness. Elementary sheaf theory, not in the sources; stated for general locally ringed spaces.

• restrictIncl X h : X | V → X | W for nested opens V ≤ W — the inclusion of subtypes with the restriction of sections along the inclusion of image opens as sheaf component, so that its sheaf component is a restriction map of 𝒪_X and restrictIncl ≫ ofRestrict W = ofRestrict V. Compatibility of the pieces is stated with it: GlueCompatible U g says restrictIncl ≫ g i = restrictIncl ≫ g j on X | (Uᵢ ⊓ Uⱼ).
• The base map is pasted from the bases of the pieces (ContinuousMap.liftCover).
• A section s of 𝒪_W over V pulls back to the pieces (g i)^* s over the image opens gluePieceOpens i V = Uᵢ ∩ b⁻¹ V; they are compatible because their germs agree, through the overlap space, when the pieces do (germ_gluePieceSection_of_overlap, gluePieceSection_isCompatible), and glue uniquely (TopCat.Sheaf.existsUnique_gluing') to glueSection V s; the glued sections form a ring homomorphism and a natural transformation by the uniqueness of the gluing.
• The stalk map of the glued morphism at x ∈ Uᵢ is the stalk map of g i, read through the identification of the image points and the stalk of the open subspace (glueHom_stalkMap), hence local; ofRestrict ≫ glueOfCover = g i by SheafedSpace.hom_stalk_ext.
• The K-morphism form (KLocallyRingedSpace.glueOfCover): the glued morphism respects the K-structures because its global sections restrict to those of the pieces.

Mathlib has LocallyRingedSpace.GlueData (gluing spaces), IsOpenImmersion.lift and the sheaf-level existsUnique_gluing', but no gluing of morphisms out of a space covered by opens; Scheme.OpenCover.glueMorphisms is for schemes.

def AnalyticSpace.restrictInclHom (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) : (X.restrict ⋯).toPresheafedSpace ⟶ (X.restrict ⋯).toPresheafedSpace

The inclusion X | V → X | W of the restrictions to nested opens V ≤ W, as a morphism of presheafed spaces: the inclusion of subtypes on points, restriction of sections along the inclusion of image opens on sheaves.

Equations

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

theorem AnalyticSpace.restrictInclHom_base_apply (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) (p : ↑(X.restrict ⋯).toTopCat) : (CategoryTheory.ConcreteCategory.hom (restrictInclHom X h).base) p = ⟨↑p, ⋯⟩

theorem AnalyticSpace.restrictInclHom_comp_ofRestrict (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) : CategoryTheory.CategoryStruct.comp (restrictInclHom X h) (X.ofRestrict ⋯).toHom = (X.ofRestrict ⋯).toHom

X | V → X | W → X is X | V → X.

instance AnalyticSpace.restrictInclHom_stalkMap_isIso (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) (p : ↑(X.restrict ⋯).toTopCat) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (restrictInclHom X h) p)

The stalk map of the inclusion X | V → X | W is an isomorphism (the two ofRestrict stalk maps are).

def AnalyticSpace.restrictIncl (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) : X.restrict ⋯ ⟶ X.restrict ⋯

The inclusion X | V → X | W of the restrictions to nested opens V ≤ W, as a morphism of locally ringed spaces.

Equations

• AnalyticSpace.restrictIncl X h = { toHom := AnalyticSpace.restrictInclHom X h, prop := ⋯ }

theorem AnalyticSpace.restrictIncl_comp_ofRestrict (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) : CategoryTheory.CategoryStruct.comp (restrictIncl X h) (X.ofRestrict ⋯) = X.ofRestrict ⋯

theorem AnalyticSpace.restrictIncl_base_apply (X : AlgebraicGeometry.LocallyRingedSpace) {V W : TopologicalSpace.Opens ↑X.toTopCat} (h : V ≤ W) (p : ↑(X.restrict ⋯).toTopCat) : (CategoryTheory.ConcreteCategory.hom (restrictIncl X h).base) p = ⟨↑p, ⋯⟩

def AnalyticSpace.GlueCompatible {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) : Prop

The pieces g i : X | Uᵢ → W agree on the overlaps X | (Uᵢ ⊓ Uⱼ).

Equations

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

theorem AnalyticSpace.GlueCompatible.base_apply_eq {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} {U : ι → TopologicalSpace.Opens ↑X.toTopCat} {W : AlgebraicGeometry.LocallyRingedSpace} {g : (i : ι) → X.restrict ⋯ ⟶ W} (hg : GlueCompatible U g) (i j : ι) (x : ↑X.toTopCat) (hi : x ∈ U i) (hj : x ∈ U j) : (CategoryTheory.ConcreteCategory.hom (g i).base) ⟨x, hi⟩ = (CategoryTheory.ConcreteCategory.hom (g j).base) ⟨x, hj⟩

theorem AnalyticSpace.exists_mem_nhds_of_cover {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (x : ↑X.toTopCat) : ∃ (i : ι), ↑(U i) ∈ nhds x

The members of the cover are neighbourhoods of every point.

noncomputable def AnalyticSpace.glueCoverBase {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) : X.toTopCat ⟶ W.toTopCat

The glued base map: x ↦ (g i).base x for any i with x ∈ Uᵢ.

Equations

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

theorem AnalyticSpace.glueCoverBase_apply {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) (p : ↥(U i)) : (CategoryTheory.ConcreteCategory.hom (glueCoverBase U g hU hg)) ↑p = (CategoryTheory.ConcreteCategory.hom (g i).base) p

def AnalyticSpace.gluePieceOpens {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (i : ι) (V : TopologicalSpace.Opens ↑W.toTopCat) : TopologicalSpace.Opens ↑X.toTopCat

The image in X of (g i).base ⁻¹ V ⊆ Uᵢ: the open on which the piece (g i)^* s lives.

Equations

• AnalyticSpace.gluePieceOpens U g i V = ⋯.functor.obj ((TopologicalSpace.Opens.map (g i).base).obj V)

theorem AnalyticSpace.mem_gluePieceOpens {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) {i : ι} {V : TopologicalSpace.Opens ↑W.toTopCat} {x : ↑X.toTopCat} : x ∈ gluePieceOpens U g i V ↔ ∃ (hi : x ∈ U i), (CategoryTheory.ConcreteCategory.hom (g i).base) ⟨x, hi⟩ ∈ V

def AnalyticSpace.gluePieceSection {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (i : ι) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) : ↑(X.presheaf.obj (Opposite.op (gluePieceOpens U g i V)))

The piece (g i)^* s, a section of X over gluePieceOpens i V.

Equations

• AnalyticSpace.gluePieceSection U g i V s = (CategoryTheory.ConcreteCategory.hom ((g i).c.app (Opposite.op V))) s

theorem AnalyticSpace.gluePieceOpens_le {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) (V : TopologicalSpace.Opens ↑W.toTopCat) : gluePieceOpens U g i V ≤ (TopologicalSpace.Opens.map (glueCoverBase U g hU hg)).obj V

theorem AnalyticSpace.le_iSup_gluePieceOpens {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) : (TopologicalSpace.Opens.map (glueCoverBase U g hU hg)).obj V ≤ ⨆ (i : ι), gluePieceOpens U g i V

theorem AnalyticSpace.germ_gluePieceSection_of_overlap {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (i j k : ι) (hk : U i ⊓ U j ≤ U k) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) {x : ↑X.toTopCat} (hi : x ∈ U i) (hj : x ∈ U j) (hV : (CategoryTheory.ConcreteCategory.hom (g k).base) ⟨x, ⋯⟩ ∈ V) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso ⋯ ⟨x, ⋯⟩).hom) ((CategoryTheory.ConcreteCategory.hom ((X.restrict ⋯).presheaf.germ ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (restrictIncl X hk) (g k)).base).obj V) ⟨x, ⋯⟩ hV)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp (restrictIncl X hk) (g k)).c.app (Opposite.op V))) s)) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (gluePieceOpens U g k V) x ⋯)) (gluePieceSection U g k V s)

The germ of a piece at a point, through the overlap space X | (Uᵢ ⊓ Uⱼ): the piece of g k restricted along X | (Uᵢ ⊓ Uⱼ) → X | U_k has the germ of the piece itself.

theorem AnalyticSpace.gluePieceSection_isCompatible {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) : X.presheaf.IsCompatible (fun (i : ι) => gluePieceOpens U g i V) fun (i : ι) => gluePieceSection U g i V s

The pieces (g i)^* s are compatible on the overlaps (their germs agree, through the overlap space, because the pieces agree there).

noncomputable def AnalyticSpace.glueSection {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (glueCoverBase U g hU hg)).obj V)))

The glued section over b⁻¹ V, b the glued base map: the unique section restricting to the piece (g i)^* s on every gluePieceOpens i V.

Equations

• AnalyticSpace.glueSection U g hU hg V s = Exists.choose ⋯

theorem AnalyticSpace.glueSection_res {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) (i : ι) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (glueSection U g hU hg V s) = gluePieceSection U g i V s

theorem AnalyticSpace.eq_glueSection {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) (t : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (glueCoverBase U g hU hg)).obj V)))) (ht : ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) t = gluePieceSection U g i V s) : t = glueSection U g hU hg V s

noncomputable def AnalyticSpace.glueSectionHom {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) : W.presheaf.obj (Opposite.op V) ⟶ X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (glueCoverBase U g hU hg)).obj V))

The glued sections form a ring homomorphism 𝒪_W(V) → 𝒪_X(b⁻¹ V).

Equations

• AnalyticSpace.glueSectionHom U g hU hg V = CommRingCat.ofHom { toFun := AnalyticSpace.glueSection U g hU hg V, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem AnalyticSpace.glueSectionHom_apply {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (V : TopologicalSpace.Opens ↑W.toTopCat) (s : ↑(W.presheaf.obj (Opposite.op V))) : (CommRingCat.Hom.hom (glueSectionHom U g hU hg V)) s = glueSection U g hU hg V s

noncomputable def AnalyticSpace.glueCoverC {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) : W.presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat (glueCoverBase U g hU hg)).obj X.presheaf

The sheaf component of the glued morphism.

Equations

• AnalyticSpace.glueCoverC U g hU hg = { app := fun (V : (TopologicalSpace.Opens ↑↑W.toPresheafedSpace)ᵒᵖ) => AnalyticSpace.glueSectionHom U g hU hg (Opposite.unop V), naturality := ⋯ }

noncomputable def AnalyticSpace.glueHom {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) : X.toPresheafedSpace ⟶ W.toPresheafedSpace

The glued morphism of presheafed spaces.

Equations

• AnalyticSpace.glueHom U g hU hg = { base := AnalyticSpace.glueCoverBase U g hU hg, c := AnalyticSpace.glueCoverC U g hU hg }

theorem AnalyticSpace.glueHom_base_apply {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) (p : ↥(U i)) : (CategoryTheory.ConcreteCategory.hom (glueHom U g hU hg).base) ↑p = (CategoryTheory.ConcreteCategory.hom (g i).base) p

theorem AnalyticSpace.inseparable_glueCoverBase {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) {x : ↑X.toTopCat} (hi : x ∈ U i) : Inseparable ((CategoryTheory.ConcreteCategory.hom (glueCoverBase U g hU hg)) x) ((CategoryTheory.ConcreteCategory.hom (g i).base) ⟨x, hi⟩)

theorem AnalyticSpace.glueHom_stalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) {x : ↑X.toTopCat} (hi : x ∈ U i) : AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (glueHom U g hU hg) x = CategoryTheory.CategoryStruct.comp (W.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (g i) ⟨x, hi⟩) (X.restrictStalkIso ⋯ ⟨x, hi⟩).hom)

The stalk map of the glued morphism at a point of Uᵢ is the stalk map of g i, read through the identification of the image points and the stalk of the open subspace.

theorem AnalyticSpace.isLocalHom_glueHom_stalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (x : ↑X.toTopCat) : IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (glueHom U g hU hg) x))

noncomputable def AnalyticSpace.glueOfCover {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) : X ⟶ W

The morphism of locally ringed spaces glued from compatible pieces g i : X | Uᵢ → W along an open cover of X.

Equations

• AnalyticSpace.glueOfCover U g hU hg = { toHom := AnalyticSpace.glueHom U g hU hg, prop := ⋯ }

theorem AnalyticSpace.glueOfCover_base_apply {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) (p : ↥(U i)) : (CategoryTheory.ConcreteCategory.hom (glueOfCover U g hU hg).base) ↑p = (CategoryTheory.ConcreteCategory.hom (g i).base) p

theorem AnalyticSpace.ofRestrict_comp_glueOfCover {X : AlgebraicGeometry.LocallyRingedSpace} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X.toTopCat) {W : AlgebraicGeometry.LocallyRingedSpace} (g : (i : ι) → X.restrict ⋯ ⟶ W) (hU : ∀ (x : ↑X.toTopCat), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) : CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) (glueOfCover U g hU hg) = g i

The glued morphism restricts to the pieces.

noncomputable def AnalyticSpace.KLocallyRingedSpace.restrictIncl {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {V W : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : V ≤ W) : X.restrictOpen V ⟶ X.restrictOpen W

The inclusion X | V → X | W of the open subspaces of nested opens V ≤ W, as a K-morphism (the factorization of X | V → X through X | W → X).

Equations

• X.restrictIncl h = AnalyticSpace.KLocallyRingedSpace.Hom.ofFac (X.ofRestrict V) (X.ofRestrict W) (AnalyticSpace.restrictIncl X.toLocallyRingedSpace h) ⋯

theorem AnalyticSpace.KLocallyRingedSpace.restrictIncl_comp_ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {V W : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : V ≤ W) : CategoryTheory.CategoryStruct.comp (X.restrictIncl h) (X.ofRestrict W) = X.ofRestrict V

theorem AnalyticSpace.KLocallyRingedSpace.restrictIncl_val {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {V W : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : V ≤ W) : ↑(X.restrictIncl h) = AnalyticSpace.restrictIncl X.toLocallyRingedSpace h

def AnalyticSpace.KLocallyRingedSpace.GlueCompatible {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {W : KLocallyRingedSpace K} (g : (i : ι) → X.restrictOpen (U i) ⟶ W) : Prop

The K-morphisms g i : X | Uᵢ → W agree on the overlaps X | (Uᵢ ⊓ Uⱼ).

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.GlueCompatible.val {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {W : KLocallyRingedSpace K} (g : (i : ι) → X.restrictOpen (U i) ⟶ W) (hg : GlueCompatible U g) : AnalyticSpace.GlueCompatible U fun (i : ι) => ↑(g i)

noncomputable def AnalyticSpace.KLocallyRingedSpace.glueOfCover {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {W : KLocallyRingedSpace K} (g : (i : ι) → X.restrictOpen (U i) ⟶ W) (hU : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) : X ⟶ W

The K-morphism glued from compatible K-morphisms g i : X | Uᵢ → W along an open cover of X: the glued morphism of locally ringed spaces, which respects the K-structures because its global sections restrict to those of the pieces.

Equations

• AnalyticSpace.KLocallyRingedSpace.glueOfCover U g hU hg = ⟨AnalyticSpace.glueOfCover U (fun (i : ι) => ↑(g i)) hU ⋯, ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.ofRestrict_comp_glueOfCover {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {W : KLocallyRingedSpace K} (g : (i : ι) → X.restrictOpen (U i) ⟶ W) (hU : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) : CategoryTheory.CategoryStruct.comp (X.ofRestrict (U i)) (glueOfCover U g hU hg) = g i

theorem AnalyticSpace.KLocallyRingedSpace.glueOfCover_toFun_apply {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {W : KLocallyRingedSpace K} (g : (i : ι) → X.restrictOpen (U i) ⟶ W) (hU : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (i : ι), x ∈ U i) (hg : GlueCompatible U g) (i : ι) (p : ↥(U i)) : Hom.toFun (glueOfCover U g hU hg) ↑p = Hom.toFun (g i) p