Gluing Schemes #
Given a family of gluing data of schemes, we may glue them together.
Main definitions #
algebraic_geometry.Scheme.glue_data
: A structure containing the family of gluing data.algebraic_geometry.Scheme.glue_data.glued
: The glued scheme. This is defined as the multicoequalizer of∐ V i j ⇉ ∐ U i
, so that the general colimit API can be used.algebraic_geometry.Scheme.glue_data.ι
: The immersionι i : U i ⟶ glued
for eachi : J
.algebraic_geometry.Scheme.glue_data.iso_carrier
: The isomorphism between the underlying space of the glued scheme and the gluing of the underlying topological spaces.algebraic_geometry.Scheme.open_cover.glue_data
: The glue data associated with an open cover.algebraic_geometry.Scheme.open_cover.from_glue_data
: The canonical morphism𝒰.glue_data.glued ⟶ X
. This has anis_iso
instance.algebraic_geometry.Scheme.open_cover.glue_morphisms
: We may glue a family of compatible morphisms defined on an open cover of a scheme.
Main results #
algebraic_geometry.Scheme.glue_data.ι_is_open_immersion
: The mapι i : U i ⟶ glued
is an open immersion for eachi : J
.algebraic_geometry.Scheme.glue_data.ι_jointly_surjective
: The underlying maps ofι i : U i ⟶ glued
are jointly surjective.algebraic_geometry.Scheme.glue_data.V_pullback_cone_is_limit
:V i j
is the pullback (intersection) ofU i
andU j
over the glued space.algebraic_geometry.Scheme.glue_data.ι_eq_iff_rel
:ι i x = ι j y
if and only if they coincide when restricted toV i i
.algebraic_geometry.Scheme.glue_data.is_open_iff
: An subset of the glued scheme is open iff all its preimages inU i
are open.
Implementation details #
All the hard work is done in algebraic_geometry/presheafed_space/gluing.lean
where we glue
presheafed spaces, sheafed spaces, and locally ringed spaces.
- to_glue_data : category_theory.glue_data algebraic_geometry.Scheme
- f_open : ∀ (i j : self.to_glue_data.J), algebraic_geometry.is_open_immersion (self.to_glue_data.f i j)
A family of gluing data consists of
- An index type
J
- An scheme
U i
for eachi : J
. - An scheme
V i j
for eachi j : J
. (Note that this isJ × J → Scheme
rather thanJ → J → Scheme
to connect to the limits library easier.) - An open immersion
f i j : V i j ⟶ U i
for eachi j : ι
. - A transition map
t i j : V i j ⟶ V j i
for eachi 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 throughV j k ×[U j] V j i ⟶ V j i
via somet' : 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 schemes U i
together by identifying V i j
with V j i
, such
that the U i
's are open subschemes of the glued space.
Instances for algebraic_geometry.Scheme.glue_data
- algebraic_geometry.Scheme.glue_data.has_sizeof_inst
The glue data of locally ringed spaces spaces associated to a family of glue data of schemes.
(Implementation). The glued scheme of a glue data.
This should not be used outside this file. Use Scheme.glue_data.glued
instead.
Equations
- algebraic_geometry.Scheme.glue_data.algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.category_theory.creates_colimit D = category_theory.creates_colimit_of_fully_faithful_of_iso D.glued_Scheme (category_theory.limits.has_colimit.iso_of_nat_iso (D.to_glue_data.diagram_iso algebraic_geometry.Scheme.forget_to_LocallyRingedSpace).symm)
Equations
- algebraic_geometry.Scheme.glue_data.algebraic_geometry.Scheme.forget_to_Top.category_theory.limits.preserves_colimit D = id (category_theory.limits.comp_preserves_colimit algebraic_geometry.Scheme.forget_to_LocallyRingedSpace (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget CommRing))
The glued scheme of a glued space.
The immersion from D.U i
into the glued space.
The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.
The pullback cone spanned by V i j ⟶ U i
and V i j ⟶ U j
.
This is a pullback diagram (V_pullback_cone_is_limit
).
Equations
- D.V_pullback_cone i j = category_theory.limits.pullback_cone.mk (D.to_glue_data.f i j) (D.to_glue_data.t i j ≫ D.to_glue_data.f j i) _
The following diagram is a pullback, i.e. Vᵢⱼ
is the intersection of Uᵢ
and Uⱼ
in X
.
Vᵢⱼ ⟶ Uᵢ | | ↓ ↓ Uⱼ ⟶ X
The underlying topological space of the glued scheme is isomorphic to the gluing of the underlying spacess
Equations
- D.iso_carrier = (algebraic_geometry.PresheafedSpace.forget CommRing).map_iso (algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.map_iso (algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.map_iso D.iso_LocallyRingedSpace ≪≫ D.to_LocallyRingedSpace_glue_data.iso_SheafedSpace) ≪≫ D.to_LocallyRingedSpace_glue_data.to_SheafedSpace_glue_data.iso_PresheafedSpace) ≪≫ D.to_LocallyRingedSpace_glue_data.to_SheafedSpace_glue_data.to_PresheafedSpace_glue_data.to_glue_data.glued_iso (algebraic_geometry.PresheafedSpace.forget CommRing)
An equivalence relation on Σ i, D.U i
that holds iff 𝖣 .ι i x = 𝖣 .ι j y
.
See Scheme.gluing_data.ι_eq_iff
.
The open cover of the glued space given by the glue data.
Equations
- D.open_cover = {J := D.to_glue_data.J, obj := D.to_glue_data.U, map := D.ι, f := λ (x : ↥(D.glued.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), _.some, covers := _, is_open := _}
(Implementation) the transition maps in the glue data associated with an open cover.
Equations
- 𝒰.glued_cover_t' x y z = (category_theory.limits.pullback_right_pullback_fst_iso (𝒰.map x) (𝒰.map z) category_theory.limits.pullback.fst).hom ≫ (category_theory.limits.pullback.map (category_theory.limits.pullback.fst ≫ 𝒰.map x) (𝒰.map z) (category_theory.limits.pullback.fst ≫ 𝒰.map y) (𝒰.map z) (category_theory.limits.pullback_symmetry (𝒰.map x) (𝒰.map y)).hom (𝟙 (𝒰.obj z)) (𝟙 X) _ _ ≫ (category_theory.limits.pullback_right_pullback_fst_iso (𝒰.map y) (𝒰.map z) category_theory.limits.pullback.fst).inv) ≫ (category_theory.limits.pullback_symmetry category_theory.limits.pullback.fst category_theory.limits.pullback.fst).hom
The glue data associated with an open cover.
The canonical isomorphism 𝒰.glued_cover.glued ⟶ X
is provided by 𝒰.from_glued
.
Equations
- 𝒰.glued_cover = {to_glue_data := {J := 𝒰.J, U := 𝒰.obj, V := λ (_x : 𝒰.J × 𝒰.J), algebraic_geometry.Scheme.open_cover.glued_cover._match_1 𝒰 _x, f := λ (x y : 𝒰.J), category_theory.limits.pullback.fst, f_mono := _, f_has_pullback := _, f_id := _, t := λ (x y : 𝒰.J), (category_theory.limits.pullback_symmetry (𝒰.map x) (𝒰.map y)).hom, t_id := _, t' := λ (x y z : 𝒰.J), 𝒰.glued_cover_t' x y z, t_fac := _, cocycle := _}, f_open := _}
- algebraic_geometry.Scheme.open_cover.glued_cover._match_1 𝒰 (x, y) = category_theory.limits.pullback (𝒰.map x) (𝒰.map y)
The canonical morphism from the gluing of an open cover of X
into X
.
This is an isomorphism, as witnessed by an is_iso
instance.
Equations
- 𝒰.from_glued = category_theory.limits.multicoequalizer.desc 𝒰.glued_cover.to_glue_data.diagram X (λ (x : 𝒰.glued_cover.to_glue_data.diagram.R), 𝒰.map x) _
Instances for algebraic_geometry.Scheme.open_cover.from_glued
Given an open cover of X
, and a morphism 𝒰.obj x ⟶ Y
for each open subscheme in the cover,
such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms
together into a morphism X ⟶ Y
.
Note:
If X
is exactly (defeq to) the gluing of U i
, then using multicoequalizer.desc
suffices.