AlgebraicGeometry.ProjSpace.stdCover
The standard ordered affine cover of projective space by the coordinate basic opens.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjSpace
section StdCover
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) RLean source · full declaration
def stdCover : Scheme.OrderedAffineCover.{u} (Proj 𝒜) where
ι := ULift.{u} (Fin (n + 1))
U j := AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j.down)
isAffineOpen j := AlgebraicGeometry.Proj.isAffineOpen_basicOpen 𝒜 (MvPolynomial.X j.down)
((MvPolynomial.mem_homogeneousSubmodule 1 _).mpr (MvPolynomial.isHomogeneous_X R j.down))
one_pos
iSup_eq_top := by
have key : (⨆ j : ULift.{u} (Fin (n + 1)),
AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j.down))
= ⨆ j : Fin (n + 1), AlgebraicGeometry.Proj.basicOpen 𝒜 (MvPolynomial.X j) := by
refine le_antisymm (iSup_le fun j => ?_) (iSup_le fun j => ?_)
· exact le_iSup (fun j' : Fin (n + 1) => AlgebraicGeometry.Proj.basicOpen 𝒜 (X j')) j.down
· exact le_iSup (fun j' : ULift.{u} (Fin (n + 1)) =>
AlgebraicGeometry.Proj.basicOpen 𝒜 (X j'.down)) (ULift.up j)
rw [key]
exact AlgebraicGeometry.Proj.iSup_basicOpen_eq_top 𝒜 _
(irrelevant_le_span_X R n)