Gluing Structured spaces

Given a family of gluing data of structured spaces (presheafed spaces, sheafed spaces, or locally ringed spaces), we may glue them together.

The construction should be "sealed" and considered as a black box, while only using the API provided.

Main definitions

• AlgebraicGeometry.PresheafedSpace.GlueData: A structure containing the family of gluing data.
• CategoryTheory.GlueData.glued: The glued presheafed space. This is defined as the multicoequalizer of ∐ V i j ⇉ ∐ U i, so that the general colimit API can be used.
• CategoryTheory.GlueData.ι: The immersion ι i : U i ⟶ glued for each i : J.

Main results

• AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion: The map ι i : U i ⟶ glued is an open immersion for each i : J.
• AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective : The underlying maps of ι i : U i ⟶ glued are jointly surjective.
• AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit : V i j is the pullback (intersection) of U i and U j over the glued space.

Analogous results are also provided for SheafedSpace and LocallyRingedSpace.

Implementation details

Almost the whole file is dedicated to showing tht ι i is an open immersion. The fact that this is an open embedding of topological spaces follows from Mathlib/Topology/Gluing.lean, and it remains to construct Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, ι i '' U) for each U ⊆ U i. Since Γ(𝒪_X, ι i '' U) is the limit of diagram_over_open, the components of the structure sheafs of the spaces in the gluing diagram, we need to construct a map ιInvApp_π_app : Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V) for each V in the gluing diagram.

We will refer to in the following doc strings. The X is the glued space, and the dotted arrow is a partial inverse guaranteed by the fact that it is an open immersion. The map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, _) is given by the composition of the red arrows, and the map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{V_{jk}}, _) is given by the composition of the blue arrows. To lift this into a map from Γ(𝒪_X, ι i '' U), we also need to show that these commute with the maps in the diagram (the green arrows), which is just a lengthy diagram-chasing.

structure AlgebraicGeometry.PresheafedSpace.GlueData (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.GlueData : Type (max u (v + 1))

A family of gluing data consists of

1. An index type J
2. A presheafed space U i for each i : J.
3. A presheafed space V i j for each i j : J. (Note that this is J × J → PresheafedSpace C rather than J → J → PresheafedSpace C to connect to the limits library easier.)
4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
6. f i i is an isomorphism.
7. t i i is the identity.
8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

• J : Type v
• U : self.J → AlgebraicGeometry.PresheafedSpace C
• V : self.J × self.J → AlgebraicGeometry.PresheafedSpace C
• f : (i j : self.J) → self.V (i, j) ⟶ self.U i
• f_mono : ∀ (i j : self.J), CategoryTheory.Mono (self.f i j)
• f_hasPullback : ∀ (i j k : self.J), CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
• f_id : ∀ (i : self.J), CategoryTheory.IsIso (self.f i i)
• t : (i j : self.J) → self.V (i, j) ⟶ self.V (j, i)
• t_id : ∀ (i : self.J), self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
• t' : (i j k : self.J) → CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
• t_fac : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.t i j)
• cocycle : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
• f_open : ∀ (i j : self.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (self.f i j)

@[inline, reducible]

abbrev AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) : TopCat.GlueData

The glue data of topological spaces associated to a family of glue data of PresheafedSpaces.

Equations

• AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData D = { toGlueData := CategoryTheory.GlueData.mapGlueData D.toGlueData (AlgebraicGeometry.PresheafedSpace.forget C), f_open := ⋯ }

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : OpenEmbedding ⇑(CategoryTheory.GlueData.ι D.toGlueData i).base

theorem AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (S : Set ↑↑(D.V (i, j))) : ⇑CategoryTheory.Limits.pullback.snd.base '' (⇑CategoryTheory.Limits.pullback.fst.base ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)

theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))) {Z : C} (h : ((D.f i k).base _* (D.V (i, k)).presheaf).obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) (CategoryTheory.CategoryStruct.comp ((D.f i k).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { carrier := ⇑CategoryTheory.Limits.pullback.fst.base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ }) (CategoryTheory.CategoryStruct.comp ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) ((D.f i k).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑CategoryTheory.Limits.pullback.fst.base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))) : ∃ (eq : (TopologicalSpace.Opens.map (D.t k i).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U)) = Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop)), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U))) ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq))) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U)) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop)

We can prove the eq along with the lemma. Thus this is bundled together here, and the lemma itself is separated below.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))) {Z : C} (h : ((D.t k i).base _* (D.V (k, i)).presheaf).obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U))) h) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ }) (CategoryTheory.CategoryStruct.comp ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ U) ((D.t k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj U))) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)))

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : (TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U) = (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj ((TopologicalSpace.Opens.map (D.t j i).base).obj ((TopologicalSpace.Opens.map (D.f i j).base).obj U))

def AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : (D.U i).presheaf.obj (Opposite.op U) ⟶ (D.U j).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U)))

(Implementation). The map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' (𝖣.ι i '' U))

Equations

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : ∃ (eq : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor ⋯).obj { unop := { carrier := ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) = (TopologicalSpace.Opens.map (D.f j k).base).op.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U)))), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap D i j U) ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U)))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom eq)))

theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap D i j U) ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U)))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) {X' : C} (f' : ((D.f j k).base _* (D.V (j, k)).presheaf).obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U))) ⟶ X') : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap D i j U) (CategoryTheory.CategoryStruct.comp ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor ⋯).obj U)))) f') = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp ⋯ { unop := { carrier := ⇑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop) (CategoryTheory.CategoryStruct.comp ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) f'))

@[inline, reducible]

abbrev AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.GlueData.diagram D.toGlueData).fstFrom (CategoryTheory.GlueData.diagram D.toGlueData).sndFrom)ᵒᵖ C

(Implementation) Given an open subset of one of the spaces U ⊆ Uᵢ, the sheaf component of the image ι '' U in the glued space is the limit of this diagram.

Equations

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

@[inline, reducible]

abbrev AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) (j : D.J) : CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen D U) ⟶ (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen D U).obj (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right j))

(Implementation) The projection from the limit of diagram_over_open to a component of D.U j.

Equations

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

def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) (j : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.GlueData.diagram D.toGlueData).fstFrom (CategoryTheory.GlueData.diagram D.toGlueData).sndFrom) : (D.U i).presheaf.obj (Opposite.op U) ⟶ (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen D U).obj (Opposite.op j)

(Implementation) We construct the map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V) for each V in the gluing diagram. We will lift these maps into ιInvApp.

Equations

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

def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) : (D.U i).presheaf.obj (Opposite.op U) ⟶ CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen D U)

(Implementation) The natural map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, 𝖣.ι i '' U). This forms the inverse of (𝖣.ι i).c.app (op U).

Equations

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) : ∃ (eq : Opposite.op U = Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D.toGlueData)) (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)).unop).base).obj ((IsOpenMap.functor ⋯).obj U))), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp D U) (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U i) = (D.U i).presheaf.map (CategoryTheory.eqToHom eq)

ιInvApp is the left inverse of D.ι i on U.

@[inline, reducible]

abbrev AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) : (D.U i).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D.toGlueData)) (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)).unop).base).obj ((IsOpenMap.functor ⋯).obj U))) ⟶ (D.U i).presheaf.obj (Opposite.op U)

The eqToHom given by ιInvApp_π.

Equations

• AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap D U = (D.U i).presheaf.map (CategoryTheory.eqToIso ⋯).inv

theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap D U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp D U) (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U j))) = AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U j

ιInvApp is the right inverse of D.ι i on U.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap D U) (AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp D U)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen D U))

ιInvApp is the inverse of D.ι i on U.

instance AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ D U i)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.GlueData.ι D.toGlueData i)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) : CategoryTheory.Limits.IsLimit (CategoryTheory.GlueData.vPullbackCone D.toGlueData i j)

The following diagram is a pullback, i.e. Vᵢⱼ is the intersection of Uᵢ and Uⱼ in X.

Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X

Equations

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (x : ↑↑(CategoryTheory.GlueData.glued D.toGlueData)) : ∃ (i : D.J) (y : ↑↑(D.U i)), (CategoryTheory.GlueData.ι D.toGlueData i).base y = x

structure AlgebraicGeometry.SheafedSpace.GlueData (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.GlueData : Type (max u (v + 1))

A family of gluing data consists of

1. An index type J
2. A sheafed space U i for each i : J.
3. A sheafed space V i j for each i j : J. (Note that this is J × J → SheafedSpace C rather than J → J → SheafedSpace C to connect to the limits library easier.)
4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
6. f i i is an isomorphism.
7. t i i is the identity.
8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

• J : Type v
• U : self.J → AlgebraicGeometry.SheafedSpace C
• V : self.J × self.J → AlgebraicGeometry.SheafedSpace C
• f : (i j : self.J) → self.V (i, j) ⟶ self.U i
• f_mono : ∀ (i j : self.J), CategoryTheory.Mono (self.f i j)
• f_hasPullback : ∀ (i j k : self.J), CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
• f_id : ∀ (i : self.J), CategoryTheory.IsIso (self.f i i)
• t : (i j : self.J) → self.V (i, j) ⟶ self.V (j, i)
• t_id : ∀ (i : self.J), self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
• t' : (i j k : self.J) → CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
• t_fac : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.t i j)
• cocycle : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
• f_open : ∀ (i j : self.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (self.f i j)

@[inline, reducible]

abbrev AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) : AlgebraicGeometry.PresheafedSpace.GlueData C

The glue data of presheafed spaces associated to a family of glue data of sheafed spaces.

Equations

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

@[inline, reducible]

abbrev AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] : (CategoryTheory.GlueData.glued D.toGlueData).toPresheafedSpace ≅ CategoryTheory.GlueData.glued (AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData D).toGlueData

The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.

Equations

• AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace D = CategoryTheory.GlueData.gluedIso D.toGlueData AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace

theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.ι (AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData D).toGlueData i) (AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace D).inv = CategoryTheory.GlueData.ι D.toGlueData i

instance AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.GlueData.ι D.toGlueData i)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (x : ↑↑(CategoryTheory.GlueData.glued D.toGlueData).toPresheafedSpace) : ∃ (i : D.J) (y : ↑↑(D.U i).toPresheafedSpace), (CategoryTheory.GlueData.ι D.toGlueData i).base y = x

def AlgebraicGeometry.SheafedSpace.GlueData.vPullbackConeIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (j : D.J) : CategoryTheory.Limits.IsLimit (CategoryTheory.GlueData.vPullbackCone D.toGlueData i j)

The following diagram is a pullback, i.e. Vᵢⱼ is the intersection of Uᵢ and Uⱼ in X.

Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X

Equations

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

structure AlgebraicGeometry.LocallyRingedSpace.GlueDataextends CategoryTheory.GlueData : Type (u_1 + 1)

A family of gluing data consists of

1. An index type J
2. A locally ringed space U i for each i : J.
3. A locally ringed space V i j for each i j : J. (Note that this is J × J → LocallyRingedSpace rather than J → J → LocallyRingedSpace to connect to the limits library easier.)
4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
6. f i i is an isomorphism.
7. t i i is the identity.
8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

• J : Type u_1
• U : self.J → AlgebraicGeometry.LocallyRingedSpace
• V : self.J × self.J → AlgebraicGeometry.LocallyRingedSpace
• f : (i j : self.J) → self.V (i, j) ⟶ self.U i
• f_mono : ∀ (i j : self.J), CategoryTheory.Mono (self.f i j)
• f_hasPullback : ∀ (i j k : self.J), CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
• f_id : ∀ (i : self.J), CategoryTheory.IsIso (self.f i i)
• t : (i j : self.J) → self.V (i, j) ⟶ self.V (j, i)
• t_id : ∀ (i : self.J), self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
• t' : (i j k : self.J) → CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
• t_fac : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.t i j)
• cocycle : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
• f_open : ∀ (i j : self.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (self.f i j)

@[inline, reducible]

abbrev AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) : AlgebraicGeometry.SheafedSpace.GlueData CommRingCat

The glue data of ringed spaces associated to a family of glue data of locally ringed spaces.

Equations

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

@[inline, reducible]

abbrev AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) : (CategoryTheory.GlueData.glued D.toGlueData).toSheafedSpace ≅ CategoryTheory.GlueData.glued (AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData D).toGlueData

The gluing as locally ringed spaces is isomorphic to the gluing as ringed spaces.

Equations

• AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace D = CategoryTheory.GlueData.gluedIso D.toGlueData AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.ι (AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData D).toGlueData i) (AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace D).inv = (CategoryTheory.GlueData.ι D.toGlueData i).val

instance AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.GlueData.ι D.toGlueData i)

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitLocallyRingedSpaceInstCategoryLocallyRingedSpaceSheafedSpaceCommRingCatInstCommRingCatLargeCategoryInstCategorySheafedSpaceWalkingCospanCategoryWalkingPairCospanVToGlueDataMkJUFForgetToSheafedSpace (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) (j : D.J) (k : D.J) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

Equations

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

theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (CategoryTheory.GlueData.glued D.toGlueData))) : ∃ (i : D.J) (y : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat (D.U i))), (CategoryTheory.GlueData.ι D.toGlueData i).val.base y = x

def AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) (j : D.J) : CategoryTheory.Limits.IsLimit (CategoryTheory.GlueData.vPullbackCone D.toGlueData i j)

The following diagram is a pullback, i.e. Vᵢⱼ is the intersection of Uᵢ and Uⱼ in X.

Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X

Equations

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