Open covers of schemes

This file provides the basic API for open covers of schemes.

Main definition

• AlgebraicGeometry.Scheme.OpenCover: The type of open covers of a scheme X, consisting of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.
• AlgebraicGeometry.Scheme.affineCover: X.affineCover is a choice of an affine cover of X.
• AlgebraicGeometry.Scheme.AffineOpenCover: The type of affine open covers of a scheme X.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.OpenCover (X : Scheme) : Type (max (v + 1) (u + 1))

An open cover of a scheme X is a cover where all component maps are open immersions.

Equations

• X.OpenCover = AlgebraicGeometry.Scheme.Cover (@AlgebraicGeometry.IsOpenImmersion) X

@[deprecated AlgebraicGeometry.Scheme.Cover.map_prop (since := "2024-11-06")]

theorem AlgebraicGeometry.Scheme.OpenCover.IsOpen {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (self : Cover P X) (j : self.J) : P (self.map j)

Alias of AlgebraicGeometry.Scheme.Cover.map_prop.

---

the component maps satisfy P

instance AlgebraicGeometry.Scheme.instIsOpenImmersionMap {X : Scheme} (𝒰 : X.OpenCover) (i : 𝒰.J) : IsOpenImmersion (𝒰.map i)

def AlgebraicGeometry.Scheme.affineCover (X : Scheme) : X.OpenCover

The affine cover of a scheme.

Equations

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

instance AlgebraicGeometry.Scheme.instInhabitedOpenCover {X : Scheme} : Inhabited X.OpenCover

Equations

• AlgebraicGeometry.Scheme.instInhabitedOpenCover = { default := X.affineCover }

theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange {X : Scheme} (𝒰 : X.OpenCover) : ⨆ (i : 𝒰.J), Hom.opensRange (𝒰.map i) = ⊤

def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↑↑X.toPresheafedSpace] : X.OpenCover

Every open cover of a quasi-compact scheme can be refined into a finite subcover.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_map {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↑↑X.toPresheafedSpace] (x : { x : ↑↑X.toPresheafedSpace // x ∈ ⋯.choose }) : 𝒰.finiteSubcover.map x = 𝒰.map (𝒰.f ↑x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_obj {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↑↑X.toPresheafedSpace] (x : { x : ↑↑X.toPresheafedSpace // x ∈ ⋯.choose }) : 𝒰.finiteSubcover.obj x = 𝒰.obj (𝒰.f ↑x)

instance AlgebraicGeometry.Scheme.instFintypeJIsOpenImmersionFiniteSubcover {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↑↑X.toPresheafedSpace] : Fintype 𝒰.finiteSubcover.J

Equations

• AlgebraicGeometry.Scheme.instFintypeJIsOpenImmersionFiniteSubcover 𝒰 = id inferInstance

theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace {X : Scheme} (𝒰 : X.OpenCover) [Finite 𝒰.J] [H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace] : CompactSpace ↑↑X.toPresheafedSpace

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.AffineOpenCover (X : Scheme) : Type (max (v + 1) (u + 1))

An affine open cover of X consists of a family of open immersions into X from spectra of rings.

Equations

• X.AffineOpenCover = AlgebraicGeometry.Scheme.AffineCover (@AlgebraicGeometry.IsOpenImmersion) X

instance AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionMap {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.J) : IsOpenImmersion (𝒰.map j)

def AlgebraicGeometry.Scheme.AffineOpenCover.openCover {X : Scheme} (𝒰 : X.AffineOpenCover) : X.OpenCover

The open cover associated to an affine open cover.

Equations

• 𝒰.openCover = AlgebraicGeometry.Scheme.AffineCover.cover 𝒰

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_obj {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.J) : 𝒰.openCover.obj j = Spec (𝒰.obj j)

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_map {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.J) : 𝒰.openCover.map j = 𝒰.map j

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f {X : Scheme} (𝒰 : X.AffineOpenCover) (x : ↑↑X.toPresheafedSpace) : 𝒰.openCover.f x = 𝒰.f x

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_J {X : Scheme} (𝒰 : X.AffineOpenCover) : 𝒰.openCover.J = 𝒰.J

def AlgebraicGeometry.Scheme.affineOpenCover (X : Scheme) : X.AffineOpenCover

A choice of an affine open cover of a scheme.

Equations

• X.affineOpenCover = { J := X.affineCover.J, obj := fun (j : X.affineCover.J) => ⋯.choose, map := X.affineCover.map, f := X.affineCover.f, covers := ⋯, map_prop := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_map (X : Scheme) (j : X.affineCover.J) : X.affineOpenCover.map j = X.affineCover.map j

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_obj (X : Scheme) (j : X.affineCover.J) : X.affineOpenCover.obj j = ⋯.choose

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_J (X : Scheme) : X.affineOpenCover.J = X.affineCover.J

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_f (X : Scheme) (x : ↑↑X.toPresheafedSpace) : X.affineOpenCover.f x = X.affineCover.f x

@[simp]

theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover (X : Scheme) : X.affineOpenCover.openCover = X.affineCover

def AlgebraicGeometry.Scheme.OpenCover.affineRefinement {X : Scheme} (𝓤 : X.OpenCover) : X.AffineOpenCover

Given any open cover 𝓤, this is an affine open cover which refines it. The morphism in the category of open covers which proves that this is indeed a refinement, see AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement.

Equations

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

def AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).obj i ≅ (Cover.pullbackCover (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst)).obj i.snd

The pullback of the affine refinement is the pullback of the affine cover.

Equations

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

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ((Cover.pullbackCover 𝒰.affineRefinement.openCover f).map i) = CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst)).map i.snd) ((Cover.pullbackCover 𝒰 f).map i.fst)

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover 𝒰.affineRefinement.openCover f).map i) h) = CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst)).map i.snd) (CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover 𝒰 f).map i.fst) h)

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (Cover.pullbackHom 𝒰.affineRefinement.openCover f i) = Cover.pullbackHom (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst) i.snd

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) {Z : Scheme} (h : 𝒰.affineRefinement.openCover.obj i ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp (Cover.pullbackHom 𝒰.affineRefinement.openCover f i) h) = CategoryTheory.CategoryStruct.comp (Cover.pullbackHom (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst) i.snd) h

noncomputable def AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) : (Spec R).AffineOpenCover

A family of elements spanning the unit ideal of R gives a affine open cover of Spec R.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_map {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι) : (affineOpenCoverOfSpanRangeEqTop s hs).map i = Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (s i))))

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (x : ↑↑(Spec R).toPresheafedSpace) : (affineOpenCoverOfSpanRangeEqTop s hs).f x = let_fun this := ⋯; this.choose

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_obj_carrier {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι) : ↑((affineOpenCoverOfSpanRangeEqTop s hs).obj i) = Localization.Away (s i)

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_J {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) : (affineOpenCoverOfSpanRangeEqTop s hs).J = ι

def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement {X : Scheme} (𝓤 : X.OpenCover) : 𝓤.affineRefinement.openCover ⟶ 𝓤

Given any open cover 𝓤, this is an affine open cover which refines it.

Equations

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

theorem AlgebraicGeometry.Scheme.OpenCover.ext_elem {X : Scheme} {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.map i) U)) f = (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.map i) U)) g) : f = g

If two global sections agree after restriction to each member of an open cover, then they agree globally.

theorem AlgebraicGeometry.Scheme.zero_of_zero_cover {X : Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s = 0) : s = 0

If the restriction of a global section to each member of an open cover is zero, then it is globally zero.

theorem AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover {X : Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) [Finite 𝒰.J] (h : ∀ (i : 𝒰.J), IsNilpotent ((CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.map i) U)) s)) : IsNilpotent s

If a global section is nilpotent on each member of a finite open cover, then f is nilpotent.

def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine (R : CommRingCat) : (Spec R).OpenCover

The basic open sets form an affine open cover of Spec R.

Equations

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

def AlgebraicGeometry.Scheme.affineBasisCover (X : Scheme) : X.OpenCover

We may bind the basic open sets of an open affine cover to form an affine cover that is also a basis.

Equations

• X.affineBasisCover = AlgebraicGeometry.Scheme.Cover.bind X.affineCover fun (x : X.affineCover.J) => AlgebraicGeometry.Scheme.affineBasisCoverOfAffine ⋯.choose

def AlgebraicGeometry.Scheme.affineBasisCoverRing (X : Scheme) (i : X.affineBasisCover.J) : CommRingCat

The coordinate ring of a component in the affine_basis_cover.

Equations

• X.affineBasisCoverRing i = CommRingCat.of (Localization.Away i.snd)

theorem AlgebraicGeometry.Scheme.affineBasisCover_obj (X : Scheme) (i : X.affineBasisCover.J) : X.affineBasisCover.obj i = Spec (X.affineBasisCoverRing i)

theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range (X : Scheme) (x : ↑↑X.toPresheafedSpace) (r : ↑⋯.choose) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.affineBasisCover.map ⟨x, r⟩).base) = ⇑(CategoryTheory.ConcreteCategory.hom (X.affineCover.map x).base) '' (PrimeSpectrum.basicOpen r).carrier

theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis (X : Scheme) : TopologicalSpace.IsTopologicalBasis {x : Set ↑↑X.toPresheafedSpace | ∃ (a : X.affineBasisCover.J), x = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.affineBasisCover.map a).base)}