Gluing Schemes

Given a family of gluing data of schemes, we may glue them together.

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) : CategoryTheory.Mono (self.f i j)
• f_hasPullback (i j k : self.J) : CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : CategoryTheory.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 = CategoryTheory.CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : AlgebraicGeometry.IsOpenImmersion (self.f i j)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData (D : AlgebraicGeometry.Scheme.GlueData) : AlgebraicGeometry.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 := ⋯ }

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

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

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

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

def AlgebraicGeometry.Scheme.GlueData.gluedScheme (D : AlgebraicGeometry.Scheme.GlueData) : AlgebraicGeometry.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 ⋯

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

Equations

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

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

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

@[reducible, inline]

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

The glued scheme of a glued space.

Equations

• D.glued = D.glued

@[reducible, inline]

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

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

Equations

• D.ι i = D.ι i

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace (D : AlgebraicGeometry.Scheme.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

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

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

theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : AlgebraicGeometry.Scheme.GlueData) (x : ↑↑D.glued.toPresheafedSpace) : ∃ (i : D.J) (y : ↑↑(D.U i).toPresheafedSpace), (D.ι i).base y = x

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition (D : AlgebraicGeometry.Scheme.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)

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J) {Z : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme.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)) ⋯

def AlgebraicGeometry.Scheme.GlueData.vPullbackConeIsLimit (D : AlgebraicGeometry.Scheme.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)

def AlgebraicGeometry.Scheme.GlueData.isoCarrier (D : AlgebraicGeometry.Scheme.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.

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv (D : AlgebraicGeometry.Scheme.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 : AlgebraicGeometry.Scheme.GlueData) (a b : (i : D.J) × ↑↑(D.U i).toPresheafedSpace) : Prop

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

Equations

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

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

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

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

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

Equations

• D.openCover = { J := D.J, obj := D.U, map := D.ι, f := fun (x : ↑↑D.glued.toPresheafedSpace) => ⋯.choose, covers := ⋯, map_prop := ⋯ }

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

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

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

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

def AlgebraicGeometry.Scheme.Cover.gluedCoverT' {X : AlgebraicGeometry.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.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj z ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.obj x ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x) (AlgebraicGeometry.Scheme.Cover.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 : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : AlgebraicGeometry.Scheme.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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Cover.fromGlued {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : (AlgebraicGeometry.Scheme.Cover.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.

@[simp]

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

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

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

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

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

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

@[deprecated AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding (since := "2024-10-18")]

theorem AlgebraicGeometry.Scheme.Cover.fromGlued_openEmbedding {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : Topology.IsOpenEmbedding ⇑(AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰).base

Alias of AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding.

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

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

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

def AlgebraicGeometry.Scheme.Cover.glueMorphisms {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.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.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.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) (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) = f x

theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.map x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) h) = CategoryTheory.CategoryStruct.comp (f x) h

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