Module

HenselReduction.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.HenselReduction

1 declaration indexed from sourceView source ↗

Module documentation

the unramified base-change theorem: irreducible reduction source

The base-change proof uses the following exact Hensel step. If a monic polynomial over a Henselian valuation ring is irreducible over the fraction field and its reduction is separable, then that reduction is already irreducible. Otherwise a nontrivial residual factorization is coprime and Hensel lifting contradicts irreducibility upstairs.

Imports2

Imported by2

theorem

irreducible_residue_of_irreducible_of_separable_of_henselian

L29 ↗

AlgebraicNumberTheory.Valuations.irreducible_residue_of_irreducible_of_separable_of_henselian

Documentation

A monic polynomial irreducible over the valued field has irreducible reduction whenever that reduction is separable.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem irreducible_residue_of_irreducible_of_separable_of_henselian
    {K : Type*} [Field K]
    (V : ValuationSubring K)
    (hhens : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty V)
    {f : V[X]} (hf : f.Monic)
    (hirr : Irreducible (f.map (algebraMap V K)))
    (hsep : (f.map (IsLocalRing.residue V)).Separable) :
    Irreducible (f.map (IsLocalRing.residue V))

Module documentation

the unramified base-change theorem: irreducible reduction source

Declarations

irreducible_residue_of_irreducible_of_separable_of_henselian