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.

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

An open cover of X consists of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.

This is merely a coverage in the Zariski pretopology, and it would be optimal if we could reuse the existing API about pretopologies, However, the definitions of sieves and grothendieck topologies uses Props, so that the actual open sets and immersions are hard to obtain. Also, since such a coverage in the pretopology usually contains a proper class of immersions, it is quite hard to glue them, reason about finite covers, etc.

• J : Type v

  index set of an open cover of a scheme X

• obj : self.J → AlgebraicGeometry.Scheme

  the subschemes of an open cover

• map : (j : self.J) → self.obj j ⟶ X

  the embedding of subschemes to X

• f : ↑↑X.toPresheafedSpace → self.J

  given a point of x : X, f x is the index of the subscheme which contains x

• covers : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(self.map (self.f x)).base

  the subschemes covers X

• IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

  the embedding of subschemes are open immersions

theorem AlgebraicGeometry.Scheme.OpenCover.covers {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : ↑↑X.toPresheafedSpace) : x ∈ Set.range ⇑(self.map (self.f x)).base

the subschemes covers X

theorem AlgebraicGeometry.Scheme.OpenCover.IsOpen {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : self.J) : AlgebraicGeometry.IsOpenImmersion (self.map x)

the embedding of subschemes are open immersions

@[deprecated AlgebraicGeometry.Scheme.OpenCover.covers]

theorem AlgebraicGeometry.Scheme.OpenCover.Covers {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : ↑↑X.toPresheafedSpace) : x ∈ Set.range ⇑(self.map (self.f x)).base

Alias of AlgebraicGeometry.Scheme.OpenCover.covers.

---

the subschemes covers X

def AlgebraicGeometry.Scheme.affineCover (X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} : Inhabited X.OpenCover

Equations

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

theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : ⋃ (i : 𝒰.J), Set.range ⇑(𝒰.map i).base = Set.univ

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

def AlgebraicGeometry.Scheme.OpenCover.bind {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) : X.OpenCover

Given an open cover { Uᵢ } of X, and for each Uᵢ an open cover, we may combine these open covers to form an open cover of X.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) : (𝒰.bind f).J = ((i : 𝒰.J) × (f i).J)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J) : (𝒰.bind f).map x = CategoryTheory.CategoryStruct.comp ((f x.fst).map x.snd) (𝒰.map x.fst)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.bind_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J) : (𝒰.bind f).obj x = (f x.fst).obj x.snd

def AlgebraicGeometry.Scheme.openCoverOfIsIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : Y.OpenCover

An isomorphism X ⟶ Y is an open cover of Y.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : PUnit.{v + 1} ), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).map x = f

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (AlgebraicGeometry.Scheme.openCoverOfIsIso f).J = PUnit.{v + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.openCoverOfIsIso_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : PUnit.{v + 1} ), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).obj x = X

def AlgebraicGeometry.Scheme.OpenCover.copy {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : X.OpenCover

We construct an open cover from another, by providing the needed fields and showing that the provided fields are isomorphic with the original open cover.

Equations

• 𝒰.copy J obj map e₁ e₂✝ e₂ = { J := J, obj := obj, map := map, f := fun (x : ↑↑X.toPresheafedSpace) => e₁.symm (𝒰.f x), covers := ⋯, IsOpen := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : ∀ (a : J), (𝒰.copy J obj map e₁ e₂✝ e₂).obj a = obj a

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) (i : J) : (𝒰.copy J obj map e₁ e₂✝ e₂).map i = map i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.copy_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) : (𝒰.copy J obj map e₁ e₂✝ e₂).J = J

def AlgebraicGeometry.Scheme.OpenCover.pushforwardIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [CategoryTheory.IsIso f] : Y.OpenCover

The pushforward of an open cover along an isomorphism.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : 𝒰.J), (𝒰.pushforwardIso f).obj x = 𝒰.obj x

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [CategoryTheory.IsIso f] : (𝒰.pushforwardIso f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Y) [CategoryTheory.IsIso f] : ∀ (x : 𝒰.J), (𝒰.pushforwardIso f).map x = CategoryTheory.CategoryStruct.comp (𝒰.map x) f

def AlgebraicGeometry.Scheme.OpenCover.add {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] : X.OpenCover

Adding an open immersion into an open cover gives another open cover.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] : (𝒰.add f).J = Option 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) : (𝒰.add f).map i = Option.rec f 𝒰.map i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) : (𝒰.add f).obj i = Option.rec Y 𝒰.obj i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.add_f {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace) : (𝒰.add f).f x = some (𝒰.f x)

def AlgebraicGeometry.Scheme.OpenCover.pullbackCover {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : W.OpenCover

Given an open cover on X, we may pull them back along a morphism W ⟶ X to obtain an open cover of W.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_obj {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J) : (𝒰.pullbackCover f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_J {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : (𝒰.pullbackCover f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_f {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace) : (𝒰.pullbackCover f).f x = 𝒰.f (f.base x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_map {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : ∀ (x : 𝒰.J), (𝒰.pullbackCover f).map x = CategoryTheory.Limits.pullback.fst f (𝒰.map x)

def AlgebraicGeometry.Scheme.OpenCover.pullbackHom {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (i : (𝒰.pullbackCover f).J) : (𝒰.pullbackCover f).obj i ⟶ 𝒰.obj i

The family of morphisms from the pullback cover to the original cover.

Equations

• 𝒰.pullbackHom f i = CategoryTheory.Limits.pullback.snd f (𝒰.map i)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackHom_map {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (i : (𝒰.pullbackCover f).J) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (𝒰.map i) = CategoryTheory.CategoryStruct.comp ((𝒰.pullbackCover f).map i) f

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackHom_map_assoc {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (i : (𝒰.pullbackCover f).J) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.map i) h) = CategoryTheory.CategoryStruct.comp ((𝒰.pullbackCover f).map i) (CategoryTheory.CategoryStruct.comp f h)

def AlgebraicGeometry.Scheme.OpenCover.pullbackCover' {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : W.OpenCover

Given an open cover on X, we may pull them back along a morphism f : W ⟶ X to obtain an open cover of W. This is similar to Scheme.OpenCover.pullbackCover, but here we take pullback (𝒰.map x) f instead of pullback f (𝒰.map x).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_obj {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : 𝒰.J) : (𝒰.pullbackCover' f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_f {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) (x : ↑↑W.toPresheafedSpace) : (𝒰.pullbackCover' f).f x = 𝒰.f (f.base x)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_J {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : (𝒰.pullbackCover' f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_map {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W ⟶ X) : ∀ (x : 𝒰.J), (𝒰.pullbackCover' f).map x = CategoryTheory.Limits.pullback.snd (𝒰.map x) f

def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover {X : AlgebraicGeometry.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_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace ↑↑X.toPresheafedSpace] (x : { x : ↑↑X.toPresheafedSpace // x ∈ ⋯.choose }) : 𝒰.finiteSubcover.obj x = 𝒰.obj (𝒰.f ↑x)

@[simp]

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

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

Equations

• AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover 𝒰 = id inferInstance

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

def AlgebraicGeometry.Scheme.OpenCover.inter {X : AlgebraicGeometry.Scheme} (𝒰₁ : X.OpenCover) (𝒰₂ : X.OpenCover) : X.OpenCover

Given open covers { Uᵢ } and { Uⱼ }, we may form the open cover { Uᵢ ∩ Uⱼ }.

Equations

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

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

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

• J : Type v

  index set of an affine open cover of a scheme X

• obj : self.J → CommRingCat

  the ring associated to a component of an affine open cover

• map : (j : self.J) → AlgebraicGeometry.Spec (self.obj j) ⟶ X

  the embedding of subschemes to X

• f : ↑↑X.toPresheafedSpace → self.J

  given a point of x : X, f x is the index of the subscheme which contains x

• covers : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ Set.range ⇑(self.map (self.f x)).base

  the subschemes covers X

• IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

  the embedding of subschemes are open immersions

theorem AlgebraicGeometry.Scheme.AffineOpenCover.covers {X : AlgebraicGeometry.Scheme} (self : X.AffineOpenCover) (x : ↑↑X.toPresheafedSpace) : x ∈ Set.range ⇑(self.map (self.f x)).base

the subschemes covers X

theorem AlgebraicGeometry.Scheme.AffineOpenCover.IsOpen {X : AlgebraicGeometry.Scheme} (self : X.AffineOpenCover) (x : self.J) : AlgebraicGeometry.IsOpenImmersion (self.map x)

the embedding of subschemes are open immersions

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

The open cover associated to an affine open cover.

Equations

• 𝓤.openCover = { J := 𝓤.J, obj := fun (j : 𝓤.J) => AlgebraicGeometry.Spec (𝓤.obj j), map := 𝓤.map, f := 𝓤.f, covers := ⋯, IsOpen := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) : ∀ (a : ↑↑X.toPresheafedSpace), 𝓤.openCover.f a = 𝓤.f a

@[simp]

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

def AlgebraicGeometry.Scheme.affineOpenCover (X : AlgebraicGeometry.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 := ⋯, IsOpen := ⋯ }

@[simp]

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

def AlgebraicGeometry.Scheme.OpenCover.affineRefinement {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (𝒰.affineRefinement.openCover.pullbackCover f).J) : (𝒰.affineRefinement.openCover.pullbackCover f).obj i ≅ ((𝒰.obj i.fst).affineCover.pullbackCover (𝒰.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (𝒰.affineRefinement.openCover.pullbackCover f).J) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ((𝒰.affineRefinement.openCover.pullbackCover f).map i) = CategoryTheory.CategoryStruct.comp (((𝒰.obj i.fst).affineCover.pullbackCover (𝒰.pullbackHom f i.fst)).map i.snd) ((𝒰.pullbackCover f).map i.fst)

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

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

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

structure AlgebraicGeometry.Scheme.OpenCover.Hom {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (𝓥 : X.OpenCover) : Type (max u v)

A morphism between open covers 𝓤 ⟶ 𝓥 indicates that 𝓤 is a refinement of 𝓥. Since open covers of schemes are indexed, the definition also involves a map on the indexing types.

• idx : 𝓤.J → 𝓥.J

  The map on indexing types associated to a morphism of open covers.

• app : (j : 𝓤.J) → 𝓤.obj j ⟶ 𝓥.obj (self.idx j)

  The morphism between open subsets associated to a morphism of open covers.

• isOpen : ∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (self.app j)
• w : ∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j

theorem AlgebraicGeometry.Scheme.OpenCover.Hom.isOpen {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) : AlgebraicGeometry.IsOpenImmersion (self.app j)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.Hom.w {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) : CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.Hom.w_assoc {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app j) (CategoryTheory.CategoryStruct.comp (𝓥.map (self.idx j)) h) = CategoryTheory.CategoryStruct.comp (𝓤.map j) h

def AlgebraicGeometry.Scheme.OpenCover.Hom.id {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) : 𝓤.Hom 𝓤

The identity morphism in the category of open covers of a scheme.

Equations

• AlgebraicGeometry.Scheme.OpenCover.Hom.id 𝓤 = { idx := fun (j : 𝓤.J) => j, app := fun (x : 𝓤.J) => CategoryTheory.CategoryStruct.id (𝓤.obj x), isOpen := ⋯, w := ⋯ }

def AlgebraicGeometry.Scheme.OpenCover.Hom.comp {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤.Hom 𝓥) (g : 𝓥.Hom 𝓦) : 𝓤.Hom 𝓦

The composition of two morphisms in the category of open covers of a scheme.

Equations

• f.comp g = { idx := fun (j : 𝓤.J) => g.idx (f.idx j), app := fun (x : 𝓤.J) => CategoryTheory.CategoryStruct.comp (f.app x) (g.app (f.idx x)), isOpen := ⋯, w := ⋯ }

instance AlgebraicGeometry.Scheme.OpenCover.category {X : AlgebraicGeometry.Scheme} : CategoryTheory.Category.{max u v, max (v + 1) (u + 1)} X.OpenCover

Equations

• AlgebraicGeometry.Scheme.OpenCover.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.id_idx_apply {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.id 𝓤).idx j = j

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.id_app {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.id 𝓤).app j = CategoryTheory.CategoryStruct.id (𝓤.obj j)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.comp f g).idx j = g.idx (f.idx j)

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.comp_app {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤 ⟶ 𝓥) (g : 𝓥 ⟶ 𝓦) (j : 𝓤.J) : (CategoryTheory.CategoryStruct.comp f g).app j = CategoryTheory.CategoryStruct.comp (f.app j) (g.app (f.idx j))

def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) f = (AlgebraicGeometry.Scheme.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) [Finite 𝒰.J] (h : ∀ (i : 𝒰.J), IsNilpotent ((AlgebraicGeometry.Scheme.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) : (AlgebraicGeometry.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 : AlgebraicGeometry.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 = X.affineCover.bind fun (x : X.affineCover.J) => AlgebraicGeometry.Scheme.affineBasisCoverOfAffine ⋯.choose

def AlgebraicGeometry.Scheme.affineBasisCoverRing (X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.J) : X.affineBasisCover.obj i = AlgebraicGeometry.Spec (X.affineBasisCoverRing i)

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

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