NYLL
Module

ProperNoetherianNormalization.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianNormalization
3 declarations indexed from sourceView source ↗

Module documentation

The finite étale factor of a proper reduced family

For a proper flat geometrically reduced family over a locally Noetherian scheme, the actual native relative normalization has finite étale second map. On an affine base this follows from the computed section algebra and the actual section isomorphism of the first map. The native normalization comparison under smooth base change then supplies the affine-open descent.

This proves the locally Noetherian case of the finite étale conclusion in Stacks Project Tag 0BUN, using the native relative normalization.

Imports9
Imported by2

Declarations

theorem

finite_etale_appTop_of_proper_flat_affine_noetherian

L38 ↗
AlgebraicGeometry.finite_etale_appTop_of_proper_flat_affine_noetherian
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem finite_etale_appTop_of_proper_flat_affine_noetherian
    {X S : Scheme.{u}} [IsAffine S] [IsLocallyNoetherian S]
    (f : X ⟶ S) [IsProper f] [Flat f] [GeometricallyReduced f] :
    f.appTop.hom.Finite ∧ f.appTop.hom.Etale
theorem

finite_etale_fromNormalization_of_proper_flat_affine_noetherian

L55 ↗
AlgebraicGeometry.finite_etale_fromNormalization_of_proper_flat_affine_noetherian
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem finite_etale_fromNormalization_of_proper_flat_affine_noetherian
    {X S : Scheme.{u}} [IsAffine S] [IsLocallyNoetherian S]
    (f : X ⟶ S) [IsProper f] [Flat f] [GeometricallyReduced f] :
    IsFiniteEtale f.fromNormalization
theorem

finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_noetherian

L82 ↗
AlgebraicGeometry.finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_noetherian
Documentation

The actual second map of relative normalization is finite étale for a proper flat geometrically reduced family over a locally Noetherian base. No section-algebra comparison or étaleness is supplied as an input.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem finite_etale_fromNormalization_of_proper_flat_geometricallyReduced_noetherian
    {X S : Scheme.{u}} [IsLocallyNoetherian S] (f : X ⟶ S)
    [IsProper f] [Flat f] [GeometricallyReduced f] :
    IsFinite f.fromNormalization ∧ Etale f.fromNormalization

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