NYLL
Module

ProperGeometricallyReducedSections.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperGeometricallyReducedSections
1 declaration indexed from sourceView source ↗

Module documentation

Global sections of proper geometrically reduced schemes over fields

The global section algebra is finite by proper coherent cohomology. Its extension to an algebraic closure is reduced because flat base change identifies it with the actual sections of the reduced geometric fibre. The resulting finite étale algebra is the field case of the supplier needed for Stacks Project Tag 0BUN.

Imports5
Imported by4

Declarations

theorem

finite_etale_appTop_of_isProper_of_geometricallyReduced_overField

L34 ↗
AlgebraicGeometry.finite_etale_appTop_of_isProper_of_geometricallyReduced_overField
Documentation

The actual global-section map of a proper geometrically reduced scheme over a field is finite étale.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem finite_etale_appTop_of_isProper_of_geometricallyReduced_overField
    {K : Type u} [Field K] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of K)) [IsProper f] [GeometricallyReduced f] :
    f.appTop.hom.Finite ∧ f.appTop.hom.Etale

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