RadicalConverse.lean

theorem maximalUnramifiedSubextension_separableResidueRootLifts
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
    let T := maximalUnramifiedSubextension v w hExt
    let wT := exponentialValuationRestrict w T
    let hTL : ∀ a : T, w (algebraMap T L a) = wT a := by
      intro a
      rfl
    SeparableResidueRootLifts wT w hTL := by
  classical
  let T := maximalUnramifiedSubextension v w hExt
  let wT := exponentialValuationRestrict w T
  let hKT := exponentialValuationRestrict_extends v w hExt T
  let hTL : ∀ a : T, w (algebraMap T L a) = wT a := by
    intro a
    rfl
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let VT := LubinTate.Valuations.exponentialValuationSubring wT
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let iKT := unramifiedValuationRingValuationRingMap v wT hKT
  let iKL := unramifiedValuationRingValuationRingMap v w hExt
  let : IsLocalHom iKT :=
    unramifiedValuationRingValuationRingMap_isLocalHom v wT hKT
  let : IsLocalHom iKL :=
    unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
  let k := IsLocalRing.ResidueField V
  let kT := IsLocalRing.ResidueField VT
  let ell := IsLocalRing.ResidueField W
  let : Algebra k kT := (IsLocalRing.ResidueField.map iKT).toAlgebra
  let : Algebra k ell := (IsLocalRing.ResidueField.map iKL).toAlgebra
  let g : kT →ₐ[k] ell := restrictedResidueAlgHomToAmbient v w hExt T
  let : Algebra kT ell := g.toAlgebra
  let : IsScalarTower k kT ell :=
    IsScalarTower.of_algebraMap_eq fun x ↦ (g.commutes x).symm
  have hrange : g.fieldRange = separableClosure k ell := by
    simpa [g] using
      maximalUnramifiedSubextension_residue_fieldRange_eq_separableClosure
        v w hExt hhens
  let : Algebra.IsSeparable k kT := ⟨fun x ↦ by
    apply (isSeparable_map_iff g g.injective).mp
    apply mem_separableClosure_iff.mp
    rw [← hrange]
    exact ⟨x, rfl⟩⟩
  change ∀ (y : ell) (P : Polynomial kT), P.Separable →
    (P.map (tameResidueFieldMap wT w hTL)).eval y = 0 →
      ∃ c : kT, tameResidueFieldMap wT w hTL c = y
  intro y P hPsep hPy
  have hmap : tameResidueFieldMap wT w hTL = g.toRingHom := by rfl
  have halg : algebraMap kT ell = g.toRingHom := by rfl
  have hySepT : IsSeparable kT y := by
    apply hPsep.of_dvd (minpoly.dvd kT y ?_)
    rw [Polynomial.aeval_def]
    rw [← Polynomial.eval_map, halg, ← hmap]
    exact hPy
  have hySep : IsSeparable k y :=
    IsSeparable.of_algebra_isSeparable_of_isSeparable k hySepT
  have hyRange : y ∈ g.fieldRange := by
    rw [hrange]
    exact mem_separableClosure_iff.mpr hySep
  rcases hyRange with ⟨c, hc⟩
  refine ⟨c, ?_⟩
  rw [hmap]
  exact hc

theorem separableResidueRootLifts_to_left_in_tower
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a)
    (hlifts : SeparableResidueRootLifts v w hKL) :
    SeparableResidueRootLifts v u hKM

theorem separableResidueRootLifts_to_right_of_surjective_left
    (v : LubinTate.Valuations.ExponentialValuation K)
    (u : LubinTate.Valuations.ExponentialValuation M)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, u (algebraMap K M a) = v a)
    (hML : ∀ a : M, w (algebraMap M L a) = u a)
    (hKL : ∀ a : K, w (algebraMap K L a) = v a)
    (hlifts : SeparableResidueRootLifts v w hKL)
    (hsurj : Function.Surjective (tameResidueFieldMap v u hKM)) :
    SeparableResidueRootLifts u w hML

theorem exponentialRamificationIndex_eq_one_and_residueFieldMap_surjective_of_finrank_eq_one
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hdegree : Module.finrank K L = 1) :
    exponentialRamificationIndex v w = 1 ∧
      Function.Surjective (tameResidueFieldMap v w hExt)

theorem radicalFamily_totalRamified_surjective_coprime_of_separableResidue
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hlifts : SeparableResidueRootLifts v w hExt)
    (r : ℕ) (m : Fin r → ℕ) (a : Fin r → K) (α : Fin r → L)
    (hmpos : ∀ i, 0 < m i)
    (hmcop : ∀ i, Nat.Coprime (m i) (residueCharacteristic v))
    (hpow : ∀ i, α i ^ m i = algebraMap K L (a i))
    (hgen : IntermediateField.adjoin K (Set.range α) = ⊤) :
    exponentialRamificationIndex v w = Module.finrank K L ∧
      Function.Surjective (tameResidueFieldMap v w hExt) ∧
        Nat.Coprime (Module.finrank K L) (residueCharacteristic v)

theorem finiteTamelyRamifiedExtension_of_generatedOverMaximalUnramifiedByRadicals
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hrad : GeneratedOverMaximalUnramifiedByRadicals v w hExt) :
    FiniteTamelyRamifiedExtension v w hExt