Module

ProperSectionsEtaleFieldDescent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperSectionsEtaleFieldDescent

1 declaration indexed from sourceView source ↗

Module documentation

Étale descent for proper global sections along a field extension

The actual flat section comparison identifies the extended section algebra with the global sections of the field-base-changed scheme. Geometric reducedness there supplies étaleness, which faithfully flat descent reflects to the original section algebra.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperGeometricallyReducedSections
Nyll.SchemeTheory.Affine.SpecFlatBaseChangeSections
Mathlib.RingTheory.Etale.Descent

Imported by2

theorem

etale_appTop_of_isProper_of_geometricallyReduced_field_baseChange

L31 ↗

AlgebraicGeometry.etale_appTop_of_isProper_of_geometricallyReduced_field_baseChange

Documentation

To obtain an étale proper section algebra over a field, it suffices that the family becomes geometrically reduced after a field extension.

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 etale_appTop_of_isProper_of_geometricallyReduced_field_baseChange
    {K L : Type u} [Field K] [Field L] [Algebra K L] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of K)) [IsProper f]
    [GeometricallyReduced
      (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap K L))))] :
    f.appTop.hom.Etale

Module documentation

Étale descent for proper global sections along a field extension

Declarations

etale_appTop_of_isProper_of_geometricallyReduced_field_baseChange