Documentation

GAGA.OpenCover

source
@[simp]
theorem AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens_f_coe (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) :
↑((AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).f x) = (Exists.choose ⋯).obj
source
@[simp]
theorem AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens_map (X : AlgebraicGeometry.Scheme) :
∀ (x : ↑(AlgebraicGeometry.Scheme.affineOpens X)), (AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).map x = AlgebraicGeometry.Scheme.ofRestrict X ⋯
source
@[simp]
theorem AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens_obj (X : AlgebraicGeometry.Scheme) (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) :
(AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).obj U = AlgebraicGeometry.Scheme.restrict X ⋯
source
@[simp]
theorem AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens_J (X : AlgebraicGeometry.Scheme) :
(AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).J = ↑(AlgebraicGeometry.Scheme.affineOpens X)
source
noncomputable def AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens (X : AlgebraicGeometry.Scheme) :
AlgebraicGeometry.Scheme.OpenCover X

Open cover of a scheme by all of its affine opens.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance AlgebraicGeometry.Scheme.inst_isAffine_of_openCoverOfAllAffineOpens (X : AlgebraicGeometry.Scheme) (U : (AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).J) :
    AlgebraicGeometry.IsAffine ((AlgebraicGeometry.Scheme.openCoverOfAllAffineOpens X).obj U)
    Equations
    • ⋯ = ⋯