NYLL
Module

ChowDatum_nonempty.lean

Nyll.SchemeTheory.Morphisms.ChowDatum_nonempty
19 declarations indexed from sourceView source ↗

Module documentation

Construction of Chow data from finite affine covers of proper integral schemes.

Imports11
  • Nyll.SchemeTheory.ProjectiveSpace.Basic
  • Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  • Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
  • Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
  • Mathlib.AlgebraicGeometry.ZariskisMainTheorem
  • Mathlib.AlgebraicGeometry.Noetherian
  • Mathlib.AlgebraicGeometry.Birational.RationalMap
  • Mathlib.AlgebraicGeometry.Morphisms.Proper
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
  • Mathlib.Topology.QuasiSeparated
Imported by3

Declarations

structure

FinAffCover

L47 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.FinAffCover
Documentation

A finite linearly ordered affine open cover of a scheme.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
Lean source · full declaration
structure FinAffCover (V : Scheme.{u}) where

  /-- The type indexing the affine open subsets. -/
  ι : Type u
  /-- Finiteness of the index type. -/
  [fι : Fintype ι]
  /-- The linear order used to enumerate the affine opens. -/
  [linι : LinearOrder ι]
  /-- The affine open subsets in the cover. -/
  U : ι → V.Opens

  /-- Each member of the cover is affine. -/
  hU : ∀ i, IsAffineOpen (U i)

  /-- The affine opens cover the whole scheme. -/
  hcov : ⨆ i, U i = ⊤
theorem

exists_of_isProper

L66 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.FinAffCover.exists_of_isProper
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
Lean source · statement
theorem FinAffCover.exists_of_isProper {R : Type u} [CommRing R] {V : Scheme.{u}}
    (π : V ⟶ Spec (CommRingCat.of R)) [IsProper π] :
    Nonempty (FinAffCover V)
def

canonicalAlg

L88 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.canonicalAlg
Documentation

The base-ring algebra structure on sections induced by the structure morphism.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section CanonicalAlg
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · statement
def canonicalAlg (W : V.Opens) : Algebra R Γ(V, W)
theorem

canonicalAlg_compat

L92 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.canonicalAlg_compat
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section CanonicalAlg
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
theorem canonicalAlg_compat (W : V.Opens) :
    ∀ c, letI := canonicalAlg π W
      algebraMap R Γ(V, W) c = (V.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
        (π.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom c)) :=
  fun _ => rfl
theorem

gammaFiniteType

L108 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.gammaFiniteType
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
Lean source · full declaration
theorem gammaFiniteType :
    letI := canonicalAlg π W
    Algebra.FiniteType R Γ(V, W) := by
  let := canonicalAlg π W
  have happ : (π.appLE ⊤ W le_top).hom.FiniteType :=
    π.finiteType_appLE (isAffineOpen_top _) hW le_top
  have hcomp : ((π.appLE ⊤ W le_top).hom.comp
      (Scheme.ΓSpecIso (.of R)).symm.commRingCatIsoToRingEquiv.toRingHom).FiniteType :=
    RingHom.finiteType_respectsIso.2 _ _ happ
  refine RingHom.finiteType_algebraMap.mp ?_
  convert hcomp using 2
  exact RingHom.ext fun _ => rfl
def

chartN

L122 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartN
Documentation

The number of affine coordinate generators chosen for an affine chart.

Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
Lean source · statement
def chartN : ℕ
def

chartφ

L131 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartφ
Documentation

Present an affine chart by homogeneous coordinates with an additional unit coordinate.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
def chartφ :
    MvPolynomial (Fin (chartN π W hW + 1)) R →+* Γ(W.toScheme, ⊤)
theorem

chartφ_surj

L140 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartφ_surj
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartφ_surj : Function.Surjective (chartφ π W hW)
theorem

chartφ_X0

L158 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartφ_X0
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartφ_X0 : chartφ π W hW (MvPolynomial.X 0) = 1
theorem

chartφ_irr

L163 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartφ_irr
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartφ_irr :
    (HomogeneousIdeal.irrelevant 𝒜W).toIdeal.map (chartφ π W hW) = ⊤
def

chartJ

L174 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJ
Documentation

The morphism from an affine chart to its projective closure.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
def chartJ : W.toScheme ⟶ Proj 𝒜W
theorem

chartJ_over

L177 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJ_over
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartJ_over :
    chartJ π W hW ≫ ProjSpace.π R (chartN π W hW)
      = W.ι ≫ π
theorem

chartJ_preimage_D0

L206 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJ_preimage_D0
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartJ_preimage_D0 :
    chartJ π W hW ⁻¹ᵁ Proj.basicOpen 𝒜W (MvPolynomial.X 0) = ⊤
def

chartJD

L213 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJD
Documentation

Factor the chart morphism through the basic open of the unit coordinate.

Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
def chartJD :
    W.toScheme ⟶ (Proj.basicOpen 𝒜W (MvPolynomial.X 0)).toScheme
theorem

chartJD_ι

L218 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJD_ι
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartJD_ι :
    chartJD π W hW ≫ (Proj.basicOpen 𝒜W (MvPolynomial.X 0)).ι
      = chartJ π W hW
theorem

chartJD_closed

L224 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.chartJD_closed
Source context 17 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section PerChart
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R] {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π]
variable (W : V.Opens) (hW : IsAffineOpen W)
include hW
local notation "𝒜W" =>
  MvPolynomial.homogeneousSubmodule (Fin (chartN π W hW + 1)) R
Lean source · statement
theorem chartJD_closed : IsClosedImmersion (chartJD π W hW)
theorem

exists_integral_chowDatum

L299 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty.AlgebraicGeometry.ChowLemma.exists_integral_chowDatum
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ChowLemma
attribute [scoped instance] FinAffCover.fι FinAffCover.linι
section Headline
open AlgebraicGeometry.Proj
variable {R : Type u} [CommRing R]
variable {V : Scheme.{u}} (π : V ⟶ Spec (.of R)) [IsProper π] [IsIntegral V]
Lean source · statement
theorem exists_integral_chowDatum :
    ∃ D : ChowDatum π, IsIntegral D.V' ∧ Surjective D.p
theorem

exists_integral

L740 ↗
AlgebraicGeometry.ChowDatum.exists_integral
Documentation

A proper integral scheme over any ring has integral, surjective projective Chow data. Quasi-compactness comes from finite affine intersections and proper inverse images, so no Noetherian hypothesis is needed.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
Lean source · statement
theorem _root_.AlgebraicGeometry.ChowDatum.exists_integral {R : Type u} [CommRing R]
    {V : AlgebraicGeometry.Scheme.{u}}
    (π : V ⟶ AlgebraicGeometry.Spec (.of R)) [AlgebraicGeometry.IsProper π]
        [AlgebraicGeometry.IsIntegral V] :
    ∃ D : AlgebraicGeometry.ChowDatum π,
      AlgebraicGeometry.IsIntegral D.V' ∧ AlgebraicGeometry.Surjective D.p
theorem

nonempty

L748 ↗
AlgebraicGeometry.ChowDatum.nonempty
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.ChowDatum_nonempty
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
Lean source · statement
theorem _root_.AlgebraicGeometry.ChowDatum.nonempty {R : Type u} [CommRing R]
    [IsNoetherianRing R] {V : AlgebraicGeometry.Scheme.{u}}
    (π : V ⟶ AlgebraicGeometry.Spec (.of R)) [AlgebraicGeometry.IsProper π]
        [AlgebraicGeometry.IsIntegral V] :
    Nonempty (AlgebraicGeometry.ChowDatum π)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.