NYLL
Module

ProperNoetherianSectionAlgebra.lean

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

Module documentation

Finite étale sections over a Noetherian affine base

Actual flat base change identifies each localization of the section algebra with sections of the localized family. The proved local-family theorem gives finite projectivity and étaleness there. Localization detects projectivity and the vanishing of differentials for the original section algebra.

Imports7
Imported by2

Declarations

theorem

finite_etale_appTop_of_proper_flat_geometricallyReduced_noetherian

L36 ↗
AlgebraicGeometry.finite_etale_appTop_of_proper_flat_geometricallyReduced_noetherian
Documentation

The original global-section map of a proper flat geometrically reduced family over a Noetherian affine base is finite étale. The base is not assumed local or reduced.

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_proper_flat_geometricallyReduced_noetherian
    {R : Type u} [CommRing R] [IsNoetherianRing R] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] [Flat 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.