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 : 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 = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (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)

@[inline, reducible]

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionULocallyRingedSpaceInstCategoryLocallyRingedSpaceToGlueDataToLocallyRingedSpaceGlueDataGluedHasColimitOfHasColimitsOfShapeWalkingMultispanLDiagramRFstFromSndFromInstSmallCategoryWalkingMultispanHasColimitsOfShapeOfHasColimitsOfSizeInstHasColimitsLocallyRingedSpaceInstCategoryLocallyRingedSpaceMultispanι (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (CategoryTheory.GlueData.ι (AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData D).toGlueData i)

Equations

• ⋯ = ⋯

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

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

instance AlgebraicGeometry.Scheme.GlueData.instCreatesColimitSchemeInstCategorySchemeLocallyRingedSpaceInstCategoryLocallyRingedSpaceWalkingMultispanLDiagramToGlueDataRFstFromSndFromInstSmallCategoryWalkingMultispanMultispanForgetToLocallyRingedSpace (D : AlgebraicGeometry.Scheme.GlueData) : CategoryTheory.CreatesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D.toGlueData)) AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

Equations

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

instance AlgebraicGeometry.Scheme.GlueData.instPreservesColimitSchemeInstCategorySchemeTopCatInstTopCatLargeCategoryWalkingMultispanLDiagramToGlueDataRFstFromSndFromInstSmallCategoryWalkingMultispanMultispanForgetToTop (D : AlgebraicGeometry.Scheme.GlueData) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D.toGlueData)) AlgebraicGeometry.Scheme.forgetToTop

Equations

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

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

Equations

• ⋯ = ⋯

@[inline, reducible]

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

The glued scheme of a glued space.

Equations

• AlgebraicGeometry.Scheme.GlueData.glued D = CategoryTheory.GlueData.glued D.toGlueData

@[inline, reducible]

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

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

Equations

• AlgebraicGeometry.Scheme.GlueData.ι D i = CategoryTheory.GlueData.ι D.toGlueData i

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace (D : AlgebraicGeometry.Scheme.GlueData) : (AlgebraicGeometry.Scheme.GlueData.glued D).toLocallyRingedSpace ≅ CategoryTheory.GlueData.glued (AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData D).toGlueData

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

Equations

• AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace D = CategoryTheory.GlueData.gluedIso D.toGlueData AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition_assoc (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (j : D.J) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Scheme.GlueData.glued D ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.GlueData.ι D j) h)) = CategoryTheory.CategoryStruct.comp (D.f i j) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.GlueData.ι D i) h)

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.glue_condition (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (j : D.J) : CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (AlgebraicGeometry.Scheme.GlueData.ι D j)) = CategoryTheory.CategoryStruct.comp (D.f i j) (AlgebraicGeometry.Scheme.GlueData.ι D i)

def AlgebraicGeometry.Scheme.GlueData.vPullbackCone (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (j : D.J) : CategoryTheory.Limits.PullbackCone (AlgebraicGeometry.Scheme.GlueData.ι D i) (AlgebraicGeometry.Scheme.GlueData.ι 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

• AlgebraicGeometry.Scheme.GlueData.vPullbackCone D 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 : D.J) (j : D.J) : CategoryTheory.Limits.IsLimit (AlgebraicGeometry.Scheme.GlueData.vPullbackCone D 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

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

def AlgebraicGeometry.Scheme.GlueData.isoCarrier (D : AlgebraicGeometry.Scheme.GlueData) : ↑(AlgebraicGeometry.Scheme.GlueData.glued D).toPresheafedSpace ≅ CategoryTheory.GlueData.glued (AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData (AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData (AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData (AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData D)))).toGlueData

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 (CategoryTheory.GlueData.ι (AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData (AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData (AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData (AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData D)))).toGlueData i) (AlgebraicGeometry.Scheme.GlueData.isoCarrier D).inv = (AlgebraicGeometry.Scheme.GlueData.ι D i).val.base

def AlgebraicGeometry.Scheme.GlueData.Rel (D : AlgebraicGeometry.Scheme.GlueData) (a : (i : D.J) × ↑↑(D.U i).toPresheafedSpace) (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 : D.J) (j : D.J) (x : ↑↑(D.U i).toPresheafedSpace) (y : ↑↑(D.U j).toPresheafedSpace) : (CategoryTheory.GlueData.ι D.toGlueData i).val.base x = (CategoryTheory.GlueData.ι D.toGlueData j).val.base y ↔ AlgebraicGeometry.Scheme.GlueData.Rel D { fst := i, snd := x } { fst := j, snd := y }

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

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

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

Equations

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_U {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : ∀ (a : 𝒰.J), (AlgebraicGeometry.Scheme.OpenCover.gluedCover 𝒰).U a = 𝒰.obj a

@[simp]

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

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

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

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_openEmbedding {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : OpenEmbedding ⇑(AlgebraicGeometry.Scheme.OpenCover.fromGlued 𝒰).val.base

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Given an open cover of X, and a morphism 𝒰.obj x ⟶ Y for each open subscheme in the cover, such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms together into a morphism X ⟶ Y.

Note: If X is exactly (defeq to) the gluing of U i, then using Multicoequalizer.desc suffices.

Equations

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

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

@[simp]

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

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