AlgebraicNumberTheory.Valuations.henselFactorization_complete_exists_factorization
Hensel's lemma in the complete nonarchimedean-valued-field setting. A primitive polynomial over the valuation ring whose reduction is a product of coprime factors lifts to a factorization with the prescribed reductions and with the degree of the left factor unchanged.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace ValuationsLean source · statement
theorem henselFactorization_complete_exists_factorization
{K : Type*} [Field K]
(v : AbsoluteValue K ℝ)
(hcomplete : IsCompleteForAbsoluteValue v)
(hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
{f : (absoluteValueValuationSubring v hnonarch)[X]}
{gbar hbar : (IsLocalRing.ResidueField
(absoluteValueValuationSubring v hnonarch))[X]}
(hprim : f.map (IsLocalRing.residue
(absoluteValueValuationSubring v hnonarch)) ≠ 0)
(hfbar : f.map (IsLocalRing.residue
(absoluteValueValuationSubring v hnonarch)) =
gbar * hbar)
(hcop : IsCoprime gbar hbar) :
∃ G H :
(absoluteValueValuationSubring v hnonarch)[X],
f = G * H ∧
G.natDegree = gbar.natDegree ∧
G.map (IsLocalRing.residue
(absoluteValueValuationSubring v hnonarch)) =
gbar ∧
H.map (IsLocalRing.residue
(absoluteValueValuationSubring v hnonarch)) =
hbar