Module

UnramifiedFiberDegree.lean

Nyll.EtaleFundamentalGroups.Normalization.UnramifiedFiberDegree

4 declarations indexed from sourceView source ↗

Module documentation

Degrees of the fibers of an unramified normalization

The actual generic-fiber square identifies the rank of a finite etale normalization with the degree of the original field extension. Local constancy then gives the same degree on every scheme-theoretic fiber. This proves the implication from unramifiedness to condition (8) of Stacks Project, Tag 0BTF, with equality rather than only a lower bound. No separability, Galois, or Noetherian hypothesis is added.

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

Imports6

Nyll.EtaleFundamentalGroups.Normalization.GenericExtensionFiber
Nyll.EtaleFundamentalGroups.Normalization.UnramifiedNormalization
Nyll.SchemeTheory.Morphisms.FiberRank
Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Imported by2

instance

fieldSpecQuasiCompact

L35 ↗

EtaleFundamentalGroups.fieldSpecQuasiCompact

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
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

finiteFieldExtension_spec_finrank

L40 ↗

EtaleFundamentalGroups.finiteFieldExtension_spec_finrank

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
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 finiteFieldExtension_spec_finrank
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] (p : PrimeSpectrum K) :
    (Spec.map (CommRingCat.ofHom (algebraMap K L))).finrank p =
      Module.finrank K L

theorem

finiteEtale_genericExtensionNormalization_finrank

L53 ↗

EtaleFundamentalGroups.finiteEtale_genericExtensionNormalization_finrank

Documentation

The degree of the actual finite etale normalization is the original field-extension degree at every point of the integral base.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
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 finiteEtale_genericExtensionNormalization_finrank
    (X : Scheme.{u}) [IsIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    [IsFinite (X.genericExtensionMorphism L).fromNormalization]
    [Etale (X.genericExtensionMorphism L).fromNormalization] (x : X) :
    (X.genericExtensionMorphism L).fromNormalization.finrank x =
      Module.finrank X.functionField L

theorem

unramified_normalization_fiber_finiteEtale_degree

L78 ↗

EtaleFundamentalGroups.unramified_normalization_fiber_finiteEtale_degree

Documentation

The scheme-theoretic fibers of an unramified normalization are finite etale of degree exactly [L : K]. This supplies (2) -> (8) in Tag 0BTF for an arbitrary finite extension of the function field.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
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_fiber_finiteEtale_degree
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : Type u) [Field L] [Algebra X.functionField L]
    [FiniteDimensional X.functionField L]
    (h : FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
      LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization)
    (x : X) :
    IsFinite ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField x) ∧
      Etale ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField x) ∧
      ((X.genericExtensionMorphism L).fromNormalization.fiberToSpecResidueField x).finrank
          (IsLocalRing.closedPoint (X.residueField x)) =
        Module.finrank X.functionField L

Module documentation

Degrees of the fibers of an unramified normalization

Declarations

fieldSpecQuasiCompact

finiteFieldExtension_spec_finrank

finiteEtale_genericExtensionNormalization_finrank

unramified_normalization_fiber_finiteEtale_degree