NYLL
Module

UnramifiedNormalization.lean

Nyll.EtaleFundamentalGroups.Normalization.UnramifiedNormalization
7 declarations indexed from sourceView source ↗

Module documentation

Unramified normalizations are finite étale

A dominant unramified morphism from an integral scheme to a normal integral scheme is étale. Applied to relative normalization in a field extension of the function field, integrality then supplies finiteness. No Noetherian assumption is needed.

Reference: https://stacks.math.columbia.edu/tag/0BQK

Imports14
Imported by4

Declarations

theorem

etale_of_dominant_unramified

L45 ↗
EtaleFundamentalGroups.etale_of_dominant_unramified
Documentation

A quasi-compact dominant unramified morphism between integral schemes is étale if its target is normal.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem etale_of_dominant_unramified
    {X Y : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X] [IsIntegral Y]
    (f : Y ⟶ X) [IsDominant f] [QuasiCompact f]
    [FormallyUnramified f] [LocallyOfFiniteType f] : Etale f
instance

fieldSpecQuasiCompact

L78 ↗
EtaleFundamentalGroups.fieldSpecQuasiCompact
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
theorem

isDominant_genericExtensionMorphism

L85 ↗
EtaleFundamentalGroups.isDominant_genericExtensionMorphism
Documentation

The generic extension morphism has dense image because its image contains the generic point.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem isDominant_genericExtensionMorphism
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L] :
    IsDominant (X.genericExtensionMorphism L)
theorem

isDominant_fromNormalization_genericExtension

L99 ↗
EtaleFundamentalGroups.isDominant_fromNormalization_genericExtension
Documentation

The relative normalization in a field extension remains dominant over the original integral scheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem isDominant_fromNormalization_genericExtension
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L] :
    IsDominant (X.genericExtensionMorphism L).fromNormalization
theorem

unramified_normalization_iff_etale_iff_finiteEtale

L112 ↗
EtaleFundamentalGroups.unramified_normalization_iff_etale_iff_finiteEtale
Documentation

Stacks Project, Tag 0BQK: normalization is unramified exactly when it is étale, and in this case it is finite.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem unramified_normalization_iff_etale_iff_finiteEtale
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L] :
    ((FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
        LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization) ↔
      Etale (X.genericExtensionMorphism L).fromNormalization) ∧
    (Etale (X.genericExtensionMorphism L).fromNormalization ↔
      IsFinite (X.genericExtensionMorphism L).fromNormalization ∧
        Etale (X.genericExtensionMorphism L).fromNormalization)
theorem

unramified_normalization_stalk_of_unramified

L143 ↗
EtaleFundamentalGroups.unramified_normalization_stalk_of_unramified
Documentation

An unramified normalization remains unramified over the local ring at any point. This is the original implication (2) → (5) in Tag 0BTF.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem unramified_normalization_stalk_of_unramified
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    (h : FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
      LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization)
    (x : X) :
    FormallyUnramified (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x)) ∧
      LocallyOfFiniteType (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x))
theorem

unramified_normalization_stalk_iff_geometricStalk

L176 ↗
EtaleFundamentalGroups.unramified_normalization_stalk_iff_geometricStalk
Documentation

Unramifiedness over the actual local ring is equivalent to unramifiedness over its constructed pointed étale stalk. Faithful flatness of the actual structure map supplies descent, and pullback pasting compares the literal scheme morphisms. The residue-field point gives the ordinary henselization; a separably closed geometric point gives the strict henselization. Thus this supplies (5) ↔ (6) and (5) ↔ (7) in Tag 0BTF. No finite-presentation, separability, Galois, or Noetherian premise is added.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact
Lean source · statement
theorem unramified_normalization_stalk_iff_geometricStalk
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    (x : X) {Ω : Type u} [Field Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ] :
    (FormallyUnramified (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x)) ∧
      LocallyOfFiniteType (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization (X.fromSpecStalk x))) ↔
    (FormallyUnramified (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization
        (Spec.map (CommRingCat.ofHom (StrictHenselian.geometricStalkStructureMap φ)) ≫
          X.fromSpecStalk x)) ∧
      LocallyOfFiniteType (pullback.snd
        (X.genericExtensionMorphism L).fromNormalization
        (Spec.map (CommRingCat.ofHom (StrictHenselian.geometricStalkStructureMap φ)) ≫
          X.fromSpecStalk x)))

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