MonicFactorization.lean

theorem valuation_coeff_prod_X_sub_C_le_pow_card
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (B : Γ) (hB : 1 ≤ B) (s : Multiset L)
    (hs : ∀ α ∈ s, w α ≤ B) (i : ℕ) :
    w (((s.map (fun α => Polynomial.X - Polynomial.C α)).prod).coeff i) ≤
      B ^ s.card := by
  induction s using Multiset.induction_on generalizing i with
  | empty =>
      cases i <;> simp [Polynomial.coeff_one]
  | @cons α s ih =>
      have hα : w α ≤ B := hs α (by simp)
      have hs' : ∀ β ∈ s, w β ≤ B := by
        intro β hβ
        exact hs β (by simp [hβ])
      have hpow_step : B ^ s.card ≤ B ^ (s.card + 1) := by
        rw [pow_succ]
        calc
          B ^ s.card = B ^ s.card * 1 := (mul_one _).symm
          _ ≤ B ^ s.card * B := by
            simpa [mul_comm] using mul_le_mul_right hB (B ^ s.card)
      simp only [Multiset.map_cons, Multiset.prod_cons, Multiset.card_cons]
      cases i with
      | zero =>
          have hq := ih hs' 0
          calc
            w (((Polynomial.X - Polynomial.C α) *
                (s.map (fun β => Polynomial.X - Polynomial.C β)).prod).coeff 0) =
                w α *
                  w (((s.map (fun β =>
                    Polynomial.X - Polynomial.C β)).prod).coeff 0) := by
              simp [Polynomial.coeff_zero_eq_eval_zero]
            _ ≤ B * B ^ s.card := mul_le_mul' hα hq
            _ = B ^ (s.card + 1) := by
              rw [pow_succ]
              ac_rfl
      | succ j =>
          rw [Polynomial.coeff_X_sub_C_mul]
          have hqj := ih hs' j
          have hqsucc := ih hs' (j + 1)
          have hterm :
              w (α * ((s.map (fun β =>
                Polynomial.X - Polynomial.C β)).prod).coeff (j + 1)) ≤
                B ^ (s.card + 1) := by
            rw [w.map_mul]
            calc
              w α * w (((s.map (fun β =>
                  Polynomial.X - Polynomial.C β)).prod).coeff (j + 1)) ≤
                  B * B ^ s.card := mul_le_mul' hα hqsucc
              _ = B ^ (s.card + 1) := by
                rw [pow_succ]
                ac_rfl
          calc
            w (((s.map (fun β => Polynomial.X - Polynomial.C β)).prod).coeff j -
                α * ((s.map (fun β =>
                  Polynomial.X - Polynomial.C β)).prod).coeff (j + 1)) ≤
                max
                  (w (((s.map (fun β =>
                    Polynomial.X - Polynomial.C β)).prod).coeff j))
                  (w (α * ((s.map (fun β =>
                    Polynomial.X - Polynomial.C β)).prod).coeff (j + 1))) := by
              exact
                w.map_sub
                  (((s.map (fun β =>
                    Polynomial.X - Polynomial.C β)).prod).coeff j)
                  (α * ((s.map (fun β =>
                    Polynomial.X - Polynomial.C β)).prod).coeff (j + 1))
            _ ≤ B ^ (s.card + 1) :=
              max_le (hqj.trans hpow_step) hterm

theorem valuation_multiset_prod_eq_pow_card_of_eq
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (t : Γ) (s : Multiset L)
    (hs : ∀ α ∈ s, w α = t) :
    w s.prod = t ^ s.card

theorem esymm_cons_succ
    {R : Type*} [CommRing R] (a : R) (s : Multiset R) (n : ℕ) :
    (a ::ₘ s).esymm (n + 1) = s.esymm (n + 1) + a * s.esymm n

theorem valuation_esymm_le_pow
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (t : Γ) (s : Multiset L)
    (hs : ∀ a ∈ s, w a ≤ t) (n : ℕ) :
    w (s.esymm n) ≤ t ^ n

theorem valuation_esymm_lt_pow
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (t : Γ) (ht : t ≠ 0) (s : Multiset L)
    (hs : ∀ a ∈ s, w a < t) {n : ℕ} (hn : 0 < n) :
    w (s.esymm n) < t ^ n

theorem valuation_multiset_prod_lt_one_of_mem_lt_one
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (s : Multiset L) {a : L}
    (ha : a ∈ s) (halt : w a < 1)
    (hs : ∀ b ∈ s, w b ≤ 1) :
    w s.prod < 1

theorem valuation_esymm_eq_pow_card_add_of_eq_of_lt
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (t : Γ) (ht : t ≠ 0)
    (seq slt : Multiset L)
    (hseq : ∀ a ∈ seq, w a = t)
    (hslt : ∀ a ∈ slt, w a < t) :
    w ((seq + slt).esymm seq.card) = t ^ seq.card

theorem residue_ne_zero_of_isPrimitive_valuationSubring
    {K : Type u} [Field K] (V : ValuationSubring K)
    {p : Polynomial V} (hp : p.IsPrimitive) :
    p.map (IsLocalRing.residue V) ≠ 0

theorem valuation_coeff_prod_X_sub_C_lt_coeff_zero_of_one_lt
    {L Γ : Type*} [Field L] [LinearOrderedCommGroupWithZero Γ]
    (w : Valuation L Γ) (s : Multiset L)
    (hs : ∀ α ∈ s, 1 < w α) (j : ℕ) (hj : 0 < j) :
    w (((s.map (fun α => Polynomial.X - Polynomial.C α)).prod).coeff j) <
      w (((s.map (fun α => Polynomial.X - Polynomial.C α)).prod).coeff 0) := by
  induction s using Multiset.induction_on generalizing j with
  | empty =>
      simp [Polynomial.coeff_one, Nat.ne_of_gt hj]
  | @cons α s ih =>
      have hα : 1 < w α := hs α (by simp)
      have hs' : ∀ β ∈ s, 1 < w β := by
        intro β hβ
        exact hs β (by simp [hβ])
      let q : Polynomial L :=
        (s.map (fun β => Polynomial.X - Polynomial.C β)).prod
      have hqzero : q.coeff 0 ≠ 0 := by
        have hprod : (s.map fun β => -β).prod ≠ 0 := by
          apply Multiset.prod_ne_zero
          intro hzero
          rcases Multiset.mem_map.mp hzero with ⟨β, hβ, hβzero⟩
          have hβne : β ≠ 0 := by
            intro h
            subst β
            simpa using hs' 0 hβ
          exact hβne (neg_eq_zero.mp hβzero)
        dsimp [q]
        rw [Polynomial.coeff_zero_eq_eval_zero,
          Polynomial.eval_multiset_prod]
        simpa using hprod
      have hqzeroPos : 0 < w (q.coeff 0) :=
        (Valuation.pos_iff w).2 hqzero
      cases j with
      | zero => simp at hj
      | succ k =>
          have hfirst :
              w (q.coeff k) < w α * w (q.coeff 0) := by
            cases k with
            | zero => exact lt_mul_of_one_lt_left hqzeroPos hα
            | succ k =>
                exact (ih hs' (k + 1) (Nat.succ_pos k)).trans
                  (lt_mul_of_one_lt_left hqzeroPos hα)
          have hsecond :
              w (α * q.coeff (k + 1)) <
                w α * w (q.coeff 0) := by
            rw [w.map_mul]
            exact mul_lt_mul_of_pos_left
              (ih hs' (k + 1) (Nat.succ_pos k)) (zero_lt_one.trans hα)
          simp only [Multiset.map_cons, Multiset.prod_cons]
          rw [Polynomial.coeff_X_sub_C_mul]
          have hadd := w.map_add (q.coeff k) (-α * q.coeff (k + 1))
          have hneg : w (-α * q.coeff (k + 1)) =
              w (α * q.coeff (k + 1)) := by simp
          have hcoeff :
              w (q.coeff k - α * q.coeff (k + 1)) <
                w α * w (q.coeff 0) := by
            calc
              w (q.coeff k - α * q.coeff (k + 1)) ≤
                  max (w (q.coeff k))
                    (w (-α * q.coeff (k + 1))) := by
                      simpa [sub_eq_add_neg] using hadd
              _ < w α * w (q.coeff 0) :=
                max_lt hfirst (hneg.trans_lt hsecond)
          simpa [q, Polynomial.coeff_zero_eq_eval_zero, w.map_mul] using hcoeff

theorem residue_root_of_integral_root
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (B : ValuationSubring L)
    [V.valuation.HasExtension B.valuation]
    {Q : Polynomial V} {β : L}
    (hβle : B.valuation β ≤ 1)
    (hroot : ((Q.map V.subtype).map (algebraMap K L)).IsRoot β) :
    ∃ ρ : IsLocalRing.ResidueField V →+* IsLocalRing.ResidueField B,
      ((Q.map (IsLocalRing.residue V)).map ρ).IsRoot
        (IsLocalRing.residue B
          (⟨β, (B.valuation_le_one_iff β).1 hβle⟩ : B))

theorem exists_mixed_residual_minpoly_of_irreducible_roots_unequal
    {K L : Type*} [Field K] [Field L] [Algebra K L] [Normal K L]
    (V : ValuationSubring K) (B : ValuationSubring L)
    [V.valuation.HasExtension B.valuation]
    {p : Polynomial K} (hp : Irreducible p)
    (hsplit : (p.map (algebraMap K L)).Splits)
    {α β : L}
    (hα : α ∈ (p.map (algebraMap K L)).roots)
    (hβ : β ∈ (p.map (algebraMap K L)).roots)
    (hαβ : B.valuation α ≠ B.valuation β) :
    ∃ Q : Polynomial V,
      Q.Monic ∧ Irreducible (Q.map V.subtype) ∧
        (Q.map (IsLocalRing.residue V)).coeff 0 = 0 ∧
          ∃ (ρ : IsLocalRing.ResidueField V →+*
              IsLocalRing.ResidueField B)
            (b : IsLocalRing.ResidueField B),
            b ≠ 0 ∧ ((Q.map (IsLocalRing.residue V)).map ρ).IsRoot b

theorem not_all_roots_same_valuation_of_primitive_irreducible_endpoints_nonunit
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (B : ValuationSubring L)
    [V.valuation.HasExtension B.valuation]
    {p : Polynomial V}
    (hpprim : p.IsPrimitive)
    (hirr : Irreducible (p.map (algebraMap V K)))
    (hsplit :
      ((p.map (algebraMap V K)).map (algebraMap K L)).Splits)
    (hlead : ¬IsUnit p.leadingCoeff)
    (hconst : ¬IsUnit (p.coeff 0))
    {α : L}
    (hα : α ∈ ((p.map (algebraMap V K)).map
      (algebraMap K L)).roots) :
    ¬ ∀ β ∈ ((p.map (algebraMap V K)).map
      (algebraMap K L)).roots, B.valuation β = B.valuation α

def MonicResidualCoprimeFactorLifting
    {K : Type u} [Field K] (V : ValuationSubring K) : Prop

theorem monicResidualCoprimeFactorLifting_of_henselFactorization
    {K : Type u} [Field K] {V : ValuationSubring K}
    (hhensel : HenselFactorizationProperty V) :
    MonicResidualCoprimeFactorLifting V

theorem not_irreducible_of_factor_natDegree_lt
    {K : Type u} [Field K] {f g h : Polynomial K}
    (hfactor : f = g * h)
    (hgpos : 0 < g.natDegree)
    (hglt : g.natDegree < f.natDegree) :
    ¬ Irreducible f

theorem MonicResidualCoprimeFactorLifting.not_irreducible_map
    {K : Type u} [Field K] {V : ValuationSubring K}
    (hlift : MonicResidualCoprimeFactorLifting V)
    {f : Polynomial V}
    {gbar hbar : Polynomial (IsLocalRing.ResidueField V)}
    (hf : f.Monic) (hgbar : gbar.Monic) (hhbar : hbar.Monic)
    (hfactor : f.map (IsLocalRing.residue V) = gbar * hbar)
    (hcoprime : IsCoprime gbar hbar)
    (hgpos : 0 < gbar.natDegree) (hhpos : 0 < hbar.natDegree) :
    ¬ Irreducible (f.map (algebraMap V K))

theorem MonicResidualCoprimeFactorLifting.irreducible_monic_reduction_coprime_factor_degree_zero
    {K : Type u} [Field K] {V : ValuationSubring K}
    (hlift : MonicResidualCoprimeFactorLifting V)
    {f : Polynomial V}
    {gbar hbar : Polynomial (IsLocalRing.ResidueField V)}
    (hf : f.Monic)
    (hirr : Irreducible (f.map (algebraMap V K)))
    (hgbar : gbar.Monic) (hhbar : hbar.Monic)
    (hfactor : f.map (IsLocalRing.residue V) = gbar * hbar)
    (hcoprime : IsCoprime gbar hbar) :
    gbar.natDegree = 0 ∨ hbar.natDegree = 0

theorem MonicResidualCoprimeFactorLifting.false_of_residue_constant_zero_and_nonzero_root
    {K : Type u} [Field K] {V : ValuationSubring K}
    (hlift : MonicResidualCoprimeFactorLifting V)
    {Q : Polynomial V} (hQmonic : Q.Monic)
    (hQirr : Irreducible (Q.map V.subtype))
    (hconst : (Q.map (IsLocalRing.residue V)).coeff 0 = 0)
    {k' : Type*} [Field k']
    (ρ : IsLocalRing.ResidueField V →+* k')
    {b : k'} (hb0 : b ≠ 0)
    (hroot : ((Q.map (IsLocalRing.residue V)).map ρ).IsRoot b) :
    False

theorem MonicResidualCoprimeFactorLifting.irreducible_roots_same_valuation
    {K L : Type*} [Field K] [Field L] [Algebra K L] [Normal K L]
    {V : ValuationSubring K} (B : ValuationSubring L)
    [V.valuation.HasExtension B.valuation]
    (hlift : MonicResidualCoprimeFactorLifting V)
    {p : Polynomial K} (hp : Irreducible p)
    (hsplit : (p.map (algebraMap K L)).Splits)
    {α β : L}
    (hα : α ∈ (p.map (algebraMap K L)).roots)
    (hβ : β ∈ (p.map (algebraMap K L)).roots) :
    B.valuation α = B.valuation β

theorem henselianRing_of_monicResidualCoprimeFactorLifting
    {K : Type u} [Field K] {V : ValuationSubring K}
    (hlift : MonicResidualCoprimeFactorLifting V) :
    HenselianRing V (IsLocalRing.maximalIdeal V) where
  jac := by
    rw [Ideal.jacobson, le_sInf_iff]
    rintro I ⟨-, hI⟩
    exact (IsLocalRing.eq_maximalIdeal hI).ge
  is_henselian := by
    intro f hf a0 hroot hsimple
    let fbar : Polynomial (IsLocalRing.ResidueField V) :=
      f.map (IsLocalRing.residue V)
    let abar : IsLocalRing.ResidueField V := IsLocalRing.residue V a0
    let lbar : Polynomial (IsLocalRing.ResidueField V) :=
      Polynomial.X - Polynomial.C abar
    let qbar : Polynomial (IsLocalRing.ResidueField V) := fbar /ₘ lbar
    have hlbar : lbar.Monic := Polynomial.monic_X_sub_C abar
    have hresidual : fbar = lbar * qbar := by
      symm
      exact residual_X_sub_C_mul_divByMonic_eq_map_of_eval_mem hroot
    have hfbar : fbar.Monic := hf.map (IsLocalRing.residue V)
    have hqbar : qbar.Monic :=
      hlbar.of_mul_monic_left (hresidual ▸ hfbar)
    have hcoprime : IsCoprime lbar qbar :=
      isCoprime_residual_X_sub_C_divByMonic_of_simpleRoot_mod hsimple
    rcases hlift hf hlbar hqbar hresidual hcoprime with
      ⟨G, H, hG, _hH, hfactor, hGmap, _hHmap⟩
    have hGdegree : G.natDegree = 1 := by
      calc
        G.natDegree = (G.map (IsLocalRing.residue V)).natDegree :=
          (hG.natDegree_map (IsLocalRing.residue V)).symm
        _ = lbar.natDegree := by rw [hGmap]
        _ = 1 := by simp [lbar]
    let a : V := -G.coeff 0
    have hGshape : G = Polynomial.X - Polynomial.C a := by
      rw [hG.eq_X_add_C hGdegree]
      simp [a]
    have haRoot : f.IsRoot a := by
      rw [hfactor, hGshape, Polynomial.IsRoot, Polynomial.eval_mul]
      simp
    have hcoeffmap :
        IsLocalRing.residue V (G.coeff 0) = -abar := by
      have h := congrArg (fun p => p.coeff 0) hGmap
      simpa [lbar, Polynomial.coeff_map] using h
    have haresidue : IsLocalRing.residue V a = abar := by
      dsimp [a]
      rw [map_neg, hcoeffmap]
      simp
    refine ⟨a, haRoot, ?_⟩
    rw [← Ideal.Quotient.eq_zero_iff_mem]
    change IsLocalRing.residue V (a - a0) = 0
    rw [map_sub, haresidue]
    simp [abar]