HigherRadicalActualFactor.lean

def adjoinRootBaseChangeAlgEquiv
    {A : Type u} {S : Type v}
    [CommRing A] [CommRing S] [Algebra A S]
    (p : A[X]) :
    S ⊗[A] AdjoinRoot p ≃ₐ[S]
      AdjoinRoot (p.map (algebraMap A S))

theorem adjoinRootBaseChangeAlgEquiv_tmul_root
    {A : Type u} {S : Type v}
    [CommRing A] [CommRing S] [Algebra A S]
    (p : A[X]) :
    adjoinRootBaseChangeAlgEquiv p
        (1 ⊗ₜ[A] AdjoinRoot.root p) =
      AdjoinRoot.root (p.map (algebraMap A S))

def adjoinRootGenericFactorAlgEquiv
    {A : Type u} {K : Type v} [CommRing A] [Field K] [Algebra A K]
    (p : A[X]) {E : Type w} [Field E] [Algebra K E]
    (e : AdjoinRoot (p.map (algebraMap A K)) ≃ₐ[K] E) :
    K ⊗[A] AdjoinRoot p ≃ₐ[K] E

theorem adjoinRootGenericFactorAlgEquiv_tmul_root
    {A : Type u} {K : Type v} [CommRing A] [Field K] [Algebra A K]
    (p : A[X]) {E : Type w} [Field E] [Algebra K E]
    (e : AdjoinRoot (p.map (algebraMap A K)) ≃ₐ[K] E) :
    adjoinRootGenericFactorAlgEquiv p e
        (1 ⊗ₜ[A] AdjoinRoot.root p) =
      e (AdjoinRoot.root (p.map (algebraMap A K)))

def pureRadicalGenericFiberAlgEquiv
    {A : Type u} {K : Type v} {Omega : Type w}
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [Field Omega]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K Omega]
    {n : ℕ} (hn : 0 < n) (t : A) (ht : Prime t)
    (beta : Omega)
    (hbetaPow : beta ^ n =
      algebraMap K Omega (algebraMap A K t)) :
    K ⊗[A] AdjoinRoot (X ^ n - C t) ≃ₐ[K]
      IntermediateField.adjoin K ({beta} : Set Omega)

theorem pureRadicalGenericFiberAlgEquiv_tmul_root
    {A : Type u} {K : Type v} {Omega : Type w}
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [Field Omega]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K Omega]
    {n : ℕ} (hn : 0 < n) (t : A) (ht : Prime t)
    (beta : Omega)
    (hbetaPow : beta ^ n =
      algebraMap K Omega (algebraMap A K t)) :
    pureRadicalGenericFiberAlgEquiv hn t ht beta hbetaPow
        (1 ⊗ₜ[A] AdjoinRoot.root (X ^ n - C t)) =
      IntermediateField.AdjoinSimple.gen K beta

def lowerRadicalField
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (e N : ℕ) (beta : Omega) :
    IntermediateField K Omega

def targetCompositumOverLowerRadical
    {K : Type u} {L Omega : Type v}
    [Field K] [Field L] [Field Omega]
    [Algebra K L] [Algebra L Omega] [Algebra K Omega]
    [IsScalarTower K L Omega]
    (e N : ℕ) (beta : Omega) :
    let F := lowerRadicalField (K := K) e N beta
    IntermediateField F Omega := by
  let F := lowerRadicalField (K := K) e N beta
  let Limage : IntermediateField K Omega :=
    (IsScalarTower.toAlgHom K L Omega).fieldRange
  exact (Limage ⊔ F).toSubfield.toIntermediateField
    (fun z ↦ (show F ≤ Limage ⊔ F from le_sup_right) z.2)

def higherRadicalFieldOverLower
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (e N : ℕ) (beta : Omega) :
    let F := lowerRadicalField (K := K) e N beta
    IntermediateField F Omega := by
  let F := lowerRadicalField (K := K) e N beta
  let Kₙ : IntermediateField K Omega :=
    IntermediateField.adjoin K ({beta} : Set Omega)
  have hF : F.toSubfield ≤ Kₙ.toSubfield := by
    dsimp only [F, lowerRadicalField]
    change IntermediateField.adjoin K
      ({beta ^ (N / e)} : Set Omega) ≤ Kₙ
    rw [IntermediateField.adjoin_le_iff]
    intro z hz
    rw [Set.mem_singleton_iff.mp hz]
    exact Kₙ.toSubfield.pow_mem
      (IntermediateField.subset_adjoin K ({beta} : Set Omega)
        (Set.mem_singleton beta)) (N / e)
  exact Kₙ.toSubfield.toIntermediateField (fun z ↦ hF z.2)

theorem targetCompositumOverLowerRadical_restrictScalars
    {K : Type u} {L Omega : Type v}
    [Field K] [Field L] [Field Omega]
    [Algebra K L] [Algebra L Omega] [Algebra K Omega]
    [IsScalarTower K L Omega]
    (e N : ℕ) (beta : Omega) :
    (targetCompositumOverLowerRadical
        (K := K) (L := L) e N beta).restrictScalars K =
      (IsScalarTower.toAlgHom K L Omega).fieldRange ⊔
        lowerRadicalField (K := K) e N beta

theorem higherRadicalFieldOverLower_restrictScalars
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (e N : ℕ) (beta : Omega) :
    (higherRadicalFieldOverLower
        (K := K) e N beta).restrictScalars K =
      IntermediateField.adjoin K ({beta} : Set Omega)

theorem intermediateField_coe_pow
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (F : IntermediateField K Omega)
    (z : F) (n : ℕ) :
    ((z ^ n : F) : Omega) = (z : Omega) ^ n

theorem intermediateField_coe_algebraMap
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (F : IntermediateField K Omega)
    (E : IntermediateField F Omega) (z : F) :
    ((algebraMap F E z : E) : Omega) = (z : Omega)

theorem intermediateField_coe_pow_eq_algebraMap_of_eq
    {K : Type u} {Omega : Type v} [Field K] [Field Omega]
    [Algebra K Omega] (F : IntermediateField K Omega)
    (E : IntermediateField F Omega) (x : E) (y : F)
    (n : ℕ) (beta : Omega)
    (hx : (x : Omega) = beta) (hy : (y : Omega) = beta ^ n) :
    ((x ^ n : E) : Omega) = ((algebraMap F E y : E) : Omega)

theorem adjoinRoot_ringHom_eq_of_comp_subtype_eq
    {A : Type u} {E Omega : Type v}
    [CommRing A] [CommRing E] [CommRing Omega]
    (p : A[X]) (i : E →+* Omega) (hi : Function.Injective i)
    (f g : AdjoinRoot p →+* E)
    (hcoeff : ∀ z : A,
      i (f (algebraMap A (AdjoinRoot p) z)) =
        i (g (algebraMap A (AdjoinRoot p) z)))
    (hroot : i (f (AdjoinRoot.root p)) = i (g (AdjoinRoot.root p))) :
    f = g

theorem higherRoot_genericMaps_comp_eq
    {A K : Type u} {Omega : Type v}
    [CommRing A] [Field K] [Field Omega] [Algebra K Omega]
    (F : IntermediateField K Omega) (K' : IntermediateField F Omega)
    {e N : ℕ} (a : A) (hdiv : e ∣ N)
    (fN : AdjoinRoot (X ^ N - C a) →+* K')
    (fE : AdjoinRoot (X ^ e - C a) →+* F)
    (hcoeff : ∀ z : A,
      ((fN (algebraMap A (AdjoinRoot (X ^ N - C a)) z) : K') : Omega) =
        ((algebraMap F K'
          (fE (algebraMap A (AdjoinRoot (X ^ e - C a)) z)) : K') : Omega))
    (beta alpha : Omega)
    (hNroot : ((fN (AdjoinRoot.root (X ^ N - C a)) : K') : Omega) = beta)
    (hEroot : ((fE (AdjoinRoot.root (X ^ e - C a)) : F) : Omega) = alpha)
    (halpha : beta ^ (N / e) = alpha) :
    fN.comp (adjoinRootPowerMapOfDvd hdiv a).toRingHom =
      (algebraMap F K').comp fE

theorem unitFactor_genericMaps_comp_eq
    {A : Type u} {W F E Omega : Type v}
    [CommRing A] [CommRing W] [CommRing F] [CommRing E] [CommRing Omega]
    {e : ℕ} (a : A) (pi : W) (q : W[X])
    (radicalMap : AdjoinRoot (X ^ e - C a) →+* AdjoinRoot q)
    (fCq : AdjoinRoot q →+* E)
    (fRe : AdjoinRoot (X ^ e - C a) →+* F)
    (j : F →+* E) (i : E →+* Omega) (hi : Function.Injective i)
    (hcoeff : ∀ z : A,
      i (fCq (radicalMap (algebraMap A
        (AdjoinRoot (X ^ e - C a)) z))) =
      i (j (fRe (algebraMap A
        (AdjoinRoot (X ^ e - C a)) z))))
    (delta alpha piOmega : Omega)
    (hRadicalRoot :
      radicalMap (AdjoinRoot.root (X ^ e - C a)) =
        AdjoinRoot.root q * algebraMap W (AdjoinRoot q) pi)
    (hCqRoot : i (fCq (AdjoinRoot.root q)) = delta)
    (hCqCoeff : i (fCq (algebraMap W (AdjoinRoot q) pi)) = piOmega)
    (hReRoot :
      i (j (fRe (AdjoinRoot.root (X ^ e - C a)))) = alpha)
    (halpha : alpha = delta * piOmega) :
    fCq.comp radicalMap = j.comp fRe

def higherRadicalActualCompositumField
    {K : Type u} {L Omega : Type v}
    [Field K] [Field L] [Field Omega]
    [Algebra K L] [Algebra L Omega] [Algebra K Omega]
    [IsScalarTower K L Omega]
    (e N : ℕ) (beta : Omega) :
    let F := lowerRadicalField (K := K) e N beta
    IntermediateField F Omega :=
  targetCompositumOverLowerRadical (K := K) (L := L) e N beta ⊔
    higherRadicalFieldOverLower (K := K) e N beta

theorem higherRadicalActualCompositumField_restrictScalars
    {K : Type u} {L Omega : Type v}
    [Field K] [Field L] [Field Omega]
    [Algebra K L] [Algebra L Omega] [Algebra K Omega]
    [IsScalarTower K L Omega]
    (e N : ℕ) (beta : Omega) :
    (higherRadicalActualCompositumField
        (K := K) (L := L) e N beta).restrictScalars K =
      (IsScalarTower.toAlgHom K L Omega).fieldRange ⊔
        IntermediateField.adjoin K ({beta} : Set Omega)

theorem finiteDimensional_of_finite_valuationSubrings
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring] :
    FiniteDimensional K L

theorem finiteDimensional_targetCompositumOverLowerRadical
    {K : Type u} {L Omega : Type v}
    [Field K] [Field L] [Field Omega]
    [Algebra K L] [Algebra L Omega] [Algebra K Omega]
    [IsScalarTower K L Omega] [FiniteDimensional K L]
    (e N : ℕ) (beta : Omega) :
    let F := lowerRadicalField (K := K) e N beta
    let E := targetCompositumOverLowerRadical
      (K := K) (L := L) e N beta
    FiniteDimensional F E := by
  let F := lowerRadicalField (K := K) e N beta
  let Limage : IntermediateField K Omega :=
    (IsScalarTower.toAlgHom K L Omega).fieldRange
  let E := targetCompositumOverLowerRadical
    (K := K) (L := L) e N beta
  let : FiniteDimensional K Limage :=
    Module.Finite.equiv
      (IsScalarTower.toAlgHom K L Omega).equivFieldRange.toLinearEquiv
  let eSupE : (Limage ⊔ F : IntermediateField K Omega) ≃ₐ[F] E :=
    { toFun := fun z ↦ ⟨z.1, z.2⟩
      invFun := fun z ↦ ⟨z.1, z.2⟩
      left_inv := fun _ ↦ rfl
      right_inv := fun _ ↦ rfl
      map_mul' _ _ := rfl
      map_add' _ _ := rfl
      commutes' := fun _ ↦ rfl }
  let : FiniteDimensional F
      (Limage ⊔ F : IntermediateField K Omega) :=
    DiscreteValuationField.FieldCompositum.finiteDimensional_sup_over_right_of_left
      Limage F
  exact Module.Finite.equiv eSupE.toLinearEquiv

structure HigherRadicalActualFactorData
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    (varpi : base.valuationSubring) (N : ℕ)
    (beta : AlgebraicClosure L) where
  /-- The prescribed higher root ring maps into its actual compositum field. -/
  rootMap :
    AdjoinRoot (X ^ N - C varpi) →+*
      higherRadicalActualCompositumField
        (K := K) (L := L) (ramificationIndex base target) N beta
  /-- The root map agrees with the original embedding of the base valuation ring. -/
  commutes_coe (z : base.valuationSubring) :
    ((rootMap (algebraMap base.valuationSubring
        (AdjoinRoot (X ^ N - C varpi)) z) :
          higherRadicalActualCompositumField
            (K := K) (L := L) (ramificationIndex base target) N beta) :
        AlgebraicClosure L) =
      algebraMap K (AlgebraicClosure L) (z : K)
  /-- The distinguished higher root maps to the prescribed root `beta`. -/
  root_coe :
    ((rootMap (AdjoinRoot.root (X ^ N - C varpi)) :
        higherRadicalActualCompositumField
          (K := K) (L := L) (ramificationIndex base target) N beta) :
      AlgebraicClosure L) = beta
  /-- The normalization of the higher root ring in its actual compositum is etale. -/
  etale_normalization :
    let Rn := AdjoinRoot (X ^ N - C varpi)
    let M := higherRadicalActualCompositumField
      (K := K) (L := L) (ramificationIndex base target) N beta
    letI : Algebra Rn M := rootMap.toAlgebra
    Algebra.Etale Rn (integralClosure Rn M)

structure HigherRadicalUnitFactorData
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    (varpi : base.valuationSubring)
    (pi : target.valuationSubring) (N : ℕ)
    (beta : AlgebraicClosure L) where
  /-- The unit absorbed from the lower radical inside the fixed algebraic closure. -/
  delta : AlgebraicClosure L
  /-- The integral polynomial defining the selected unit factor. -/
  q : target.valuationSubring[X]
  /-- The generic unit factor identifies with the field generated by `delta`. -/
  unitFactorEquiv :
    AdjoinRoot (q.map (algebraMap target.valuationSubring L)) ≃ₐ[L]
      IntermediateField.adjoin L ({delta} : Set (AlgebraicClosure L))
  /-- The lower radical ring maps into the integral unit factor. -/
  radicalToUnitFactor :
    AdjoinRoot
        (X ^ ramificationIndex base target - C varpi) →ₐ[base.valuationSubring]
      AdjoinRoot q
  /-- The prescribed lower radical is the absorbed unit times the target uniformizer. -/
  alpha_eq :
    beta ^ (N / ramificationIndex base target) =
      delta * algebraMap L (AlgebraicClosure L) (pi : L)
  /-- The selected integral polynomial is monic. -/
  q_monic : q.Monic
  /-- The generic polynomial is the minimal polynomial of the absorbed unit. -/
  q_map :
    q.map (algebraMap target.valuationSubring L) = minpoly L delta
  /-- The integral unit factor is etale over the target valuation ring. -/
  q_etale : Algebra.Etale target.valuationSubring (AdjoinRoot q)
  /-- The integral unit factor is finite over the target valuation ring. -/
  q_finite : Module.Finite target.valuationSubring (AdjoinRoot q)
  /-- The field generated by the absorbed unit is the actual lower radical compositum. -/
  compositum_eq :
    (IntermediateField.adjoin L
        ({delta} : Set (AlgebraicClosure L))).restrictScalars K =
      (IsScalarTower.toAlgHom K L
          (AlgebraicClosure L)).fieldRange ⊔
        IntermediateField.adjoin K
          ({beta ^ (N / ramificationIndex base target)} :
            Set (AlgebraicClosure L))
  /-- The generic unit factor sends its distinguished root to `delta`. -/
  unitFactor_root :
    unitFactorEquiv
        (AdjoinRoot.root
          (q.map (algebraMap target.valuationSubring L))) =
      IntermediateField.AdjoinSimple.gen L delta
  /-- The lower radical root maps to the unit factor root times the target uniformizer. -/
  radical_root :
    radicalToUnitFactor
        (AdjoinRoot.root
          (X ^ ramificationIndex base target - C varpi)) =
      AdjoinRoot.root q *
        algebraMap target.valuationSubring (AdjoinRoot q) pi
  /-- The unit factor is etale over the lower radical ring through the recorded map. -/
  radical_etale :
    let Rₑ := AdjoinRoot
      (X ^ ramificationIndex base target - C varpi)
    let Cq := AdjoinRoot q
    letI : Algebra Rₑ Cq :=
      radicalToUnitFactor.toRingHom.toAlgebra
    Algebra.Etale Rₑ Cq

def lowerUnitFactorGenericFiberAlgEquiv
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (pi : target.valuationSubring) (N : ℕ)
    (beta : AlgebraicClosure L)
    (he : 0 < ramificationIndex base target)
    (hvarpiPrime : Prime varpi)
    (halphaPow :
      (beta ^ (N / ramificationIndex base target)) ^
          ramificationIndex base target =
        algebraMap K (AlgebraicClosure L) (varpi : K))
    (factor : HigherRadicalUnitFactorData base target varpi pi N beta) :
    let V := base.valuationSubring
    let e := ramificationIndex base target
    let alpha : AlgebraicClosure L := beta ^ (N / e)
    let Rₑ := AdjoinRoot (X ^ e - C varpi)
    let Cq := AdjoinRoot factor.q
    let F : IntermediateField K (AlgebraicClosure L) :=
      IntermediateField.adjoin K ({alpha} : Set (AlgebraicClosure L))
    let E : IntermediateField F (AlgebraicClosure L) :=
      targetCompositumOverLowerRadical (K := K) (L := L) e N beta
    letI : IsFractionRing V K := base.valuationSubring_isFractionRing
    letI : IsIntegrallyClosed V := base.valuationSubring_isIntegrallyClosed
    letI : Algebra V F :=
      ((algebraMap K F).comp (algebraMap V K)).toAlgebra
    letI : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
    let eRₑ : (K ⊗[V] Rₑ) ≃ₐ[K] F :=
      pureRadicalGenericFiberAlgEquiv he varpi hvarpiPrime alpha halphaPow
    letI : Algebra Rₑ F :=
      (genericFiberRightAlgHom eRₑ).toRingHom.toAlgebra
    letI : Algebra Rₑ Cq :=
      factor.radicalToUnitFactor.toRingHom.toAlgebra
    (F ⊗[Rₑ] Cq) ≃ₐ[F] E := by
  let V := base.valuationSubring
  let W := target.valuationSubring
  let e := ramificationIndex base target
  let alpha : AlgebraicClosure L := beta ^ (N / e)
  let Rₑ := AdjoinRoot (X ^ e - C varpi)
  let Cq := AdjoinRoot factor.q
  let F : IntermediateField K (AlgebraicClosure L) :=
    IntermediateField.adjoin K ({alpha} : Set (AlgebraicClosure L))
  let E₀ : IntermediateField L (AlgebraicClosure L) :=
    IntermediateField.adjoin L
      ({factor.delta} : Set (AlgebraicClosure L))
  let E : IntermediateField F (AlgebraicClosure L) :=
    targetCompositumOverLowerRadical (K := K) (L := L) e N beta
  letI : Algebra F E := E.algebra
  let Limage : IntermediateField K (AlgebraicClosure L) :=
    (IsScalarTower.toAlgHom K L (AlgebraicClosure L)).fieldRange
  let lToE : L →ₐ[K] E :=
    { toFun := fun z ↦ ⟨algebraMap L (AlgebraicClosure L) z, by
          change algebraMap L (AlgebraicClosure L) z ∈ Limage ⊔ F
          exact SetLike.coe_mono
            (show Limage ≤ Limage ⊔ F from le_sup_left)
            (AlgHom.mem_fieldRange.mpr ⟨z, rfl⟩)⟩
      map_one' := by apply Subtype.ext; simp
      map_zero' := by apply Subtype.ext; simp
      map_add' _ _ := by apply Subtype.ext; simp
      map_mul' _ _ := by apply Subtype.ext; simp
      commutes' := fun z ↦ by
        apply Subtype.ext
        exact IsScalarTower.algebraMap_apply K L (AlgebraicClosure L) z }
  letI : Algebra L E := lToE.toRingHom.toAlgebra
  letI : IsScalarTower K L E :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  have hCompositum' : E₀.restrictScalars K = Limage ⊔ F := by
    simpa [E₀, Limage, F, alpha, e] using factor.compositum_eq
  let eE : E₀ ≃ₐ[L] E :=
    { toFun := fun z ↦ ⟨z.1, by
          change z.1 ∈ Limage ⊔ F
          rw [← hCompositum']
          exact z.2⟩
      invFun := fun z ↦ ⟨z.1, by
          have hz : z.1 ∈ Limage ⊔ F := z.2
          rw [← hCompositum'] at hz
          exact hz⟩
      left_inv := fun _ ↦ rfl
      right_inv := fun _ ↦ rfl
      map_mul' _ _ := rfl
      map_add' _ _ := rfl
      commutes' := fun _ ↦ rfl }
  have hqIrreducibleMap :
      Irreducible (factor.q.map (algebraMap W L)) := by
    rw [factor.q_map]
    exact minpoly.irreducible
      (Algebra.IsIntegral.isIntegral factor.delta)
  have hqIrreducible : Irreducible factor.q :=
    (factor.q_monic.irreducible_iff_irreducible_map_fraction_map).2
      hqIrreducibleMap
  letI : IsDomain Cq := AdjoinRoot.isDomain_of_prime hqIrreducible.prime
  let eCq : (L ⊗[W] Cq) ≃ₐ[L] E :=
    (adjoinRootGenericFactorAlgEquiv factor.q
      factor.unitFactorEquiv).trans eE
  letI : Algebra Cq E :=
    (genericFiberRightAlgHom eCq).toRingHom.toAlgebra
  letI : IsFractionRing Cq E :=
    isFractionRing_of_genericFiberAlgEquiv eCq
  letI : IsFractionRing V K := base.valuationSubring_isFractionRing
  letI : IsIntegrallyClosed V := base.valuationSubring_isIntegrallyClosed
  letI : Algebra V F :=
    ((algebraMap K F).comp (algebraMap V K)).toAlgebra
  letI : IsScalarTower V K F := IsScalarTower.of_algebraMap_eq' rfl
  let eRₑ : (K ⊗[V] Rₑ) ≃ₐ[K] F :=
    pureRadicalGenericFiberAlgEquiv he varpi hvarpiPrime alpha halphaPow
  letI : IsDomain Rₑ :=
    isDomain_adjoinRoot_X_pow_sub_C_of_prime he varpi hvarpiPrime
  letI : Algebra Rₑ F :=
    (genericFiberRightAlgHom eRₑ).toRingHom.toAlgebra
  letI : IsFractionRing Rₑ F :=
    isFractionRing_of_genericFiberAlgEquiv eRₑ
  let radicalMap : Rₑ →ₐ[V] Cq := factor.radicalToUnitFactor
  letI : Algebra Rₑ Cq := radicalMap.toRingHom.toAlgebra
  letI : Algebra Rₑ E :=
    ((algebraMap F E).comp (algebraMap Rₑ F)).toAlgebra
  letI : IsScalarTower Rₑ F E := IsScalarTower.of_algebraMap_eq' rfl
  have hCqRoot :
      (((genericFiberRightAlgHom eCq) (AdjoinRoot.root factor.q) : E) :
        AlgebraicClosure L) = factor.delta := by
    change ((eE ((adjoinRootGenericFactorAlgEquiv factor.q
        factor.unitFactorEquiv)
        (1 ⊗ₜ[W] AdjoinRoot.root factor.q)) : E) :
      AlgebraicClosure L) = factor.delta
    rw [adjoinRootGenericFactorAlgEquiv_tmul_root,
      factor.unitFactor_root]
    rfl
  have hCqCoeff :
      (((genericFiberRightAlgHom eCq)
          (algebraMap W Cq pi) : E) : AlgebraicClosure L) =
        algebraMap L (AlgebraicClosure L) (pi : L) := by
    rw [(genericFiberRightAlgHom eCq).commutes]
    rfl
  have hRₑRoot :
      (((genericFiberRightAlgHom eRₑ)
          (AdjoinRoot.root (X ^ e - C varpi)) : F) :
        AlgebraicClosure L) = alpha := by
    change (((pureRadicalGenericFiberAlgEquiv he varpi hvarpiPrime alpha
        halphaPow) (1 ⊗ₜ[V] AdjoinRoot.root (X ^ e - C varpi)) :
      IntermediateField.adjoin K ({alpha} : Set (AlgebraicClosure L))) :
        AlgebraicClosure L) = alpha
    exact congrArg Subtype.val
      (pureRadicalGenericFiberAlgEquiv_tmul_root
        he varpi hvarpiPrime alpha halphaPow)
  have hCqBase (z : V) :
      (((genericFiberRightAlgHom eCq)
          (radicalMap (algebraMap V Rₑ z)) : E) :
        AlgebraicClosure L) =
      algebraMap K (AlgebraicClosure L) (z : K) := by
    rw [radicalMap.commutes]
    change (((genericFiberRightAlgHom eCq)
        (algebraMap W Cq (integerMap base target z)) : E) :
      AlgebraicClosure L) =
        algebraMap K (AlgebraicClosure L) (z : K)
    rw [(genericFiberRightAlgHom eCq).commutes]
    rfl
  have hRₑBase (z : V) :
      ((algebraMap F E ((genericFiberRightAlgHom eRₑ)
          (algebraMap V Rₑ z)) : E) : AlgebraicClosure L) =
        algebraMap K (AlgebraicClosure L) (z : K) := by
    rw [(genericFiberRightAlgHom eRₑ).commutes]
    rfl
  have hTowerRₑCqE :
      (genericFiberRightAlgHom eCq).toRingHom.comp radicalMap.toRingHom =
        (algebraMap F E).comp (genericFiberRightAlgHom eRₑ).toRingHom := by
    apply unitFactor_genericMaps_comp_eq varpi pi factor.q
      radicalMap.toRingHom
      (genericFiberRightAlgHom eCq).toRingHom
      (genericFiberRightAlgHom eRₑ).toRingHom
      (algebraMap F E) E.toSubfield.subtype
      E.toSubfield.subtype.injective
      (fun z ↦ hCqBase z |>.trans (hRₑBase z).symm)
      factor.delta alpha
      (algebraMap L (AlgebraicClosure L) (pi : L))
      factor.radical_root hCqRoot hCqCoeff
    · change (((genericFiberRightAlgHom eRₑ)
          (AdjoinRoot.root (X ^ e - C varpi)) : F) :
        AlgebraicClosure L) = alpha
      exact hRₑRoot
    · exact factor.alpha_eq
  letI : IsScalarTower Rₑ Cq E :=
    IsScalarTower.of_algebraMap_eq fun z ↦ by
      exact DFunLike.congr_fun hTowerRₑCqE z |>.symm
  letI : Module.Finite V Rₑ :=
    (monic_X_pow_sub_C varpi he.ne').finite_adjoinRoot
  letI : Module.Finite W Cq := factor.q_finite
  letI : Module.Finite V Cq := Module.Finite.trans W Cq
  letI : IsScalarTower V Rₑ Cq :=
    IsScalarTower.of_algebraMap_eq fun z ↦
      (radicalMap.commutes z).symm
  letI : Module.Finite Rₑ Cq :=
    Module.Finite.of_restrictScalars_finite V Rₑ Cq
  exact finiteGenericFiberAlgEquiv

theorem higherRadicalUnitFactorData
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (pi : target.valuationSubring)
    (unit : target.valuationSubringˣ)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hdecomp :
      integerMap base target varpi =
        (unit : target.valuationSubring) *
          pi ^ ramificationIndex base target)
    (N : ℕ) (hdiv : ramificationIndex base target ∣ N)
    (beta : AlgebraicClosure L)
    (hbetaPow :
      beta ^ N = algebraMap K (AlgebraicClosure L) (varpi : K)) :
    Nonempty (HigherRadicalUnitFactorData
      base target varpi pi N beta)

theorem higherRadicalActualFactorData_of_unitFactorData
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (pi : target.valuationSubring)
    (N : ℕ) (hdiv : ramificationIndex base target ∣ N)
    (beta : AlgebraicClosure L)
    (hbetaPow :
      beta ^ N = algebraMap K (AlgebraicClosure L) (varpi : K))
    (factor : HigherRadicalUnitFactorData base target varpi pi N beta) :
    Nonempty (HigherRadicalActualFactorData base target varpi N beta)

theorem higherRadicalActualFactorData
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (pi : target.valuationSubring)
    (unit : target.valuationSubringˣ)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hdecomp :
      integerMap base target varpi =
        (unit : target.valuationSubring) *
          pi ^ ramificationIndex base target)
    (N : ℕ) (hdiv : ramificationIndex base target ∣ N)
    (beta : AlgebraicClosure L)
    (hbetaPow :
      beta ^ N = algebraMap K (AlgebraicClosure L) (varpi : K)) :
    Nonempty (HigherRadicalActualFactorData base target varpi N beta)