Module

HenselianPolynomialFactors.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianPolynomialFactors

2 declarations indexed from sourceView source ↗

Module documentation

Descending factors from the completion of a Henselian DVF

The coefficients of a monic divisor of a separable polynomial are separable over the original field. Separable algebraic closedness in the completion therefore descends the divisor, preserving monicity and divisibility.

Imports3

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianDVF
Nyll.ValuedFieldTheory.Valuation.Completion.SeparableFactorCoefficients
Mathlib.Algebra.Polynomial.Lifts

Imported by2

theorem

exists_monic_factor_of_dvd_completion

L27 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_factor_of_dvd_completion

Documentation

A monic factor of a separable polynomial over the valuation completion descends to a monic factor over the original Henselian field.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open Polynomial
variable {K : Type*} [Field K]

Lean source · statement

theorem exists_monic_factor_of_dvd_completion (base : HenselianDVF K)
    {f : K[X]} (hf : f.Separable) {g : base.valuation.Completion[X]}
    (hg : g.Monic) (hdiv : g ∣ f.map (algebraMap K base.valuation.Completion)) :
    ∃ g₀ : K[X], g₀.Monic ∧
      g₀.map (algebraMap K base.valuation.Completion) = g ∧ g₀ ∣ f

theorem

irreducible_map_completion

L44 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.irreducible_map_completion