Module

EisensteinIntegralClosure.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.EisensteinIntegralClosure

1 declaration indexed from sourceView source ↗

Module documentation

Integral elements in an Eisenstein root extension

Over a discrete valuation ring, an integral power basis with Eisenstein minimal polynomial generates every integral element of its fraction-field extension. Clearing polynomial denominators gives a uniformizer power multiple in the generated ring; Eisenstein descent removes that power.

The argument does not require separability or Henselianity, and assumes no comparison with a chosen extension valuation ring.

Imports9

Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.FieldTheory.Minpoly.Basic
Mathlib.RingTheory.Adjoin.Polynomial.Basic
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Mathlib.RingTheory.Polynomial.RationalRoot
Mathlib.RingTheory.PowerBasis

Imported by2

theorem

mem_adjoin_of_isIntegral_of_minpoly_isEisensteinAt

L42 ↗

ValuationTheory.DiscreteValuationField.mem_adjoin_of_isIntegral_of_minpoly_isEisensteinAt

Documentation

An integral power-basis generator with Eisenstein minimal polynomial generates the integral closure of a DVR inside the extension field.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open scoped nonZeroDivisors Polynomial
universe u v w
variable {R : Type u} {K : Type v} {L : Type w}
  [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  [Field K] [Field L] [Algebra R K] [IsFractionRing R K]
  [Algebra K L] [Algebra R L] [IsScalarTower R K L]

Lean source · statement

theorem mem_adjoin_of_isIntegral_of_minpoly_isEisensteinAt
    (B : PowerBasis K L)
    (hE : (minpoly R B.gen).IsEisensteinAt (IsLocalRing.maximalIdeal R))
    {z : L} (hz : IsIntegral R z) :
    z ∈ Algebra.adjoin R ({B.gen} : Set L)

Module documentation

Integral elements in an Eisenstein root extension

Declarations

mem_adjoin_of_isIntegral_of_minpoly_isEisensteinAt