Module

ProperLocalNormalization.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperLocalNormalization

2 declarations indexed from sourceView source ↗

Module documentation

The Stein factor over an arbitrary local base

The actual section algebra computed by Noetherian approximation identifies the second map of relative normalization as finite étale. Its first map has geometrically connected fibres by the unrestricted scalar-section comparison. The original local base is not assumed Noetherian.

Imports6

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.All

theorem

finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_local

L33 ↗

AlgebraicGeometry.finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_local

Documentation

The second native normalization map of a proper flat finitely presented geometrically reduced family over an arbitrary local ring is finite étale.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_local
    {R : Type u} [CommRing R] [IsLocalRing R] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R))
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] [GeometricallyReduced f] :
    IsFiniteEtale f.fromNormalization

theorem

geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced_local

L81 ↗

AlgebraicGeometry.geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced_local