Module

DVRNormalization.lean

Nyll.SchemeTheory.RingTheory.Ramification.Unramified.DVRNormalization

4 declarations indexed from sourceView source ↗

Module documentation

Unramified field extensions of a discrete valuation ring

For a finite separable extension of a DVR's fraction field, unramifiedness means that every maximal prime of the integral closure has ramification index one and separable residue extension. This is the unramified case of Stacks Project, Tag 09E9.

We prove that these residue and ramification conditions make the actual integral closure finite étale. Its base change to the fraction field is canonically the original field extension. These are the algebraic inputs to the codimension-one step of Tag 0H2W.

Imports8

Nyll.SchemeTheory.AbhyankarLemma.Geometry.UnramifiedCriterion
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Kaehler.TensorProduct
Mathlib.RingTheory.LocalProperties.Submodule
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Smooth.Fiber

Imported by5

def

IsUnramifiedOverDVR

L43 ↗

SchemeTheory.IsUnramifiedOverDVR

Documentation

The residue-field and ramification-index condition for a field extension to be unramified with respect to a DVR. In applications the extension of the fraction field is finite separable. Every maximal prime of the integral closure contracts to the maximal ideal of the base DVR.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
universe u v w
namespace SchemeTheory

Lean source · statement

def IsUnramifiedOverDVR (R : Type u) (L : Type w)
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field L] [Algebra R L] : Prop

theorem

finite_etale_integralClosure_of_unramifiedOverDVR

L55 ↗

SchemeTheory.finite_etale_integralClosure_of_unramifiedOverDVR

Documentation

The normalization of a DVR in a finite separable fraction-field extension is finite étale when the ramification indices are one and all residue extensions are separable.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
universe u v w
namespace SchemeTheory

Lean source · statement

theorem finite_etale_integralClosure_of_unramifiedOverDVR
    (R : Type u) (K : Type v) (L : Type w)
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (h : IsUnramifiedOverDVR R L) :
    Module.Finite R (integralClosure R L) ∧
      Algebra.Etale R (integralClosure R L)

def

integralClosureGenericFiberEquiv

L98 ↗

SchemeTheory.integralClosureGenericFiberEquiv

Documentation

The generic fibre of the actual integral closure is the original algebraic field extension, with its given fraction-field algebra structure.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
universe u v w
namespace SchemeTheory

Lean source · statement

def integralClosureGenericFiberEquiv
    (R : Type u) (K : Type v) (L : Type w)
    [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [Algebra.IsAlgebraic K L] :
    K ⊗[R] integralClosure R L ≃ₐ[K] L

theorem

integralClosureGenericFiberEquiv_tmul

L113 ↗

SchemeTheory.integralClosureGenericFiberEquiv_tmul

Documentation

The generic-fibre comparison multiplies a fraction by the integral element.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
universe u v w
namespace SchemeTheory

Lean source · statement

theorem integralClosureGenericFiberEquiv_tmul
    (R : Type u) (K : Type v) (L : Type w)
    [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [Algebra.IsAlgebraic K L] (k : K) (b : integralClosure R L) :
    integralClosureGenericFiberEquiv R K L (k ⊗ₜ[R] b) =
      algebraMap K L k * (b : L)

Module documentation

Unramified field extensions of a discrete valuation ring

Declarations

IsUnramifiedOverDVR

finite_etale_integralClosure_of_unramifiedOverDVR

integralClosureGenericFiberEquiv

integralClosureGenericFiberEquiv_tmul