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.

instance AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion : IsOpenImmersion.HasPullbacks

@[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.instIsOpenImmersionF {X : Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀) : IsOpenImmersion (𝒰.f i)

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

The affine cover of a scheme.

@[implicit_reducible]

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

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

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

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

noncomputable 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_X {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose) : 𝒰.finiteSubcover.X x = 𝒰.X (Cover.idx 𝒰 ↑x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] (x : ↥⋯.choose) : 𝒰.finiteSubcover.f x = 𝒰.f (Cover.idx 𝒰 ↑x)

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instFintypeI₀FiniteSubcover {X : Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↥X] : Fintype 𝒰.finiteSubcover.I₀

theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace {X : Scheme} (𝒰 : X.OpenCover) [Finite 𝒰.I₀] [H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X 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.instIsOpenImmersionF {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : IsOpenImmersion (𝒰.f j)

noncomputable 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_X {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : 𝒰.openCover.X j = Spec (𝒰.X j)

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀ {X : Scheme} (𝒰 : X.AffineOpenCover) : 𝒰.openCover.I₀ = 𝒰.I₀

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f {X : Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀) : 𝒰.openCover.f j = 𝒰.f j

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

A choice of an affine open cover of a scheme.

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_f (X : Scheme) (i : X.affineCover.I₀) : X.affineOpenCover.f i = X.affineCover.f i

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_I₀ (X : Scheme) : X.affineOpenCover.I₀ = X.affineCover.I₀

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_X (X : Scheme) (x : ↑X.toTopCat) : X.affineOpenCover.X x = Classical.choose ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.affineOpenCover_idx (X : Scheme) (x : ↥X) : X.affineOpenCover.idx x = ⋯.choose

@[simp]

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

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

noncomputable def AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i ≅ (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).X 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 : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd) ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst) h)

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (Cover.pullbackHom 𝒰.affineRefinement.openCover f i) = Cover.pullbackHom (𝒰.X 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 : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) {Z : Scheme} (h : 𝒰.affineRefinement.openCover.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv (CategoryTheory.CategoryStruct.comp (Cover.pullbackHom 𝒰.affineRefinement.openCover f i) h) = CategoryTheory.CategoryStruct.comp (Cover.pullbackHom (𝒰.X 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 an affine open cover of Spec R.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable 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 : 𝒰.I₀), (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.f 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 : 𝒰.I₀), (CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.f 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 𝒰.I₀] (h : ∀ (i : 𝒰.I₀), IsNilpotent ((CategoryTheory.ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s)) : IsNilpotent s

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

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

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

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

noncomputable def AlgebraicGeometry.Scheme.affineBasisCoverRing (X : Scheme) (i : X.affineBasisCover.I₀) : CommRingCat

The coordinate ring of a component in the affine_basis_cover.

theorem AlgebraicGeometry.Scheme.affineBasisCover_obj (X : Scheme) (i : X.affineBasisCover.I₀) : X.affineBasisCover.X i = Spec (X.affineBasisCoverRing i)

theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range (X : Scheme) (x : ↥X) (r : ↑⋯.choose) : Set.range ⇑(X.affineBasisCover.f ⟨x, r⟩) = ⇑(X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).carrier

theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis (X : Scheme) : TopologicalSpace.IsTopologicalBasis {x : Set ↥X | ∃ (a : X.affineBasisCover.I₀), x = Set.range ⇑(X.affineBasisCover.f a)}