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)

theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_open {C : Type u} [CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.PresheafedSpace.GlueData C) (i : self.J) (j : self.J) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (self.f i j)

@[reducible, inline]

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

• D.toTopGlueData = { toGlueData := D.mapGlueData (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 ⇑(D.ι 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 { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U } ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U) (CategoryTheory.CategoryStruct.comp ((D.f i k).c.app { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd ((TopologicalSpace.Opens.map CategoryTheory.Limits.pullback.fst.base).toPrefunctor.1 U)) (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 (D.f i j) U) ((D.f i k).c.app { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U }) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd { unop := (TopologicalSpace.Opens.map CategoryTheory.Limits.pullback.fst.base).toPrefunctor.1 { unop := U }.unop }.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 { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj U } = { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.fst).obj { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑{ unop := U }.unop, is_open' := ⋯ } }.unop }), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj U }) ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq))) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app { unop := U }) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.fst { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑{ unop := 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 { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj U } ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj U }) h) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.fst { carrier := ⇑(D.t' k i j).base ⁻¹' ↑U, 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 CategoryTheory.Limits.pullback.snd U) ((D.t k i).c.app { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj U }) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.fst { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑{ unop := 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 (D.ι j).base).obj (⋯.functor.obj U) = (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f j i)).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 { unop := U } ⟶ (D.U j).presheaf.obj { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.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 : { unop := (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd).obj { unop := (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).toPrefunctor.1 { unop := U }.unop }.unop } = (TopologicalSpace.Opens.map (D.f j k).base).op.obj { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U) }), CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U) ((D.f j k).c.app { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.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 { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd { unop := (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).toPrefunctor.1 { unop := U }.unop }.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 (D.opensImagePreimageMap i j U) ((D.f j k).c.app { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.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 { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd { unop := (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).toPrefunctor.1 { unop := U }.unop }.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 { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U) } ⟶ X') : CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U) (CategoryTheory.CategoryStruct.comp ((D.f j k).c.app { unop := (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.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 { unop := U }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Limits.pullback.snd { unop := (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).toPrefunctor.1 { unop := U }.unop }.unop) (CategoryTheory.CategoryStruct.comp ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) f'))

@[reducible, inline]

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 D.diagram.fstFrom D.diagram.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

• D.diagramOverOpen U = AlgebraicGeometry.PresheafedSpace.componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)

@[reducible, inline]

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 (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj { unop := CategoryTheory.Limits.WalkingMultispan.right j }

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

Equations

• D.diagramOverOpenπ U j = CategoryTheory.Limits.limit.π (D.diagramOverOpen U) { unop := CategoryTheory.Limits.WalkingMultispan.right j }

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 D.diagram.fstFrom D.diagram.sndFrom) : (D.U i).presheaf.obj { unop := U } ⟶ (D.diagramOverOpen U).obj { unop := 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 { unop := U } ⟶ CategoryTheory.Limits.limit (D.diagramOverOpen 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 : { unop := U } = { unop := (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι D.diagram.multispan { unop := CategoryTheory.Limits.WalkingMultispan.right i }.unop).base).obj (⋯.functor.obj U) }), CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U i) = (D.U i).presheaf.map (CategoryTheory.eqToHom eq)

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

@[reducible, inline]

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 { unop := (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι D.diagram.multispan { unop := CategoryTheory.Limits.WalkingMultispan.right i }.unop).base).obj (⋯.functor.obj U) } ⟶ (D.U i).presheaf.obj { unop := U }

The eqToHom given by ιInvApp_π.

Equations

• D.ιInvAppπEqMap 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 (D.diagramOverOpenπ U i) (CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U) (CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U j))) = D.diagramOverOpenπ 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 (D.diagramOverOpenπ U i) (CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U) (D.ιInvApp U)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (D.diagramOverOpen 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 (D.diagramOverOpenπ 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 (D.ι 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 (D.vPullbackCone 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 : ↑↑D.glued) : ∃ (i : D.J) (y : ↑↑(D.U i)), (D.ι 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)

theorem AlgebraicGeometry.SheafedSpace.GlueData.f_open {C : Type u} [CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.SheafedSpace.GlueData C) (i : self.J) (j : self.J) : AlgebraicGeometry.SheafedSpace.IsOpenImmersion (self.f i j)

@[reducible, inline]

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

• D.toPresheafedSpaceGlueData = { toGlueData := D.mapGlueData AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, f_open := ⋯ }

@[reducible, inline]

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

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

Equations

• D.isoPresheafedSpace = D.gluedIso 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 (D.toPresheafedSpaceGlueData.ι i) D.isoPresheafedSpace.inv = D.ι 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 (D.ι 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 : ↑↑D.glued.toPresheafedSpace) : ∃ (i : D.J) (y : ↑↑(D.U i).toPresheafedSpace), (D.ι 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 (D.vPullbackCone 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

• D.vPullbackConeIsLimit i j = D.vPullbackConeIsLimitOfMap AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace i j (D.toPresheafedSpaceGlueData.vPullbackConeIsLimit i j)

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)

theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open (self : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : self.J) (j : self.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (self.f i j)

@[reducible, inline]

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

• D.toSheafedSpaceGlueData = { toGlueData := D.mapGlueData AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, f_open := ⋯ }

@[reducible, inline]

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

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

Equations

• D.isoSheafedSpace = D.gluedIso AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

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

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace (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

• D.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace i j k = inferInstance

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

def AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J) (j : D.J) : CategoryTheory.Limits.IsLimit (D.vPullbackCone 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

• D.vPullbackConeIsLimit i j = D.vPullbackConeIsLimitOfMap AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace i j (D.toSheafedSpaceGlueData.vPullbackConeIsLimit i j)