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

theorem AlgebraicGeometry.Scheme.GlueData.f_open (self : AlgebraicGeometry.Scheme.GlueData) (i : self.J) (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 : D.J) (j : D.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι 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

• 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

Equations

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

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

Equations

• ⋯ = ⋯

@[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 = D.ι i

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective (D : AlgebraicGeometry.Scheme.GlueData) (x : ↑↑D.glued.toPresheafedSpace) : ∃ (i : D.J) (y : ↑↑(D.U i).toPresheafedSpace), (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 : 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)

@[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) (D.ι j)) = CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)

def AlgebraicGeometry.Scheme.GlueData.vPullbackCone (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) (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 : D.J) (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).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) : (D.ι i).val.base x = (D.ι j).val.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).val.base ⁻¹' U)

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

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

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 := ⋯, IsOpen := ⋯ }

def AlgebraicGeometry.Scheme.OpenCover.gluedCoverT' {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.

theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.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.OpenCover.gluedCoverT'_fst_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.gluedCoverT'_fst_snd_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.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.OpenCover.gluedCoverT'_fst_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.gluedCoverT'_snd_fst_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.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.OpenCover.gluedCoverT'_snd_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.gluedCoverT'_snd_snd_assoc {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (z : 𝒰.J) {Z : AlgebraicGeometry.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)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.glued_cover_cocycle_fst {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.glued_cover_cocycle_snd {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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.OpenCover.glued_cover_cocycle {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) (y : 𝒰.J) (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)))

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.gluedCover_V {X : AlgebraicGeometry.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.OpenCover.gluedCover_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : 𝒰.gluedCover.J = 𝒰.J

@[simp]

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

@[simp]

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

@[simp]

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

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

def AlgebraicGeometry.Scheme.OpenCover.fromGlued {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : 𝒰.gluedCover.glued ⟶ X

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

Equations

• 𝒰.fromGlued = CategoryTheory.Limits.Multicoequalizer.desc 𝒰.gluedCover.diagram X (fun (x : 𝒰.gluedCover.diagram.R) => 𝒰.map x) ⋯

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• 𝒰.glueMorphisms f hf = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv 𝒰.fromGlued) (CategoryTheory.Limits.Multicoequalizer.desc 𝒰.gluedCover.diagram Y f ⋯)

theorem AlgebraicGeometry.Scheme.OpenCover.ι_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 (𝒰.glueMorphisms f hf) h) = CategoryTheory.CategoryStruct.comp (f x) h

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.ι_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) (𝒰.glueMorphisms f hf) = f x

theorem AlgebraicGeometry.Scheme.OpenCover.hom_ext {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {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₂