NYLL
Module

ProperNormalization.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNormalization
4 declarations indexed from sourceView source ↗

Module documentation

Stein factorization of a proper flat finitely presented reduced family

Over an arbitrary scheme, the actual native relative normalization has finite étale second map and geometrically connected first map. The affine calculation uses actual Noetherian approximation of the section algebra; normalization base change supplies descent along the affine open cover.

This proves the finite étale conclusion of Stacks Project Tag 0BUN with its original base and finite-presentation hypotheses.

Imports11
Imported by3

Declarations

theorem

finite_etale_appTop_of_proper_flat_affine

L39 ↗
AlgebraicGeometry.finite_etale_appTop_of_proper_flat_affine
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
    {X S : Scheme.{u}} [IsAffine S] (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] [GeometricallyReduced f] :
    f.appTop.hom.Finite ∧ f.appTop.hom.Etale
theorem

finite_etale_fromNormalization_of_proper_flat_affine

L53 ↗
AlgebraicGeometry.finite_etale_fromNormalization_of_proper_flat_affine
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
    {X S : Scheme.{u}} [IsAffine S] (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] [GeometricallyReduced f] :
    IsFiniteEtale f.fromNormalization
theorem

finite_etale_fromNormalization_of_proper_flat_geometricallyReduced

L80 ↗
AlgebraicGeometry.finite_etale_fromNormalization_of_proper_flat_geometricallyReduced
Documentation

The actual second map of relative normalization is finite étale for a proper flat finitely presented geometrically reduced family over any base scheme (Stacks Project Tag 0BUN).

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
    {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] [GeometricallyReduced f] :
    IsFinite f.fromNormalization ∧ Etale f.fromNormalization
theorem

geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced

L112 ↗
AlgebraicGeometry.geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced
Documentation

The first map of the actual Stein factorization has geometrically connected fibres for a proper flat finitely presented geometrically reduced family over any base scheme.

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 geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced
    {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] [GeometricallyReduced f] :
    GeometricallyConnected f.toNormalization

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