CompositumValueGroup.lean

theorem sup_eq_sup_sup_of_le
    (A B R : AddSubgroup ℝ) (hAB : A ≤ B) :
    B ⊔ R = (A ⊔ R) ⊔ B

theorem bookExponentialValueSubgroup_commonTop_eq_sup_of_finiteTame
    {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω]
    [Algebra.IsAlgebraic K Ω]
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation Ω)
    (hExt : ∀ a : K, w (algebraMap K Ω a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hTame : FiniteTamelyRamifiedExtension v
      (exponentialValuationRestrict w L)
      (exponentialValuationRestrict_extends v w hExt L)) :
    let Top := (L ⊔ K' : IntermediateField K Ω)
    let wLeft := exponentialValuationRestrict w L
    let wRight := exponentialValuationRestrict w K'
    let wTop := exponentialValuationRestrict w Top
    exponentialValueSubgroup wTop =
      exponentialValueSubgroup wLeft ⊔ exponentialValueSubgroup wRight := by
  classical
  let Top := (L ⊔ K' : IntermediateField K Ω)
  let wLeft := exponentialValuationRestrict w L
  let wRight := exponentialValuationRestrict w K'
  let wTop := exponentialValuationRestrict w Top
  let hLeft : ∀ a : K,
      wLeft (algebraMap K L a) = v a :=
    exponentialValuationRestrict_extends v w hExt L
  let hBaseRight : ∀ a : K,
      wRight (algebraMap K K' a) = v a :=
    exponentialValuationRestrict_extends v w hExt K'
  let hRightTop : ∀ a : K',
      wTop (algebraMap K' Top a) = wRight a := by
    intro a
    rfl
  let : FiniteDimensional K' Top :=
    finiteDimensional_sup_over_right_of_left L K'
  let T := maximalUnramifiedSubextension v wLeft hLeft
  let wT := exponentialValuationRestrict wLeft T
  let hKT : ∀ a : K, wT (algebraMap K T a) = v a :=
    exponentialValuationRestrict_extends v wLeft hLeft T
  let hTLeft : ∀ a : T,
      wLeft (algebraMap T L a) = wT a := by
    intro a
    rfl
  let TTop := maximalUnramifiedSubextension wRight wTop hRightTop
  let wTTop := exponentialValuationRestrict wTop TTop
  let hRightTTop : ∀ a : K',
      wTTop (algebraMap K' TTop a) = wRight a :=
    exponentialValuationRestrict_extends
      wRight wTop hRightTop TTop
  let hTTopTop : ∀ a : TTop,
      wTop (algebraMap TTop Top a) = wTTop a := by
    intro a
    rfl
  have hhensT : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring wT).valuation :=
    henselianValuation_of_algebraic_extension v wT hKT hhens
  have hcharT : residueCharacteristic v = residueCharacteristic wT :=
    residueCharacteristic_eq_of_exact_extension v wT hKT
  have hpT : PositiveResidueCharacteristic wT := by
    change residueCharacteristic wT ≠ 0
    rw [← hcharT]
    exact hTame.1
  have hresTLeft : Function.Surjective
      (tameResidueFieldMap wT wLeft hTLeft) :=
    maximalUnramifiedSubextension_residueMap_surjective_of_separable
      v wLeft hLeft hhens hTame.2.1
  have hhensRight : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring wRight).valuation :=
    henselianValuation_of_algebraic_extension
      v wRight hBaseRight hhens
  have hTameTop : FiniteTamelyRamifiedExtension
      wRight wTop hRightTop :=
    finiteTamelyRamifiedExtension_commonTop_of_baseChange
      L K' v w hExt hhens hTame
  have hhensTTop : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring wTTop).valuation :=
    henselianValuation_of_algebraic_extension
      wRight wTTop hRightTTop hhensRight
  have hcharTTop : residueCharacteristic wRight =
      residueCharacteristic wTTop :=
    residueCharacteristic_eq_of_exact_extension
      wRight wTTop hRightTTop
  have hpTTop : PositiveResidueCharacteristic wTTop := by
    change residueCharacteristic wTTop ≠ 0
    rw [← hcharTTop]
    exact hTameTop.1
  have hresTTopTop : Function.Surjective
      (tameResidueFieldMap wTTop wTop hTTopTop) :=
    maximalUnramifiedSubextension_residueMap_surjective_of_separable
      wRight wTop hRightTop hhensRight hTameTop.2.1
  have hrad : GeneratedOverMaximalUnramifiedByRadicals
      v wLeft hLeft :=
    generatedOverMaximalUnramifiedByRadicals_of_finiteTame
      v wLeft hLeft hhens hTame
  change GeneratedByRadicalsPrimeTo T (residueCharacteristic v) at hrad
  rcases hrad with
    ⟨r, m, a, alpha, hmpos, hmcop, hpow, hgen⟩
  have hmcopT : ∀ i, Nat.Coprime (m i)
      (residueCharacteristic wT) := by
    intro i
    rw [← hcharT]
    exact hmcop i
  let : FiniteDimensional T L := inferInstance
  have hvalueLeft : exponentialValueSubgroup wLeft =
      exponentialValueSubgroup wT ⊔
        ⨆ i, AddSubgroup.zmultiples (wLeft (alpha i)).untop₀ :=
    bookExponentialValueSubgroup_eq_sup_iSup_zmultiples_of_radical_family
      wT wLeft hTLeft hhensT hpT hresTLeft r m a alpha
        hmpos hmcopT hpow hgen
  let iL : L →ₐ[K] Top :=
    IntermediateField.inclusion (show L ≤ Top from le_sup_left)
  have haTopMem (i : Fin r) : iL (a i : L) ∈ TTop :=
    maximalUnramifiedSubextension_mem_commonTop_maximal
      L K' v w hExt hhens (a i)
  let aTop : Fin r → TTop := fun i => ⟨iL (a i : L), haTopMem i⟩
  let alphaTop : Fin r → Top := fun i => iL (alpha i)
  have hpowTop (i : Fin r) :
      alphaTop i ^ m i = algebraMap TTop Top (aTop i) := by
    change iL (alpha i) ^ m i = algebraMap TTop Top (aTop i)
    rw [← map_pow, hpow i]
    rfl
  have hgenAlg : Algebra.adjoin T (Set.range alpha) =
      (⊤ : Subalgebra T L) := by
    let : Algebra.IsAlgebraic T L :=
      Algebra.IsAlgebraic.of_finite T L
    exact Algebra.adjoin_eq_top_of_intermediateField
      (fun x _hx => Algebra.IsAlgebraic.isAlgebraic x) hgen
  let S : Subalgebra TTop Top :=
    Algebra.adjoin TTop (Set.range alphaTop)
  have hS : S = ⊤ := by
    apply Algebra.eq_top_iff.2
    intro z
    have hz : z ∈ Algebra.adjoin K' (Set.range iL) := by
      rw [sup_right_adjoin_left_range_eq_top
        (K := K) (Ω := Ω) L K']
      trivial
    exact Algebra.adjoin_induction
      (R := K') (A := Top) (s := Set.range iL)
      (p := fun y _hy => y ∈ S)
      (fun y hy => by
        rcases hy with ⟨x, rfl⟩
        have hx : x ∈ Algebra.adjoin T (Set.range alpha) := by
          rw [hgenAlg]
          trivial
        exact Algebra.adjoin_induction
          (R := T) (A := L) (s := Set.range alpha)
          (p := fun y _hy => iL y ∈ S)
          (fun y hy => by
            rcases hy with ⟨i, rfl⟩
            exact Algebra.subset_adjoin ⟨i, rfl⟩)
          (fun t => by
            let tTop : TTop :=
              ⟨iL (t : L),
                maximalUnramifiedSubextension_mem_commonTop_maximal
                  L K' v w hExt hhens t⟩
            have ht : iL (algebraMap T L t) =
                algebraMap TTop Top tTop := by
              rfl
            change iL (algebraMap T L t) ∈ S
            rw [ht]
            exact S.algebraMap_mem tTop)
          (fun y1 y2 _ _ hy1 hy2 => by
            simpa [map_add] using S.add_mem hy1 hy2)
          (fun y1 y2 _ _ hy1 hy2 => by
            simpa [map_mul] using S.mul_mem hy1 hy2) hx)
      (fun b => by
        let bTop : TTop := algebraMap K' TTop b
        have hb : algebraMap K' Top b =
            algebraMap TTop Top bTop := by
          exact (IsScalarTower.algebraMap_apply K' TTop Top b).symm
        change algebraMap K' Top b ∈ S
        rw [hb]
        exact S.algebraMap_mem bTop)
      (fun y1 y2 _ _ hy1 hy2 => S.add_mem hy1 hy2)
      (fun y1 y2 _ _ hy1 hy2 => S.mul_mem hy1 hy2) hz
  have hgenTop : IntermediateField.adjoin TTop
      (Set.range alphaTop) =
      (⊤ : IntermediateField TTop Top) := by
    let : FiniteDimensional TTop Top := inferInstance
    let : Algebra.IsAlgebraic TTop Top :=
      Algebra.IsAlgebraic.of_finite TTop Top
    exact (IntermediateField.adjoin_eq_top_iff).2 hS
  have hmcopTTop : ∀ i, Nat.Coprime (m i)
      (residueCharacteristic wTTop) := by
    intro i
    rw [← hcharTTop]
    have hcharRight : residueCharacteristic v = residueCharacteristic wRight :=
      residueCharacteristic_eq_of_exact_extension
        v wRight hBaseRight
    rw [← hcharRight]
    exact hmcop i
  let : FiniteDimensional TTop Top := inferInstance
  have hvalueTop : exponentialValueSubgroup wTop =
      exponentialValueSubgroup wTTop ⊔
        ⨆ i, AddSubgroup.zmultiples (wTop (alphaTop i)).untop₀ :=
    bookExponentialValueSubgroup_eq_sup_iSup_zmultiples_of_radical_family
      wTTop wTop hTTopTop hhensTTop hpTTop hresTTopTop
        r m aTop alphaTop hmpos hmcopTTop hpowTop hgenTop
  have hTUnram : FiniteUnramifiedExtension v wT hKT :=
    maximalUnramifiedSubextension_finiteUnramified
      v wLeft hLeft hhens
  have hTValue : exponentialValueSubgroup wT = exponentialValueSubgroup v :=
    bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one
      v wT hKT
        (exponentialRamificationIndex_eq_one_of_finiteUnramifiedExtension
          v wT hKT hTUnram)
  have hTTopUnram : FiniteUnramifiedExtension
      wRight wTTop hRightTTop :=
    maximalUnramifiedSubextension_finiteUnramified
      wRight wTop hRightTop hhensRight
  have hTTopValue : exponentialValueSubgroup wTTop =
      exponentialValueSubgroup wRight :=
    bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one
      wRight wTTop hRightTTop
        (exponentialRamificationIndex_eq_one_of_finiteUnramifiedExtension
          wRight wTTop hRightTTop hTTopUnram)
  have hroots :
      (⨆ i, AddSubgroup.zmultiples
        (wTop (alphaTop i)).untop₀) =
      ⨆ i, AddSubgroup.zmultiples
        (wLeft (alpha i)).untop₀ := by
    rfl
  have hBaseValue : exponentialValueSubgroup v ≤
      exponentialValueSubgroup wRight :=
    exponentialValueSubgroup_le_of_extends
      v wRight hBaseRight
  change exponentialValueSubgroup wTop =
    exponentialValueSubgroup wLeft ⊔ exponentialValueSubgroup wRight
  rw [hvalueTop, hTTopValue, hroots, hvalueLeft, hTValue]
  exact sup_eq_sup_sup_of_le
    (exponentialValueSubgroup v : AddSubgroup ℝ)
    (exponentialValueSubgroup wRight : AddSubgroup ℝ)
    ((⨆ i, AddSubgroup.zmultiples
      ((wLeft (alpha i)).untop₀ : ℝ)) : AddSubgroup ℝ)
    hBaseValue