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.

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.

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

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

theorem AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange {X : Scheme} (𝒰 : X.OpenCover) : TopologicalSpace.IsOpenCover fun (i : 𝒰.J) => Hom.opensRange (𝒰.map i)

The ranges of the maps in a scheme-theoretic open cover are a topological open cover.

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

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

@[simp]

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

@[simp]

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

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

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

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

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.

@[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_J {X : Scheme} (𝒰 : X.AffineOpenCover) : 𝒰.openCover.J = 𝒰.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) : 𝒰.openCover.f x = 𝒰.f x

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

A choice of an affine open cover of a scheme.

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

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.

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.

@[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_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 = ι

@[simp]

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

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

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

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.

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.

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

The coordinate ring of a component in the affine_basis_cover.

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) (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 | ∃ (a : X.affineBasisCover.J), x = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.affineBasisCover.map a).base)}