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 that ι 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 (AlgebraicGeometry.PresheafedSpace C) : 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) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : 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 = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : IsOpenImmersion (self.f i j)

@[reducible, inline]

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

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i).base)

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

@[simp]

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

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))) {Z : C} (h : ((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj (Opposite.op ((IsOpenImmersion.opensFunctor (D.f i j)).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (D.f i j) U) (CategoryTheory.CategoryStruct.comp ((D.f i k).c.app (Opposite.op ((IsOpenImmersion.opensFunctor (D.f i j)).obj U))) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).1 U)) (CategoryTheory.CategoryStruct.comp ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) (i 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 ((IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U)) = Opposite.op ((IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j))).obj (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (D.t' k i j).base).1 (Opposite.unop (Opposite.op U))))))), CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app (Opposite.op ((IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U))) ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq))) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U)) (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (D.t' k i j).base).1 (Opposite.unop (Opposite.op U))))))

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

@[simp]

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

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))) {Z : C} (h : ((TopCat.Presheaf.pushforward C (D.t k i).base).obj (D.V (k, i)).presheaf).obj (Opposite.op ((IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) U) (CategoryTheory.CategoryStruct.comp ((D.t k i).c.app (Opposite.op ((IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U))) h) = CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j)) ((TopologicalSpace.Opens.map (D.t' k i j).base).1 U)) (CategoryTheory.CategoryStruct.comp ((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)) h))

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U) = (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 : GlueData C) [CategoryTheory.Limits.HasLimits C] (i 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 (D.ι j).base).obj (⋯.functor.obj U)))

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

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U) ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k)) (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k)) (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1 (Opposite.unop (Opposite.op U)))))) ((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 : GlueData C) [CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) {X' : C} (f' : ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj (Opposite.op ((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 (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) f') = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k)) (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k)) (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1 (Opposite.unop (Opposite.op U)))))) (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 : GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J))ᵒᵖ 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.

@[reducible, inline]

abbrev AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ {C : Type u} [CategoryTheory.Category.{v, u} C] (D : 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 (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right j))

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

def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)) (j : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J)) : (D.U i).presheaf.obj (Opposite.op U) ⟶ (D.diagramOverOpen 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.

def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp {C : Type u} [CategoryTheory.Category.{v, u} C] (D : 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 (D.diagramOverOpen U)

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

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π {C : Type u} [CategoryTheory.Category.{v, u} C] (D : 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.ι D.diagram.multispan (Opposite.unop (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)))).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 : 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.ι D.diagram.multispan (Opposite.unop (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))) ⟶ (D.U i).presheaf.obj (Opposite.op U)

The eqToHom given by ιInvApp_π.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i 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 : 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 : GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) : CategoryTheory.IsIso (D.diagramOverOpenπ U i)

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

def AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i 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

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

structure AlgebraicGeometry.SheafedSpace.GlueData (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C) : 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) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : 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 = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : IsOpenImmersion (self.f i j)

@[reducible, inline]

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

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

@[reducible, inline]

abbrev AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace {C : Type u} [CategoryTheory.Category.{v, u} C] (D : 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.

theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (D : 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 : GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : IsOpenImmersion (D.ι i)

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

def AlgebraicGeometry.SheafedSpace.GlueData.vPullbackConeIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasLimits C] (i 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

structure AlgebraicGeometry.LocallyRingedSpace.GlueDataextends CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace : 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) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : 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 = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : IsOpenImmersion (self.f i j)

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

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

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

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

def AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit (D : GlueData) (i 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