Gluing Schemes #

Given a family of gluing data of schemes, we may glue them together. Also see the section about "locally directed" gluing, which is a special case where the conditions are easier to check.

Main definitions #

AlgebraicGeometry.Scheme.GlueData: A structure containing the family of gluing data.
AlgebraicGeometry.Scheme.GlueData.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.
AlgebraicGeometry.Scheme.GlueData.ι: The immersion ι i : U i ⟶ glued for each i : J.
AlgebraicGeometry.Scheme.GlueData.isoCarrier: The isomorphism between the underlying space of the glued scheme and the gluing of the underlying topological spaces.
AlgebraicGeometry.Scheme.OpenCover.gluedCover: The glue data associated with an open cover.
AlgebraicGeometry.Scheme.OpenCover.fromGlued: The canonical morphism 𝒰.gluedCover.glued ⟶ X. This has an is_iso instance.
AlgebraicGeometry.Scheme.OpenCover.glueMorphisms: We may glue a family of compatible morphisms defined on an open cover of a scheme.

Main results #

AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion: The map ι i : U i ⟶ glued is an open immersion for each i : J.
AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective : The underlying maps of ι i : U i ⟶ glued are jointly surjective.
AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimit : V i j is the pullback (intersection) of U i and U j over the glued space.
AlgebraicGeometry.Scheme.GlueData.ι_eq_iff : ι i x = ι j y if and only if they coincide when restricted to V i i.
AlgebraicGeometry.Scheme.GlueData.isOpen_iff : A 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 Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean where we glue presheafed spaces, sheafed spaces, and locally ringed spaces.

source

structure AlgebraicGeometry.Scheme.GlueDataextends CategoryTheory.GlueData AlgebraicGeometry.Scheme :

Type (u_1 + 1)

A family of gluing data consists of

An index type J
A scheme U i for each i : J.
A 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.

J : Type u_1
U : self.J → AlgebraicGeometry.Scheme
V : self.J × self.J → AlgebraicGeometry.Scheme
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)

Instances For

source

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData (D : GlueData) :

LocallyRingedSpace.GlueData

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

Equations

D.toLocallyRingedSpaceGlueData = { toGlueData := D.mapGlueData AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, f_open := ⋯ }

Instances For

source

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) :

LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

source

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) :

SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)

source

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) :

PresheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)

source

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData (D : GlueData) (i : D.J) :

LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i)

source

def AlgebraicGeometry.Scheme.GlueData.gluedScheme (D : GlueData) :

Scheme

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

Equations

D.gluedScheme = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme D.toLocallyRingedSpaceGlueData.glued ⋯

Instances For

source

instance AlgebraicGeometry.Scheme.GlueData.instCreatesColimitLocallyRingedSpaceWalkingMultispanProdJMultispanDiagramForgetToLocallyRingedSpace (D : GlueData) :

CategoryTheory.CreatesColimit D.diagram.multispan forgetToLocallyRingedSpace

Equations

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

source

instance AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop (D : GlueData) :

CategoryTheory.Limits.PreservesColimit D.diagram.multispan forgetToTop

source

instance AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget (D : GlueData) :

CategoryTheory.Limits.PreservesColimit D.diagram.multispan forget

source

instance AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram (D : GlueData) :

CategoryTheory.Limits.HasMulticoequalizer D.diagram

source

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.glued (D : GlueData) :

Scheme

The glued scheme of a glued space.

Equations

D.glued = D.glued

Instances For

source

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.ι (D : GlueData) (i : D.J) :

D.U i ⟶ D.glued

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

Equations

D.ι i = D.ι i

Instances For

source

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace (D : GlueData) :

D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued

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

Equations

D.isoLocallyRingedSpace = D.gluedIso AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Instances For

source

theorem AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv (D : GlueData) (i : D.J) :

CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData.ι i) D.isoLocallyRingedSpace.inv = Hom.toLRSHom (D.ι i)

source

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

IsOpenImmersion (D.ι i)

source

theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : GlueData) (x : ↥D.glued) :

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

source

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition (D : GlueData) (i j : D.J) :

CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) = CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)

Promoted to higher priority to short circuit simplifier.

source

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc (D : GlueData) (i j : D.J) {Z : Scheme} (h : D.glued ⟶ Z) :

CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (CategoryTheory.CategoryStruct.comp (D.ι j) h)) = CategoryTheory.CategoryStruct.comp (D.f i j) (CategoryTheory.CategoryStruct.comp (D.ι i) h)

Promoted to higher priority to short circuit simplifier.

source

def AlgebraicGeometry.Scheme.GlueData.vPullbackCone (D : GlueData) (i j : D.J) :

CategoryTheory.Limits.PullbackCone (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 (vPullbackConeIsLimit).

Equations

D.vPullbackCone i j = CategoryTheory.Limits.PullbackCone.mk (D.f i j) (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)) ⋯

Instances For

source

def AlgebraicGeometry.Scheme.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

Equations

D.vPullbackConeIsLimit i j = D.vPullbackConeIsLimitOfMap AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace i j (D.toLocallyRingedSpaceGlueData.vPullbackConeIsLimit i j)

Instances For

source

def AlgebraicGeometry.Scheme.GlueData.isoCarrier (D : GlueData) :

↑D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

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

Equations

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv (D : GlueData) (i : D.J) :

CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) D.isoCarrier.inv = (D.ι i).base

source

def AlgebraicGeometry.Scheme.GlueData.Rel (D : GlueData) (a b : (i : D.J) × ↥(D.U i)) :

Prop

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

Equations

D.Rel a b = ∃ (x : ↥(D.V (a.fst, b.fst))), (D.f a.fst b.fst) x = a.snd ∧ (CategoryTheory.CategoryStruct.comp (D.t a.fst b.fst) (D.f b.fst a.fst)) x = b.snd

Instances For

source

theorem AlgebraicGeometry.Scheme.GlueData.ι_eq_iff (D : GlueData) (i j : D.J) (x : ↥(D.U i)) (y : ↥(D.U j)) :

(D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

source

theorem AlgebraicGeometry.Scheme.GlueData.isOpen_iff (D : GlueData) (U : Set ↥D.glued) :

IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)

source

def AlgebraicGeometry.Scheme.GlueData.openCover (D : GlueData) :

D.glued.OpenCover

The open cover of the glued space given by the glue data.

Equations

D.openCover = { I₀ := D.J, X := D.U, f := D.ι, mem₀ := ⋯ }

Instances For

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_I₀ (D : GlueData) :

D.openCover.I₀ = D.J

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_X (D : GlueData) (a✝ : D.J) :

D.openCover.X a✝ = D.U a✝

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_f (D : GlueData) (i : D.J) :

D.openCover.f i = D.ι i

source

def AlgebraicGeometry.Scheme.Cover.gluedCoverT' {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)) ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z)) (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))

(Implementation) the transition maps in the glue data associated with an open cover.

Equations

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

source

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : Scheme} (h : 𝒰.X y ⟶ Z) :

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

source

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : Scheme} (h : 𝒰.X z ⟶ Z) :

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

source

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : Scheme} (h : 𝒰.X y ⟶ Z) :

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

source

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : Scheme} (h : 𝒰.X x ⟶ Z) :

source

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 z x y) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))

source

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 z x y) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))

source

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 y z x) (gluedCoverT' 𝒰 z x y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))

source

def AlgebraicGeometry.Scheme.Cover.gluedCover {X : Scheme} (𝒰 : X.OpenCover) :

GlueData

The glue data associated with an open cover. The canonical isomorphism 𝒰.gluedCover.glued ⟶ X is provided by 𝒰.fromGlued.

Equations

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_U {X : Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀) :

(gluedCover 𝒰).U i = 𝒰.X i

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_f {X : Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.I₀) :

(gluedCover 𝒰).f x✝ x✝¹ = CategoryTheory.Limits.pullback.fst (𝒰.f x✝) (𝒰.f x✝¹)

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_t' {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) :

(gluedCover 𝒰).t' x y z = gluedCoverT' 𝒰 x y z

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_J {X : Scheme} (𝒰 : X.OpenCover) :

(gluedCover 𝒰).J = 𝒰.I₀

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_V {X : Scheme} (𝒰 : X.OpenCover) (x✝ : 𝒰.I₀ × 𝒰.I₀) :

(gluedCover 𝒰).V x✝ = match x✝ with | (x, y) => CategoryTheory.Limits.pullback (𝒰.f x) (𝒰.f y)

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_t {X : Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.I₀) :

(gluedCover 𝒰).t x✝ x✝¹ = (CategoryTheory.Limits.pullbackSymmetry (𝒰.f x✝) (𝒰.f x✝¹)).hom

source

def AlgebraicGeometry.Scheme.Cover.fromGlued {X : Scheme} (𝒰 : X.OpenCover) :

(gluedCover 𝒰).glued ⟶ X

The canonical morphism from the gluing of an open cover of X into X. This is an isomorphism, as witnessed by an IsIso instance.

Equations

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ι_fromGlued {X : Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀) :

CategoryTheory.CategoryStruct.comp ((gluedCover 𝒰).ι x) (fromGlued 𝒰) = 𝒰.f x

source

theorem AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc {X : Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀) {Z : Scheme} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((gluedCover 𝒰).ι x) (CategoryTheory.CategoryStruct.comp (fromGlued 𝒰) h) = CategoryTheory.CategoryStruct.comp (𝒰.f x) h

source

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_injective {X : Scheme} (𝒰 : X.OpenCover) :

Function.Injective ⇑(fromGlued 𝒰)

source

instance AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued {X : Scheme} (𝒰 : X.OpenCover) (x : ↥(gluedCover 𝒰).glued) :

CategoryTheory.IsIso (Hom.stalkMap (fromGlued 𝒰) x)

source

theorem AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued {X : Scheme} (𝒰 : X.OpenCover) :

IsOpenMap ⇑(fromGlued 𝒰)

source

@[deprecated AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_open_map {X : Scheme} (𝒰 : X.OpenCover) :

IsOpenMap ⇑(fromGlued 𝒰)

Alias of AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued.

source

theorem AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued {X : Scheme} (𝒰 : X.OpenCover) :

Topology.IsOpenEmbedding ⇑(fromGlued 𝒰)

source

@[deprecated AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding {X : Scheme} (𝒰 : X.OpenCover) :

Topology.IsOpenEmbedding ⇑(fromGlued 𝒰)

Alias of AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued.

source

instance AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued {X : Scheme} (𝒰 : X.OpenCover) :

CategoryTheory.Epi (fromGlued 𝒰).base

source

instance AlgebraicGeometry.Scheme.Cover.instIsOpenImmersionFromGlued {X : Scheme} (𝒰 : X.OpenCover) :

IsOpenImmersion (fromGlued 𝒰)

source

instance AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued {X : Scheme} (𝒰 : X.OpenCover) :

CategoryTheory.IsIso (fromGlued 𝒰)

source

def AlgebraicGeometry.Scheme.Cover.glueMorphisms {X : Scheme} (𝒰 : X.OpenCover) {Y : Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) :

X ⟶ Y

Given an open cover of X, and a morphism 𝒰.X 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

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

Instances For

source

theorem AlgebraicGeometry.Scheme.Cover.hom_ext {X : Scheme} (𝒰 : X.OpenCover) {Y : Scheme} (f₁ f₂ : X ⟶ Y) (h : ∀ (x : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f x) f₁ = CategoryTheory.CategoryStruct.comp (𝒰.f x) f₂) :

f₁ = f₂

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms {X : Scheme} (𝒰 : X.OpenCover) {Y : Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) (x : 𝒰.I₀) :

CategoryTheory.CategoryStruct.comp (𝒰.f x) (glueMorphisms 𝒰 f hf) = f x

source

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc {X : Scheme} (𝒰 : X.OpenCover) {Y : Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) (hf : ∀ (x y : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) (x : 𝒰.I₀) {Z : Scheme} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (𝒰.f x) (CategoryTheory.CategoryStruct.comp (glueMorphisms 𝒰 f hf) h) = CategoryTheory.CategoryStruct.comp (f x) h

source

theorem AlgebraicGeometry.Scheme.hom_ext_of_forall {X Y : Scheme} (f g : X ⟶ Y) (H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g) :

f = g

source

instance AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage :

(CategoryTheory.MorphismProperty.isomorphisms Scheme).IsLocalAtTarget zariskiPrecoverage

Locally directed gluing #

We say that a diagram of open immersions is "locally directed" if for any V, W ⊆ U in the diagram, V ∩ W is a union of elements in the diagram. Equivalently, for every x ∈ U in the diagram, the set of elements containing x is directed (and hence the name).

For such a diagram, we can glue them directly since the gluing conditions are always satisfied. The intended usage is to provide the following instances:

∀ {i j} (f : i ⟶ j), IsOpenImmersion (F.map f)
(F ⋙ forget).IsLocallyDirected and to directly use the colimit API. Also see AlgebraicGeometry.Scheme.IsLocallyDirected.openCover for the open cover of the colimit.

source