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 AlgebraicGeometry/PresheafedSpace/Gluing.lean where we glue presheafed spaces, sheafed spaces, and locally ringed spaces.

structure AlgebraicGeometry.Scheme.GlueDataextends CategoryTheory.GlueData AlgebraicGeometry.Scheme : Type (u_1 + 1)

A family of gluing data consists of

1. An index type J
2. A scheme U i for each i : J.
3. 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.)
4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
6. f i i is an isomorphism.
7. t i i is the identity.
8. 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.
9. 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)

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

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) : LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) : SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData (D : GlueData) (i j : D.J) : PresheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)

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

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.

instance AlgebraicGeometry.Scheme.GlueData.instCreatesColimitLocallyRingedSpaceWalkingMultispanProdJMultispanDiagramForgetToLocallyRingedSpace (D : GlueData) : CategoryTheory.CreatesColimit D.diagram.multispan forgetToLocallyRingedSpace

instance AlgebraicGeometry.Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop (D : GlueData) : CategoryTheory.Limits.PreservesColimit D.diagram.multispan forgetToTop

instance AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget (D : GlueData) : CategoryTheory.Limits.PreservesColimit D.diagram.multispan forget

instance AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram (D : GlueData) : CategoryTheory.Limits.HasMulticoequalizer D.diagram

@[reducible, inline]

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

The glued scheme of a glued space.

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

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

theorem AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv (D : GlueData) (i : D.J) : CategoryTheory.CategoryStruct.comp (D.toLocallyRingedSpaceGlueData.ι i) D.isoLocallyRingedSpace.inv = Hom.toLRSHom (D.ι i)

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

theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : GlueData) (x : ↥D.glued) : ∃ (i : D.J) (y : ↥(D.U i)), (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = x

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

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)

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

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

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

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

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.

theorem AlgebraicGeometry.Scheme.GlueData.ι_eq_iff (D : GlueData) (i j : D.J) (x : ↥(D.U i)) (y : ↥(D.U j)) : (CategoryTheory.ConcreteCategory.hom (D.ι i).base) x = (CategoryTheory.ConcreteCategory.hom (D.ι j).base) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

theorem AlgebraicGeometry.Scheme.GlueData.isOpen_iff (D : GlueData) (U : Set ↥D.glued) : IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i).base) ⁻¹' U)

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

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

theorem AlgebraicGeometry.Scheme.GlueData.openCover_J (D : GlueData) : D.openCover.J = D.J

theorem AlgebraicGeometry.Scheme.GlueData.openCover_f (D : GlueData) (x : ↥D.glued) : D.openCover.f x = ⋯.choose

theorem AlgebraicGeometry.Scheme.GlueData.openCover_map (D : GlueData) (i : D.J) : D.openCover.map i = D.ι i

theorem AlgebraicGeometry.Scheme.GlueData.openCover_obj (D : GlueData) (a✝ : D.J) : D.openCover.obj a✝ = D.U a✝

def AlgebraicGeometry.Scheme.Cover.gluedCoverT' {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y))

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : Scheme} (h : 𝒰.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map z))

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : Scheme} (h : 𝒰.obj z ⟶ Z) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map z)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map z)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y))

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : Scheme} (h : 𝒰.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map x))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y))

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : Scheme} (h : 𝒰.obj x ⟶ Z) : CategoryTheory.CategoryStruct.comp (gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map x)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) h)

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : 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 (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))))) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : 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 (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))

theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : 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 (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)))

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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_U {X : Scheme} (𝒰 : X.OpenCover) (j : 𝒰.J) : (gluedCover 𝒰).U j = 𝒰.obj j

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_V {X : Scheme} (𝒰 : X.OpenCover) (x✝ : 𝒰.J × 𝒰.J) : (gluedCover 𝒰).V x✝ = match x✝ with | (x, y) => CategoryTheory.Limits.pullback (𝒰.map x) (𝒰.map y)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_t' {X : Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : (gluedCover 𝒰).t' x y z = gluedCoverT' 𝒰 x y z

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_f {X : Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.J) : (gluedCover 𝒰).f x✝ x✝¹ = CategoryTheory.Limits.pullback.fst (𝒰.map x✝) (𝒰.map x✝¹)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCover_t {X : Scheme} (𝒰 : X.OpenCover) (x✝ x✝¹ : 𝒰.J) : (gluedCover 𝒰).t x✝ x✝¹ = (CategoryTheory.Limits.pullbackSymmetry (𝒰.map x✝) (𝒰.map x✝¹)).hom

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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ι_fromGlued {X : Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) : CategoryTheory.CategoryStruct.comp ((gluedCover 𝒰).ι x) (fromGlued 𝒰) = 𝒰.map x

theorem AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc {X : Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((gluedCover 𝒰).ι x) (CategoryTheory.CategoryStruct.comp (fromGlued 𝒰) h) = CategoryTheory.CategoryStruct.comp (𝒰.map x) h

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_injective {X : Scheme} (𝒰 : X.OpenCover) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (fromGlued 𝒰).base)

instance AlgebraicGeometry.Scheme.Cover.fromGlued_stalk_iso {X : Scheme} (𝒰 : X.OpenCover) (x : ↥(gluedCover 𝒰).glued) : CategoryTheory.IsIso (Hom.stalkMap (fromGlued 𝒰) x)

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_open_map {X : Scheme} (𝒰 : X.OpenCover) : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom (fromGlued 𝒰).base)

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding {X : Scheme} (𝒰 : X.OpenCover) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (fromGlued 𝒰).base)

instance AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued {X : Scheme} (𝒰 : X.OpenCover) : CategoryTheory.Epi (fromGlued 𝒰).base

instance AlgebraicGeometry.Scheme.Cover.fromGlued_open_immersion {X : Scheme} (𝒰 : X.OpenCover) : IsOpenImmersion (fromGlued 𝒰)

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

def AlgebraicGeometry.Scheme.Cover.glueMorphisms {X : Scheme} (𝒰 : X.OpenCover) {Y : Scheme} (f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y) (hf : ∀ (x y : 𝒰.J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (f x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y)) (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.

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

@[simp]

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

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

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

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.

noncomputable def AlgebraicGeometry.Scheme.IsLocallyDirected.V {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] (i j : J) : (F.obj i).Opens

(Implementation detail) The intersection V in the glue data associated to a locally directed diagram.

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.V_self {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] (i : J) : V F i i = ⊤

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] {i j k : J} (x : ↥(CategoryTheory.Limits.pullback (V F i j).ι (V F i k).ι)) : ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ CategoryTheory.Limits.pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)), IsOpenImmersion α ∧ CategoryTheory.CategoryStruct.comp α (CategoryTheory.Limits.pullback.fst (V F i j).ι (V F i k).ι) = CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map fi)).hom ((F.obj i).homOfLE ⋯) ∧ CategoryTheory.CategoryStruct.comp α (CategoryTheory.Limits.pullback.snd (V F i j).ι (V F i k).ι) = CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map fi)).hom ((F.obj i).homOfLE ⋯) ∧ (CategoryTheory.ConcreteCategory.hom α.base) z = x

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J} (k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)) {U : (F.obj i).Opens} (h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U) (h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)) (CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map k₁.snd.1)).inv (F.map k₁.snd.2)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)) (CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map k₂.snd.1)).inv (F.map k₂.snd.2))

def AlgebraicGeometry.Scheme.IsLocallyDirected.tAux {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] (i j : J) : ↑(V F i j) ⟶ F.obj j

(Implementation detail) The inclusion map V i j ⟶ F j in the glue data associated to a locally directed diagram.

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] (i j : J) {k : J} (fi : k ⟶ i) (fj : k ⟶ j) : CategoryTheory.CategoryStruct.comp ((F.obj i).homOfLE ⋯) (tAux F i j) = CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map fi)).inv (F.map fj)

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] (i j : J) {k : J} (fi : k ⟶ i) (fj : k ⟶ j) {Z : Scheme} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj i).homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (tAux F i j) h) = CategoryTheory.CategoryStruct.comp (Hom.isoOpensRange (F.map fi)).inv (CategoryTheory.CategoryStruct.comp (F.map fj) h)

def AlgebraicGeometry.Scheme.IsLocallyDirected.t {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] (i j : J) : ↑(V F i j) ⟶ ↑(V F j i)

(Implementation detail) The transition map V i j ⟶ V j i in the glue data associated to a locally directed diagram.

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.t_id {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] (i : J) : t F i i = CategoryTheory.CategoryStruct.id ↑(V F i i)

def AlgebraicGeometry.Scheme.IsLocallyDirected.glueData {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : GlueData

(Implementation detail) The glue data associated to a locally directed diagram.

One usually does not want to use this directly, and instead use the generic colimit API.

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] {i j : Shrink.{u, w} J} (f : (equivShrink J).symm i ⟶ (equivShrink J).symm j) : CategoryTheory.CategoryStruct.comp (F.map f) ((glueData F).ι j) = (glueData F).ι i

def AlgebraicGeometry.Scheme.IsLocallyDirected.cocone {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.Cocone F

(Implementation detail) The cocone associated to a locally directed diagram.

One usually does not want to use this directly, and instead use the generic colimit API.

noncomputable def AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.IsColimit (cocone F)

(Implementation detail) The cocone associated to a locally directed diagram is a colimit.

One usually does not want to use this directly, and instead use the generic colimit API.

noncomputable def AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.IsColimit (forgetToLocallyRingedSpace.mapCocone (cocone F))

(Implementation detail) The cocone associated to a locally directed diagram is a colimit as locally ringed spaces.

One usually does not want to use this directly, and instead use the generic colimit API.

instance AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.HasColimit F

instance AlgebraicGeometry.Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.PreservesColimit F forgetToLocallyRingedSpace

instance AlgebraicGeometry.Scheme.IsLocallyDirected.instCreatesColimitLocallyRingedSpaceForgetToLocallyRingedSpace {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.CreatesColimit F forgetToLocallyRingedSpace

def AlgebraicGeometry.Scheme.IsLocallyDirected.openCover {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : (CategoryTheory.Limits.colimit F).OpenCover

The open cover of the colimit of a locally directed diagram by the components.

@[simp]

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_J {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : (openCover F).J = J

@[simp]

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_obj {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : (openCover F).obj = F.obj

@[simp]

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_map {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : (openCover F).map = CategoryTheory.Limits.colimit.ι F

instance AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] (i : J) : IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] {i j : J} {xi : ↥(F.obj i)} {xj : ↥(F.obj j)} : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i).base) xi = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j).base) xj ↔ ∃ (k : J) (fi : k ⟶ i) (fj : k ⟶ j) (x : ↥(F.obj k)), (CategoryTheory.ConcreteCategory.hom (F.map fi).base) x = xi ∧ (CategoryTheory.ConcreteCategory.hom (F.map fj).base) x = xj

instance AlgebraicGeometry.Scheme.IsLocallyDirected.instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) Scheme) [∀ {i j : CategoryTheory.Limits.WidePushoutShape J} (f : i ⟶ j), IsOpenImmersion (F.map f)] : (F.comp forget).IsLocallyDirected