# Documentation

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

# 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) extends :
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.

Instances For
@[inline, reducible]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base {C : Type u} (i : D.J) (j : D.J) (k : D.J) (S : Set (CategoryTheory.GlueData.V D.toGlueData (i, j))) :
CategoryTheory.Limits.pullback.snd.base '' (CategoryTheory.Limits.pullback.fst.base ⁻¹' S) = (CategoryTheory.GlueData.f D.toGlueData i k).base ⁻¹' ((CategoryTheory.GlueData.f D.toGlueData i j).base '' S)
theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.V D.toGlueData (i, j))) {Z : C} (h : ((CategoryTheory.GlueData.f D.toGlueData i k).base _* (CategoryTheory.GlueData.V D.toGlueData (i, k)).presheaf).obj (Opposite.op (().obj U)) Z) :
CategoryTheory.CategoryStruct.comp () (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.f D.toGlueData i k).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.GlueData.f D.toGlueData i j))).obj U))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) { carrier := CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop, is_open' := (_ : IsOpen (CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop)) }) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.V D.toGlueData (i, k)).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj { unop := { carrier := CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop, is_open' := (_ : IsOpen (CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.f D.toGlueData i k).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.GlueData.f D.toGlueData i j))).obj U))))) h))
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.V D.toGlueData (i, j))) :
CategoryTheory.CategoryStruct.comp () ((CategoryTheory.GlueData.f D.toGlueData i k).c.app (Opposite.op (().obj U))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) { unop := { carrier := CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop, is_open' := (_ : IsOpen (CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop)) } }.unop) ((CategoryTheory.GlueData.V D.toGlueData (i, k)).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj { unop := { carrier := CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop, is_open' := (_ : IsOpen (CategoryTheory.Limits.pullback.fst.base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.f D.toGlueData i k).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.GlueData.f D.toGlueData i j))).obj U))))))

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f D.toGlueData i j) (CategoryTheory.GlueData.f D.toGlueData i k))) :
∃ (eq : (TopologicalSpace.Opens.map (CategoryTheory.GlueData.t D.toGlueData k i).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U)) = Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst)).obj { unop := { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) } }.unop)), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) U) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.t D.toGlueData k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U))) ((CategoryTheory.GlueData.V D.toGlueData (k, i)).presheaf.map )) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.t' D.toGlueData k i j).c.app ()) (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst) { unop := { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) } }.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} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f D.toGlueData i j) (CategoryTheory.GlueData.f D.toGlueData i k))) {Z : C} (h : ((CategoryTheory.GlueData.t D.toGlueData k i).base _* (CategoryTheory.GlueData.V D.toGlueData (k, i)).presheaf).obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U)) Z) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) U) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.t D.toGlueData k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U))) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.t' D.toGlueData k i j).c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst) { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) }) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.V D.toGlueData (k, i)).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst)).obj { unop := { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.t D.toGlueData k i).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U))))) h))
@[simp]
theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f D.toGlueData i j) (CategoryTheory.GlueData.f D.toGlueData i k))) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) U) ((CategoryTheory.GlueData.t D.toGlueData k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.t' D.toGlueData k i j).c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst) { unop := { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) } }.unop) ((CategoryTheory.GlueData.V D.toGlueData (k, i)).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.fst)).obj { unop := { carrier := (CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.GlueData.t' D.toGlueData k i j).base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.t D.toGlueData k i).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj U))))))

The red and the blue arrows in commute.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq {C : Type u} (i : D.J) (j : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
(TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U) = ().obj ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.t D.toGlueData j i).base).obj ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.f D.toGlueData i j).base).obj U))
def AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap {C : Type u} (i : D.J) (j : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
(CategoryTheory.GlueData.U D.toGlueData i).presheaf.obj () (CategoryTheory.GlueData.U D.toGlueData j).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).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.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
∃ (eq : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj { unop := { carrier := (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.f D.toGlueData j k).base).op.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U)))), CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.f D.toGlueData j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U)))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) { unop := { carrier := (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop)) } }.unop) ((CategoryTheory.GlueData.V D.toGlueData (j, k)).presheaf.map ))
theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app {C : Type u} (i : D.J) (j : D.J) (k : D.J) (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.f D.toGlueData j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U)))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).c.app ()) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd) { unop := { carrier := (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop)) } }.unop) ((CategoryTheory.GlueData.V D.toGlueData (j, k)).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor (_ : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback.snd)).obj { unop := { carrier := (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop, is_open' := (_ : IsOpen ((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j))).base ⁻¹' ().unop)) } }.unop) = (TopologicalSpace.Opens.map (CategoryTheory.GlueData.f D.toGlueData j k).base).op.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.GlueData.ι D.toGlueData j).base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U)))))))

The red and the blue arrows in commute.

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

(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.
Instances For
@[inline, reducible]

(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.
Instances For

(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.
Instances For
def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp {C : Type u} {i : D.J} (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
(CategoryTheory.GlueData.U D.toGlueData i).presheaf.obj ()

(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.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π {C : Type u} {i : D.J} (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
∃ (eq : = Opposite.op ((TopologicalSpace.Opens.map ().base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U))), = (CategoryTheory.GlueData.U D.toGlueData i).presheaf.map

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

@[inline, reducible]
abbrev AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap {C : Type u} {i : D.J} (U : TopologicalSpace.Opens (CategoryTheory.GlueData.U D.toGlueData i)) :
(CategoryTheory.GlueData.U D.toGlueData i).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map ().base).obj ((IsOpenMap.functor (_ : IsOpenMap (CategoryTheory.GlueData.ι D.toGlueData i).base)).obj U))) (CategoryTheory.GlueData.U D.toGlueData i).presheaf.obj ()

The eqToHom given by ιInvApp_π.

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

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

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

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

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.
Instances For
theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective {C : Type u} (x : (CategoryTheory.GlueData.glued D.toGlueData)) :
∃ (i : D.J) (y : (CategoryTheory.GlueData.U D.toGlueData i)), (CategoryTheory.GlueData.ι D.toGlueData i).base y = x
structure AlgebraicGeometry.SheafedSpace.GlueData (C : Type u) extends :
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.

Instances For
@[inline, reducible]

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.
Instances For
@[inline, reducible]

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

Equations
Instances For
Equations
• (_ : ) = (_ : )
theorem AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective {C : Type u} (x : (CategoryTheory.GlueData.glued D.toGlueData).toPresheafedSpace) :
∃ (i : D.J) (y : (CategoryTheory.GlueData.U D.toGlueData i).toPresheafedSpace), (CategoryTheory.GlueData.ι D.toGlueData i).base y = x

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.
Instances For

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.

Instances For
@[inline, reducible]

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.
Instances For
@[inline, reducible]

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

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
theorem AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective (x : ) :
∃ (i : D.J) (y : ()), (CategoryTheory.GlueData.ι D.toGlueData i).val.base y = x

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.
Instances For