NYLL
Module

EisensteinResidue.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.EisensteinResidue
2 declarations indexed from sourceView source ↗

Module documentation

Residue fields of Eisenstein root extensions

In an actual extension of a Henselian discrete valuation, an Eisenstein power-basis generator generates the target valuation ring. Its residue is zero, so every target residue is the image of a constant coefficient from the base valuation ring.

Imports11
Imported by3

Declarations

theorem

residue_eq_zero_of_weaklyEisenstein_root

L36 ↗
ValuationTheory.DiscreteValuationField.residue_eq_zero_of_weaklyEisenstein_root
Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open scoped Polynomial
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residue_eq_zero_of_weaklyEisenstein_root
    (base : DVF.{u, v} K) (target : DVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (f : base.valuationSubring[X]) (hf : f.Monic)
    (hE : f.IsWeaklyEisensteinAt base.maximalIdeal)
    (a : target.valuationSubring)
    (ha : (f.map (ValuedExtension.integerMap base target)).IsRoot a) :
    target.residueMap a = 0
theorem

residueMap_surjective_of_minpoly_isEisensteinAt

L56 ↗
ValuationTheory.DiscreteValuationField.residueMap_surjective_of_minpoly_isEisensteinAt
Documentation

An Eisenstein power-basis extension of a Henselian DVF has surjective actual residue-field map. The valuation ring and its polynomial representatives are generated from Henselianity and the Eisenstein condition.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open scoped Polynomial
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residueMap_surjective_of_minpoly_isEisensteinAt
    (base : HenselianDVF.{u, v} K) (target : DVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    (B : PowerBasis K L)
    (hE : (minpoly base.valuationSubring B.gen).IsEisensteinAt base.maximalIdeal) :
    Function.Surjective (ValuedExtension.residueMap base.toDVF target)

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