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

🔶 coverage

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

🔸 coverage

@[reducible, inline]

noncomputable 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.

Instances For

source

📐 coverage

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

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

source

📐 coverage

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

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

source

📐 coverage

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

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

source

📐 coverage

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

LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i)

source

🔸 coverage

noncomputable 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.

Instances For

source

🔸 coverage

@[implicit_reducible]

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

CategoryTheory.CreatesColimit D.diagram.multispan forgetToLocallyRingedSpace

source

📐 coverage

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

CategoryTheory.Limits.PreservesColimit D.diagram.multispan forgetToTop

source

📐 coverage

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

CategoryTheory.Limits.PreservesColimit D.diagram.multispan forget

source

📐 coverage

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

CategoryTheory.Limits.HasMulticoequalizer D.diagram

source

🔸 coverage

@[reducible, inline]

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

Scheme

The glued scheme of a glued space.

Instances For

source

🔸 coverage

@[reducible, inline]

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

D.U i ⟶ D.glued

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

Instances For

source

🔸 coverage

@[reducible, inline]

noncomputable 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.

Instances For

source

📐 coverage

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

📐 coverage

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

IsOpenImmersion (D.ι i)

source

📐 coverage

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

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

source

📐 coverage

@[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

📐 coverage

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

🔸 coverage

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

Instances For

source

🔸 coverage

noncomputable 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

Instances For

source

🔸 coverage

noncomputable 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

Instances For

source

📐 coverage

@[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

🔹 coverage

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.

Instances For

source

📐 coverage

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

📐 coverage

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

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

source

🔸 coverage

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

D.glued.OpenCover

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

Instances For

source

📐 coverage

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

D.openCover.I₀ = D.J

source

📐 coverage

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

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

source

📐 coverage

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

D.openCover.f i = D.ι i

source

🔸 coverage

noncomputable 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.

Instances For

source

📐 coverage

@[simp]

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

source

📐 coverage

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

source

📐 coverage

@[simp]

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

source

📐 coverage

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

source

📐 coverage

@[simp]

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

source

📐 coverage

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

source

📐 coverage

@[simp]

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

source

📐 coverage

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

source

📐 coverage

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

📐 coverage

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

📐 coverage

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

🔸 coverage

noncomputable 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.

Instances For

source

📐 coverage

@[simp]

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

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

source

📐 coverage

@[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

📐 coverage

@[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

📐 coverage

@[simp]

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

(gluedCover 𝒰).J = 𝒰.I₀

source

📐 coverage

@[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

📐 coverage

@[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

🔸 coverage

noncomputable 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.

Instances For

source

📐 coverage

@[simp]

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

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

source

📐 coverage

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

📐 coverage

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

Function.Injective ⇑(fromGlued 𝒰)

source

📐 coverage

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

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

source

📐 coverage

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

IsOpenMap ⇑(fromGlued 𝒰)

source

📐 coverage

@[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

📐 coverage

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

Topology.IsOpenEmbedding ⇑(fromGlued 𝒰)

source

📐 coverage

@[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

📐 coverage

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

CategoryTheory.Epi (fromGlued 𝒰).base

source

📐 coverage

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

IsOpenImmersion (fromGlued 𝒰)

source

📐 coverage

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

CategoryTheory.IsIso (fromGlued 𝒰)

source

🔸 coverage

noncomputable 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.

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

📐 coverage

@[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

📐 coverage

@[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

📐 coverage

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

🔸 coverage