mathlib documentation

algebraic_geometry.presheafed_space.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 #

algebraic_geometry.PresheafedSpace.glue_data: A structure containing the family of gluing data.
category_theory.glue_data.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.
category_theory.glue_data.ι: The immersion ι i : U i ⟶ glued for each i : J.

Main results #

algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion: The map ι i : U i ⟶ glued is an open immersion for each i : J.
algebraic_geometry.PresheafedSpace.glue_data.ι_jointly_surjective : The underlying maps of ι i : U i ⟶ glued are jointly surjective.
algebraic_geometry.PresheafedSpace.glue_data.V_pullback_cone_is_limit : 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 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 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 ι_inv_app_π_app : Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V) for each V in the gluing diagram.

We will refer to this diagram 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.

@[nolint]

structure algebraic_geometry.PresheafedSpace.glue_data (C : Type u) [category_theory.category C] :

Type (max u (v+1))

to_glue_data : category_theory.glue_data (algebraic_geometry.PresheafedSpace C)
f_open : ∀ (i j : self.to_glue_data.J), algebraic_geometry.PresheafedSpace.is_open_immersion (self.to_glue_data.f i j)

A family of gluing data consists of

An index type J
A presheafed space U i for each i : J.
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.)
An open immersion f i j : V i j ⟶ U i for each i j : ι.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
f i i is an isomorphism.
t i i is the identity.
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.
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 algebraic_geometry.PresheafedSpace.glue_data

algebraic_geometry.PresheafedSpace.glue_data.has_sizeof_inst

@[reducible]

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.to_Top_glue_data {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) :

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

theorem algebraic_geometry.PresheafedSpace.glue_data.ι_open_embedding {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) :

open_embedding ⇑((D.to_glue_data.ι i).base)

theorem algebraic_geometry.PresheafedSpace.glue_data.pullback_base {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (S : set ↥((D.to_glue_data.V (i, j)).carrier)) :

⇑category_theory.limits.pullback.snd '' (⇑category_theory.limits.pullback.fst ⁻¹' S) = ⇑(D.to_glue_data.f i k) ⁻¹' (⇑(D.to_glue_data.f i j) '' S)

@[simp]

theorem algebraic_geometry.PresheafedSpace.glue_data.f_inv_app_f_app {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.V (i, j)).carrier)) :

_.inv_app U ≫ (D.to_glue_data.f i k).c.app (opposite.op (_.open_functor.obj U)) = category_theory.limits.pullback.fst.c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map category_theory.limits.pullback.fst.base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (i, k)).presheaf.map (category_theory.eq_to_hom _)

The red and the blue arrows in this diagram commute.

@[simp]

theorem algebraic_geometry.PresheafedSpace.glue_data.f_inv_app_f_app_assoc {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.V (i, j)).carrier)) {X' : C} (f' : ((D.to_glue_data.f i k).base _* (D.to_glue_data.V (i, k)).presheaf).obj (opposite.op (_.open_functor.obj U)) ⟶ X') :

_.inv_app U ≫ (D.to_glue_data.f i k).c.app (opposite.op (_.open_functor.obj U)) ≫ f' = category_theory.limits.pullback.fst.c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map category_theory.limits.pullback.fst.base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (i, k)).presheaf.map (category_theory.eq_to_hom _) ≫ f'

theorem algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app' {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((category_theory.limits.pullback (D.to_glue_data.f i j) (D.to_glue_data.f i k)).carrier)) :

∃ (eq_1 : (topological_space.opens.map (D.to_glue_data.t k i).base).op.obj (opposite.op (_.open_functor.obj U)) = opposite.op (_.open_functor.obj (opposite.unop ((topological_space.opens.map (D.to_glue_data.t' k i j).base).op.obj (opposite.op U))))), _.inv_app U ≫ (D.to_glue_data.t k i).c.app (opposite.op (_.open_functor.obj U)) ≫ (D.to_glue_data.V (k, i)).presheaf.map (category_theory.eq_to_hom eq_1) = (D.to_glue_data.t' k i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (D.to_glue_data.t' k i j).base).op.obj (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 algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app_assoc {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((category_theory.limits.pullback (D.to_glue_data.f i j) (D.to_glue_data.f i k)).carrier)) {X' : C} (f' : ((D.to_glue_data.t k i).base _* (D.to_glue_data.V (k, i)).presheaf).obj (opposite.op (_.open_functor.obj U)) ⟶ X') :

_.inv_app U ≫ (D.to_glue_data.t k i).c.app (opposite.op (_.open_functor.obj U)) ≫ f' = (D.to_glue_data.t' k i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (D.to_glue_data.t' k i j).base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (k, i)).presheaf.map (category_theory.eq_to_hom _) ≫ f'

@[simp]

theorem algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((category_theory.limits.pullback (D.to_glue_data.f i j) (D.to_glue_data.f i k)).carrier)) :

_.inv_app U ≫ (D.to_glue_data.t k i).c.app (opposite.op (_.open_functor.obj U)) = (D.to_glue_data.t' k i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (D.to_glue_data.t' k i j).base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (k, i)).presheaf.map (category_theory.eq_to_hom _)

The red and the blue arrows in this diagram commute.

theorem algebraic_geometry.PresheafedSpace.glue_data.ι_image_preimage_eq {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

(topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U) = _.open_functor.obj ((topological_space.opens.map (D.to_glue_data.t j i).base).obj ((topological_space.opens.map (D.to_glue_data.f i j).base).obj U))

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

(D.to_glue_data.U i).presheaf.obj (opposite.op U) ⟶ (D.to_glue_data.U j).presheaf.obj (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U)))

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

Equations

D.opens_image_preimage_map i j U = (D.to_glue_data.f i j).c.app (opposite.op U) ≫ (D.to_glue_data.t j i).c.app ((topological_space.opens.map (D.to_glue_data.f i j).base).op.obj (opposite.op U)) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (D.to_glue_data.t j i).base).op.obj ((topological_space.opens.map (D.to_glue_data.f i j).base).op.obj (opposite.op U)))) ≫ (D.to_glue_data.U j).presheaf.map (category_theory.eq_to_hom _).op

theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app' {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

∃ (eq_1 : opposite.op (_.open_functor.obj (opposite.unop ((topological_space.opens.map (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).base).op.obj (opposite.op U)))) = (topological_space.opens.map (D.to_glue_data.f j k).base).op.obj (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U)))), D.opens_image_preimage_map i j U ≫ (D.to_glue_data.f j k).c.app (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U))) = (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (j, k)).presheaf.map (category_theory.eq_to_hom eq_1)

theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

D.opens_image_preimage_map i j U ≫ (D.to_glue_data.f j k).c.app (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U))) = (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (j, k)).presheaf.map (category_theory.eq_to_hom _)

The red and the blue arrows in this diagram commute.

theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app_assoc {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j k : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) {X' : C} (f' : ((D.to_glue_data.f j k).base _* (D.to_glue_data.V (j, k)).presheaf).obj (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U))) ⟶ X') :

D.opens_image_preimage_map i j U ≫ (D.to_glue_data.f j k).c.app (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U))) ≫ f' = (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).c.app (opposite.op U) ≫ _.inv_app (opposite.unop ((topological_space.opens.map (category_theory.limits.pullback.fst ≫ D.to_glue_data.t j i ≫ D.to_glue_data.f i j).base).op.obj (opposite.op U))) ≫ (D.to_glue_data.V (j, k)).presheaf.map (category_theory.eq_to_hom _) ≫ f'

@[reducible]

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

(category_theory.limits.walking_multispan D.to_glue_data.diagram.fst_from D.to_glue_data.diagram.snd_from)ᵒᵖ ⥤ 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]

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open_π {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) (j : D.to_glue_data.J) :

category_theory.limits.limit (D.diagram_over_open U) ⟶ (D.diagram_over_open U).obj (opposite.op (category_theory.limits.walking_multispan.right j))

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

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_app {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) (j : category_theory.limits.walking_multispan D.to_glue_data.diagram.fst_from D.to_glue_data.diagram.snd_from) :

(D.to_glue_data.U i).presheaf.obj (opposite.op U) ⟶ (D.diagram_over_open 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 ι_inv_app.

Equations

D.ι_inv_app_π_app U j = j.cases_on (λ (j : D.to_glue_data.diagram.L), prod.cases_on j (λ (j k : D.to_glue_data.J), D.opens_image_preimage_map i j U ≫ (D.to_glue_data.f j k).c.app (opposite.op ((topological_space.opens.map (D.to_glue_data.ι j).base).obj (_.functor.obj U))) ≫ (D.to_glue_data.V (j, k)).presheaf.map (category_theory.eq_to_hom _))) (λ (j : D.to_glue_data.diagram.R), D.opens_image_preimage_map i j U)

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

(D.to_glue_data.U i).presheaf.obj (opposite.op U) ⟶ category_theory.limits.limit (D.diagram_over_open U)

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

Equations

D.ι_inv_app U = category_theory.limits.limit.lift (D.diagram_over_open U) {X := (D.to_glue_data.U i).presheaf.obj (opposite.op U), π := {app := λ (j : (category_theory.limits.walking_multispan D.to_glue_data.diagram.fst_from D.to_glue_data.diagram.snd_from)ᵒᵖ), D.ι_inv_app_π_app U (opposite.unop j), naturality' := _}}

theorem algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

∃ (eq_1 : opposite.op U = opposite.op ((topological_space.opens.map (category_theory.limits.colimit.ι D.to_glue_data.diagram.multispan (opposite.unop (opposite.op (category_theory.limits.walking_multispan.right i)))).base).obj (_.functor.obj U))), D.ι_inv_app U ≫ D.diagram_over_open_π U i = (D.to_glue_data.U i).presheaf.map (category_theory.eq_to_hom eq_1)

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

@[reducible]

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_eq_map {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] {i : D.to_glue_data.J} (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

(D.to_glue_data.U i).presheaf.obj (opposite.op ((topological_space.opens.map (category_theory.limits.colimit.ι D.to_glue_data.diagram.multispan (opposite.unop (opposite.op (category_theory.limits.walking_multispan.right i)))).base).obj (_.functor.obj U))) ⟶ (D.to_glue_data.U i).presheaf.obj (opposite.op U)

The eq_to_hom given by ι_inv_app_π.

theorem algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_π {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

D.diagram_over_open_π U i ≫ D.ι_inv_app_π_eq_map U ≫ D.ι_inv_app U ≫ D.diagram_over_open_π U j = D.diagram_over_open_π U j

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

theorem algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_eq_id {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

D.diagram_over_open_π U i ≫ D.ι_inv_app_π_eq_map U ≫ D.ι_inv_app U = 𝟙 (category_theory.limits.limit (D.diagram_over_open U))

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

@[protected, instance]

def algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) (U : topological_space.opens ↥((D.to_glue_data.U i).carrier)) :

category_theory.is_iso (D.diagram_over_open_π U i)

@[protected, instance]

def algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) :

algebraic_geometry.PresheafedSpace.is_open_immersion (D.to_glue_data.ι i)

noncomputable def algebraic_geometry.PresheafedSpace.glue_data.V_pullback_cone_is_limit {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j : D.to_glue_data.J) :

category_theory.limits.is_limit (D.to_glue_data.V_pullback_cone 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.V_pullback_cone_is_limit i j = (D.to_glue_data.V_pullback_cone i j).is_limit_aux' (λ (s : category_theory.limits.pullback_cone (D.to_glue_data.ι i) (D.to_glue_data.ι j)), ⟨algebraic_geometry.PresheafedSpace.is_open_immersion.lift (D.to_glue_data.f i j) s.fst _, _⟩)

theorem algebraic_geometry.PresheafedSpace.glue_data.ι_jointly_surjective {C : Type u} [category_theory.category C] (D : algebraic_geometry.PresheafedSpace.glue_data C) [category_theory.limits.has_limits C] (x : ↥(D.to_glue_data.glued)) :

∃ (i : D.to_glue_data.J) (y : ↥(D.to_glue_data.U i)), ⇑((D.to_glue_data.ι i).base) y = x

@[nolint]

structure algebraic_geometry.SheafedSpace.glue_data (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] :

Type (max u (v+1))

to_glue_data : category_theory.glue_data (algebraic_geometry.SheafedSpace C)
f_open : ∀ (i j : self.to_glue_data.J), algebraic_geometry.SheafedSpace.is_open_immersion (self.to_glue_data.f i j)

A family of gluing data consists of

An index type J
A sheafed space U i for each i : J.
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.)
An open immersion f i j : V i j ⟶ U i for each i j : ι.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
f i i is an isomorphism.
t i i is the identity.
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.
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 algebraic_geometry.SheafedSpace.glue_data

algebraic_geometry.SheafedSpace.glue_data.has_sizeof_inst

@[reducible]

noncomputable def algebraic_geometry.SheafedSpace.glue_data.to_PresheafedSpace_glue_data {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) :

algebraic_geometry.PresheafedSpace.glue_data C

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

@[reducible]

noncomputable def algebraic_geometry.SheafedSpace.glue_data.iso_PresheafedSpace {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) [category_theory.limits.has_limits C] :

D.to_glue_data.glued.to_PresheafedSpace ≅ D.to_PresheafedSpace_glue_data.to_glue_data.glued

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

theorem algebraic_geometry.SheafedSpace.glue_data.ι_iso_PresheafedSpace_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) :

D.to_PresheafedSpace_glue_data.to_glue_data.ι i ≫ D.iso_PresheafedSpace.inv = D.to_glue_data.ι i

@[protected, instance]

def algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i : D.to_glue_data.J) :

algebraic_geometry.SheafedSpace.is_open_immersion (D.to_glue_data.ι i)

theorem algebraic_geometry.SheafedSpace.glue_data.ι_jointly_surjective {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) [category_theory.limits.has_limits C] (x : ↥(D.to_glue_data.glued)) :

∃ (i : D.to_glue_data.J) (y : ↥(D.to_glue_data.U i)), ⇑((D.to_glue_data.ι i).base) y = x

noncomputable def algebraic_geometry.SheafedSpace.glue_data.V_pullback_cone_is_limit {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (D : algebraic_geometry.SheafedSpace.glue_data C) [category_theory.limits.has_limits C] (i j : D.to_glue_data.J) :

category_theory.limits.is_limit (D.to_glue_data.V_pullback_cone 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.V_pullback_cone_is_limit i j = D.to_glue_data.V_pullback_cone_is_limit_of_map algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace i j (D.to_PresheafedSpace_glue_data.V_pullback_cone_is_limit i j)

@[nolint]

structure algebraic_geometry.LocallyRingedSpace.glue_data :

Type (u_1+1)

to_glue_data : category_theory.glue_data algebraic_geometry.LocallyRingedSpace
f_open : ∀ (i j : self.to_glue_data.J), algebraic_geometry.LocallyRingedSpace.is_open_immersion (self.to_glue_data.f i j)

A family of gluing data consists of

An index type J
A locally ringed space U i for each i : J.
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.)
An open immersion f i j : V i j ⟶ U i for each i j : ι.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
f i i is an isomorphism.
t i i is the identity.
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.
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 algebraic_geometry.LocallyRingedSpace.glue_data

algebraic_geometry.LocallyRingedSpace.glue_data.has_sizeof_inst

@[reducible]

noncomputable def algebraic_geometry.LocallyRingedSpace.glue_data.to_SheafedSpace_glue_data (D : algebraic_geometry.LocallyRingedSpace.glue_data) :

algebraic_geometry.SheafedSpace.glue_data CommRing

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

@[reducible]

noncomputable def algebraic_geometry.LocallyRingedSpace.glue_data.iso_SheafedSpace (D : algebraic_geometry.LocallyRingedSpace.glue_data) :

D.to_glue_data.glued.to_SheafedSpace ≅ D.to_SheafedSpace_glue_data.to_glue_data.glued

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

theorem algebraic_geometry.LocallyRingedSpace.glue_data.ι_iso_SheafedSpace_inv (D : algebraic_geometry.LocallyRingedSpace.glue_data) (i : D.to_glue_data.J) :

D.to_SheafedSpace_glue_data.to_glue_data.ι i ≫ D.iso_SheafedSpace.inv = (D.to_glue_data.ι i).val

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion (D : algebraic_geometry.LocallyRingedSpace.glue_data) (i : D.to_glue_data.J) :

algebraic_geometry.LocallyRingedSpace.is_open_immersion (D.to_glue_data.ι i)

@[protected, instance]

noncomputable def algebraic_geometry.LocallyRingedSpace.glue_data.algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_limit (D : algebraic_geometry.LocallyRingedSpace.glue_data) (i j k : D.to_glue_data.J) :

category_theory.limits.preserves_limit (category_theory.limits.cospan (D.to_glue_data.f i j) (D.to_glue_data.f i k)) algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

Equations

algebraic_geometry.LocallyRingedSpace.glue_data.algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_limit D i j k = infer_instance

theorem algebraic_geometry.LocallyRingedSpace.glue_data.ι_jointly_surjective (D : algebraic_geometry.LocallyRingedSpace.glue_data) (x : ↥(D.to_glue_data.glued)) :

∃ (i : D.to_glue_data.J) (y : ↥(D.to_glue_data.U i)), ⇑((D.to_glue_data.ι i).val.base) y = x

noncomputable def algebraic_geometry.LocallyRingedSpace.glue_data.V_pullback_cone_is_limit (D : algebraic_geometry.LocallyRingedSpace.glue_data) (i j : D.to_glue_data.J) :

category_theory.limits.is_limit (D.to_glue_data.V_pullback_cone 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.V_pullback_cone_is_limit i j = D.to_glue_data.V_pullback_cone_is_limit_of_map algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace i j (D.to_SheafedSpace_glue_data.V_pullback_cone_is_limit i j)