Gluing Schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 each i : 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 an is_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 each i : 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) of U i and U 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 to V i i.
algebraic_geometry.Scheme.glue_data.is_open_iff : An subset of the glued scheme is open iff all its preimages in U 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.

source

@[nolint]

structure algebraic_geometry.Scheme.glue_data :

Type (u_1+1)

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 each i : J.
An scheme V i j for each i j : J. (Note that this is J × J → Scheme rather than J → J → Scheme 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 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

source

@[reducible]

noncomputable def algebraic_geometry.Scheme.glue_data.to_LocallyRingedSpace_glue_data (D : algebraic_geometry.Scheme.glue_data) :

algebraic_geometry.LocallyRingedSpace.glue_data

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

source

noncomputable def algebraic_geometry.Scheme.glue_data.glued_Scheme (D : algebraic_geometry.Scheme.glue_data) :

algebraic_geometry.Scheme

(Implementation). The glued scheme of a glue data. This should not be used outside this file. Use Scheme.glue_data.glued instead.

Equations

D.glued_Scheme = algebraic_geometry.LocallyRingedSpace.is_open_immersion.Scheme D.to_LocallyRingedSpace_glue_data.to_glue_data.glued _

source

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.glue_data.algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.category_theory.creates_colimit (D : algebraic_geometry.Scheme.glue_data) :

category_theory.creates_colimit D.to_glue_data.diagram.multispan algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

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)

source

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.glue_data.algebraic_geometry.Scheme.forget_to_Top.category_theory.limits.preserves_colimit (D : algebraic_geometry.Scheme.glue_data) :

category_theory.limits.preserves_colimit D.to_glue_data.diagram.multispan algebraic_geometry.Scheme.forget_to_Top

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))

source

@[protected, instance]

def algebraic_geometry.Scheme.glue_data.diagram.category_theory.limits.has_multicoequalizer (D : algebraic_geometry.Scheme.glue_data) :

category_theory.limits.has_multicoequalizer D.to_glue_data.diagram

source

@[reducible]

noncomputable def algebraic_geometry.Scheme.glue_data.glued (D : algebraic_geometry.Scheme.glue_data) :

algebraic_geometry.Scheme

The glued scheme of a glued space.

source

@[reducible]

noncomputable def algebraic_geometry.Scheme.glue_data.ι (D : algebraic_geometry.Scheme.glue_data) (i : D.to_glue_data.J) :

D.to_glue_data.U i ⟶ D.glued

The immersion from D.U i into the glued space.

source

@[reducible]

noncomputable def algebraic_geometry.Scheme.glue_data.iso_LocallyRingedSpace (D : algebraic_geometry.Scheme.glue_data) :

D.glued.to_LocallyRingedSpace ≅ D.to_LocallyRingedSpace_glue_data.to_glue_data.glued

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

source

theorem algebraic_geometry.Scheme.glue_data.ι_iso_LocallyRingedSpace_inv (D : algebraic_geometry.Scheme.glue_data) (i : D.to_glue_data.J) :

D.to_LocallyRingedSpace_glue_data.to_glue_data.ι i ≫ D.iso_LocallyRingedSpace.inv = D.to_glue_data.ι i

source

@[protected, instance]

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

algebraic_geometry.is_open_immersion (D.to_glue_data.ι i)

source

theorem algebraic_geometry.Scheme.glue_data.ι_jointly_surjective (D : algebraic_geometry.Scheme.glue_data) (x : ↥(D.to_glue_data.glued.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

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

source

@[simp]

theorem algebraic_geometry.Scheme.glue_data.glue_condition_assoc (D : algebraic_geometry.Scheme.glue_data) (i j : D.to_glue_data.J) {X' : algebraic_geometry.Scheme} (f' : D.glued ⟶ X') :

D.to_glue_data.t i j ≫ D.to_glue_data.f j i ≫ D.ι j ≫ f' = D.to_glue_data.f i j ≫ D.ι i ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.glue_data.glue_condition (D : algebraic_geometry.Scheme.glue_data) (i j : D.to_glue_data.J) :

D.to_glue_data.t i j ≫ D.to_glue_data.f j i ≫ D.ι j = D.to_glue_data.f i j ≫ D.ι i

source

noncomputable def algebraic_geometry.Scheme.glue_data.V_pullback_cone (D : algebraic_geometry.Scheme.glue_data) (i j : D.to_glue_data.J) :

category_theory.limits.pullback_cone (D.ι i) (D.ι j)

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) _

source

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

category_theory.limits.is_limit (D.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.Scheme.forget_to_LocallyRingedSpace i j (D.to_LocallyRingedSpace_glue_data.V_pullback_cone_is_limit i j)

source

noncomputable def algebraic_geometry.Scheme.glue_data.iso_carrier (D : algebraic_geometry.Scheme.glue_data) :

D.glued.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier ≅ D.to_LocallyRingedSpace_glue_data.to_SheafedSpace_glue_data.to_PresheafedSpace_glue_data.to_Top_glue_data.to_glue_data.glued

The underlying topological space of the glued scheme is isomorphic to the gluing of the underlying spacess

Equations

source

@[simp]

theorem algebraic_geometry.Scheme.glue_data.ι_iso_carrier_inv (D : algebraic_geometry.Scheme.glue_data) (i : D.to_glue_data.J) :

D.to_LocallyRingedSpace_glue_data.to_SheafedSpace_glue_data.to_PresheafedSpace_glue_data.to_Top_glue_data.to_glue_data.ι i ≫ D.iso_carrier.inv = (D.ι i).val.base

source

def algebraic_geometry.Scheme.glue_data.rel (D : algebraic_geometry.Scheme.glue_data) (a b : Σ (i : D.to_glue_data.J), ↥((D.to_glue_data.U i).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

Prop

An equivalence relation on Σ i, D.U i that holds iff 𝖣 .ι i x = 𝖣 .ι j y. See Scheme.gluing_data.ι_eq_iff.

Equations

D.rel a b = (a = b ∨ ∃ (x : ↥((D.to_glue_data.V (a.fst, b.fst)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), ⇑((D.to_glue_data.f a.fst b.fst).val.base) x = a.snd ∧ ⇑((D.to_glue_data.t a.fst b.fst ≫ D.to_glue_data.f b.fst a.fst).val.base) x = b.snd)

source

theorem algebraic_geometry.Scheme.glue_data.ι_eq_iff (D : algebraic_geometry.Scheme.glue_data) (i j : D.to_glue_data.J) (x : ↥((D.to_glue_data.U i).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (y : ↥((D.to_glue_data.U j).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

⇑((D.to_glue_data.ι i).val.base) x = ⇑((D.to_glue_data.ι j).val.base) y ↔ D.rel ⟨i, x⟩ ⟨j, y⟩

source

theorem algebraic_geometry.Scheme.glue_data.is_open_iff (D : algebraic_geometry.Scheme.glue_data) (U : set ↥(D.glued.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

is_open U ↔ ∀ (i : D.to_glue_data.J), is_open (⇑((D.ι i).val.base) ⁻¹' U)

source

noncomputable def algebraic_geometry.Scheme.glue_data.open_cover (D : algebraic_geometry.Scheme.glue_data) :

D.glued.open_cover

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 := _}

source

noncomputable def algebraic_geometry.Scheme.open_cover.glued_cover_t' {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

category_theory.limits.pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst ⟶ category_theory.limits.pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst

(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

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_fst_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : 𝒰.obj y ⟶ X') :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_fst {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_snd_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : 𝒰.obj z ⟶ X') :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_fst_snd {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_fst {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_fst_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : 𝒰.obj y ⟶ X') :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_snd_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : 𝒰.obj x ⟶ X') :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_t'_snd_snd {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst

source

theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle_fst {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ 𝒰.glued_cover_t' y z x ≫ 𝒰.glued_cover_t' z x y ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst

source

theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle_snd {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ 𝒰.glued_cover_t' y z x ≫ 𝒰.glued_cover_t' z x y ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd

source

theorem algebraic_geometry.Scheme.open_cover.glued_cover_cocycle {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover_t' x y z ≫ 𝒰.glued_cover_t' y z x ≫ 𝒰.glued_cover_t' z x y = 𝟙 (category_theory.limits.pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst)

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_U {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (j : 𝒰.J) :

𝒰.glued_cover.to_glue_data.U j = 𝒰.obj j

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

𝒰.glued_cover.to_glue_data.J = 𝒰.J

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_t {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y : 𝒰.J) :

𝒰.glued_cover.to_glue_data.t x y = (category_theory.limits.pullback_symmetry (𝒰.map x) (𝒰.map y)).hom

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_f {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y : 𝒰.J) :

𝒰.glued_cover.to_glue_data.f x y = category_theory.limits.pullback.fst

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_V {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (_x : 𝒰.J × 𝒰.J) :

𝒰.glued_cover.to_glue_data.V _x = algebraic_geometry.Scheme.open_cover.glued_cover._match_1 𝒰 _x

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_t' {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x y z : 𝒰.J) :

𝒰.glued_cover.to_glue_data.t' x y z = 𝒰.glued_cover_t' x y z

source

noncomputable def algebraic_geometry.Scheme.open_cover.glued_cover {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

algebraic_geometry.Scheme.glue_data

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)

source

noncomputable def algebraic_geometry.Scheme.open_cover.from_glued {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

𝒰.glued_cover.glued ⟶ X

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

algebraic_geometry.Scheme.open_cover.from_glued.category_theory.is_iso

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.ι_from_glued {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x : 𝒰.J) :

𝒰.glued_cover.ι x ≫ 𝒰.from_glued = 𝒰.map x

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.ι_from_glued_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : X ⟶ X') :

𝒰.glued_cover.ι x ≫ 𝒰.from_glued ≫ f' = 𝒰.map x ≫ f'

source

theorem algebraic_geometry.Scheme.open_cover.from_glued_injective {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

function.injective ⇑(𝒰.from_glued.val.base)

source

@[protected, instance]

def algebraic_geometry.Scheme.open_cover.from_glued_stalk_iso {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (x : ↥(𝒰.glued_cover.glued.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map 𝒰.from_glued.val x)

source

theorem algebraic_geometry.Scheme.open_cover.from_glued_open_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

is_open_map ⇑(𝒰.from_glued.val.base)

source

theorem algebraic_geometry.Scheme.open_cover.from_glued_open_embedding {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

open_embedding ⇑(𝒰.from_glued.val.base)

source

@[protected, instance]

def algebraic_geometry.Scheme.open_cover.base.category_theory.epi {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

category_theory.epi 𝒰.from_glued.val.base

source

@[protected, instance]

def algebraic_geometry.Scheme.open_cover.from_glued_open_immersion {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

algebraic_geometry.is_open_immersion 𝒰.from_glued

source

@[protected, instance]

def algebraic_geometry.Scheme.open_cover.from_glued.category_theory.is_iso {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) :

category_theory.is_iso 𝒰.from_glued

source

noncomputable def algebraic_geometry.Scheme.open_cover.glue_morphisms {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Π (x : 𝒰.J), 𝒰.obj x ⟶ Y) (hf : ∀ (x y : 𝒰.J), category_theory.limits.pullback.fst ≫ f x = category_theory.limits.pullback.snd ≫ f y) :

X ⟶ Y

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.

Equations

𝒰.glue_morphisms f hf = category_theory.inv 𝒰.from_glued ≫ category_theory.limits.multicoequalizer.desc 𝒰.glued_cover.to_glue_data.diagram Y f _

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.ι_glue_morphisms_assoc {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Π (x : 𝒰.J), 𝒰.obj x ⟶ Y) (hf : ∀ (x y : 𝒰.J), category_theory.limits.pullback.fst ≫ f x = category_theory.limits.pullback.snd ≫ f y) (x : 𝒰.J) {X' : algebraic_geometry.Scheme} (f' : Y ⟶ X') :

𝒰.map x ≫ 𝒰.glue_morphisms f hf ≫ f' = f x ≫ f'

source

@[simp]

theorem algebraic_geometry.Scheme.open_cover.ι_glue_morphisms {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f : Π (x : 𝒰.J), 𝒰.obj x ⟶ Y) (hf : ∀ (x y : 𝒰.J), category_theory.limits.pullback.fst ≫ f x = category_theory.limits.pullback.snd ≫ f y) (x : 𝒰.J) :

𝒰.map x ≫ 𝒰.glue_morphisms f hf = f x

source

theorem algebraic_geometry.Scheme.open_cover.hom_ext {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f₁ f₂ : X ⟶ Y) (h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂) :

f₁ = f₂