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.

source

structure AlgebraicGeometry.Scheme.GlueDataextends CategoryTheory.GlueData :

Type (u_1 + 1)

A family of gluing data consists of

An index type J
A scheme U i for each i : J.
A scheme V i j for each i j : J. (Note that this is J × J → Scheme rather than J → J → Scheme to connect to the limits library easier.)
An open immersion f i j : V i j ⟶ U i for each i j : ι.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
f i i is an isomorphism.
t i i is the identity.
V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the schemes U i together by identifying V i j with V j i, such that the U i's are open subschemes of the glued space.

J : Type u_1
U : self.J → AlgebraicGeometry.Scheme
V : self.J × self.J → AlgebraicGeometry.Scheme
f : (i j : self.J) → self.V (i, j) ⟶ self.U i
f_mono : ∀ (i j : self.J), 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)

Instances For

source

theorem AlgebraicGeometry.Scheme.GlueData.f_open (self : AlgebraicGeometry.Scheme.GlueData) (i : self.J) (j : self.J) :

AlgebraicGeometry.IsOpenImmersion (self.f i j)

source

@[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 := ⋯ }

Instances For

source

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

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

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i)

Equations

⋯ = ⋯

source

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 ⋯

Instances For

source

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.

source

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.

source

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

CategoryTheory.Limits.HasMulticoequalizer D.diagram

Equations

⋯ = ⋯

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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)

source

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

AlgebraicGeometry.IsOpenImmersion (D.ι i)

Equations

⋯ = ⋯

source

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

source

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

source

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)

source

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

Instances For

source

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)

Instances For

source

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.

Instances For

source

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

source

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.

Instances For

source

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).base x = (D.ι j).base y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

source

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)

source

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

Instances For

source

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

D.openCover.map i = D.ι i

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_f (D : AlgebraicGeometry.Scheme.GlueData) (x : ↑↑D.glued.toPresheafedSpace) :

D.openCover.f x = ⋯.choose

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_obj (D : AlgebraicGeometry.Scheme.GlueData) :

∀ (a : D.J), D.openCover.obj a = D.U a

source

theorem AlgebraicGeometry.Scheme.GlueData.openCover_J (D : AlgebraicGeometry.Scheme.GlueData) :

D.openCover.J = D.J

source

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.

Instances For

source

@[simp]

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

source

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

source

@[simp]

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

source

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

source

@[simp]

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

source

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

source

@[simp]

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

source

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

source

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

source

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

source

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

source

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.

Instances For

source

@[simp]

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

∀ (a : 𝒰.J), 𝒰.gluedCover.U a = 𝒰.obj a

source

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

source

@[simp]

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

𝒰.gluedCover.J = 𝒰.J

source

@[simp]

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

∀ (x x_1 : 𝒰.J), 𝒰.gluedCover.t x x_1 = (CategoryTheory.Limits.pullbackSymmetry (𝒰.map x) (𝒰.map x_1)).hom

source

@[simp]

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

∀ (x x_1 : 𝒰.J), 𝒰.gluedCover.f x x_1 = CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map x_1)

source

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

source

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J) :

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

source

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

source

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

Function.Injective ⇑𝒰.fromGlued.base

source

instance AlgebraicGeometry.Scheme.OpenCover.fromGlued_stalk_iso {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : ↑↑𝒰.gluedCover.glued.toPresheafedSpace) :

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

Equations

⋯ = ⋯

source

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

IsOpenMap ⇑𝒰.fromGlued.base

source

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

IsOpenEmbedding ⇑𝒰.fromGlued.base

source

@[deprecated AlgebraicGeometry.Scheme.OpenCover.fromGlued_isOpenEmbedding]

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

IsOpenEmbedding ⇑𝒰.fromGlued.base

Alias of AlgebraicGeometry.Scheme.OpenCover.fromGlued_isOpenEmbedding.

source

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

CategoryTheory.Epi 𝒰.fromGlued.base

Equations

⋯ = ⋯

source

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

AlgebraicGeometry.IsOpenImmersion 𝒰.fromGlued

Equations

⋯ = ⋯

source

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

CategoryTheory.IsIso 𝒰.fromGlued

Equations

⋯ = ⋯

source

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

Instances For

source

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

source

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

source

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₂

Documentation

Mathlib.AlgebraicGeometry.Gluing

Gluing Schemes #

Main definitions #

Main results #

Implementation details #