LubinTateUniformizerDiagonal.lean

theorem explicitLocalCompleteDVFValuation_hasExtension
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    (LocalFieldTheory.localCompleteDVF K).valuation.HasExtension
      (LocalFieldTheory.localCompleteDVF L).valuation

theorem lubinTateLevel_spectral_inertiaDeg_eq_one
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) :
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : NontriviallyNormedField T :=
      finiteExtensionSpectralNormedField K T
    letI : ValuativeRel T :=
      finiteExtensionSpectralValuativeRel K T
    letI : IsNonarchimedeanLocalField T :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K T
    letI : Valuation.HasExtension (ValuativeRel.valuation K)
        (ValuativeRel.valuation T) :=
      finiteExtensionSpectralValuation_hasExtension K T
    letI :
        (LocalFieldTheory.localCompleteDVF K).valuation.HasExtension
          (LocalFieldTheory.localCompleteDVF T).valuation :=
      explicitLocalCompleteDVFValuation_hasExtension K T
    (LocalFieldTheory.localCompleteDVF T).maximalIdeal.inertiaDeg
      (LocalFieldTheory.localCompleteDVF K).valuationSubring = 1 := by
  let T := standardLubinTateLevelField hπ n
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : NontriviallyNormedField T :=
    finiteExtensionSpectralNormedField K T
  let : ValuativeRel T :=
    finiteExtensionSpectralValuativeRel K T
  let : IsNonarchimedeanLocalField T :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K T
  let : Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation T) :=
    finiteExtensionSpectralValuation_hasExtension K T
  let base := (standardLocalField K).toCompleteDVF
  let chosen := standardLubinTateLevelCompleteDVF hπ n
  let spectral := LocalFieldTheory.localCompleteDVF T
  let : base.valuation.HasExtension spectral.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension K T
  have hValuationRing :
      chosen.valuation.valuationSubring =
        spectral.valuation.valuationSubring :=
    valuationSubring_eq_of_finite_separable base chosen spectral.valuation
  have hdegree :
      degree base.toDVF chosen.toDVF =
        ramificationIndex base.toDVF chosen.toDVF *
          residueDegree base.toDVF chosen.toDVF :=
    standardLubinTateLevelCompleteDVF_fundamentalIdentity hπ n
  have hramification :
      ramificationIndex base.toDVF chosen.toDVF =
        degree base.toDVF chosen.toDVF :=
    standardLubinTateLevel_ramificationIndex_eq_degree hπ n
  have hdegreePos : 0 < degree base.toDVF chosen.toDVF := by
    change 0 < Module.finrank K T
    exact Module.finrank_pos
  have hresidue :
      residueDegree base.toDVF chosen.toDVF = 1 := by
    apply Nat.eq_of_mul_eq_mul_left hdegreePos
    simpa [hramification] using hdegree.symm
  change chosen.maximalIdeal.inertiaDeg base.valuationSubring = 1 at hresidue
  let e : chosen.valuationSubring ≃ₐ[base.valuationSubring]
      spectral.valuationSubring :=
    { toFun := fun x => ⟨x.val, by
        rw [← hValuationRing]
        exact x.property⟩
      invFun := fun x => ⟨x.val, by
        rw [hValuationRing]
        exact x.property⟩
      left_inv := fun x => by
        apply Subtype.ext
        rfl
      right_inv := fun x => by
        apply Subtype.ext
        rfl
      map_mul' := fun x y => by
        apply Subtype.ext
        rfl
      map_add' := fun x y => by
        apply Subtype.ext
        rfl
      commutes' := fun x => by
        apply Subtype.ext
        rfl }
  have hmap :
      chosen.maximalIdeal.map e = spectral.maximalIdeal :=
    IsLocalRing.map_ringEquiv_maximalIdeal e.toRingEquiv
  have hinertia :
      spectral.maximalIdeal.inertiaDeg base.valuationSubring =
        chosen.maximalIdeal.inertiaDeg base.valuationSubring := by
    rw [Ideal.inertiaDeg_eq_of_isMaximal base.maximalIdeal spectral.maximalIdeal,
      Ideal.inertiaDeg_eq_of_isMaximal base.maximalIdeal chosen.maximalIdeal]
    exact
      (Ideal.Quotient.algEquivOfEqMap base.maximalIdeal e
        hmap.symm).toLinearEquiv.finrank_eq.symm
  change spectral.maximalIdeal.inertiaDeg base.valuationSubring = 1
  exact hinertia.trans hresidue

theorem explicitLocalCompleteDVF_ramificationIdx_eq_one_of_top
    (K M U : Type) [Field K] [Field M] [Field U]
    [Algebra K M] [Algebra K U] [Algebra M U] [IsScalarTower K M U]
    (base : CompleteDVF K) (middle : CompleteDVF M)
    (total : CompleteDVF U)
    [base.valuation.HasExtension middle.valuation]
    [base.valuation.HasExtension total.valuation]
    [middle.valuation.HasExtension total.valuation]
    [FiniteDimensional M U] [Algebra.IsSeparable M U]
    (htop :
      total.maximalIdeal.ramificationIdx base.valuationSubring = 1) :
    middle.maximalIdeal.ramificationIdx base.valuationSubring = 1

theorem
    localFiniteUnramifiedField_inf_lubinTateLevelField_ramificationIdx
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    let U := localFiniteUnramifiedField K d hd
    let T := standardLubinTateLevelField hπ n
    let M := U ⊓ T
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : FiniteDimensional K M :=
      FiniteDimensional.of_injective
        (M.inclusion (show M ≤ U from inf_le_left)).toLinearMap
        (M.inclusion (show M ≤ U from inf_le_left)).injective
    letI : NontriviallyNormedField M :=
      finiteExtensionSpectralNormedField K M
    letI : ValuativeRel M :=
      finiteExtensionSpectralValuativeRel K M
    letI : IsNonarchimedeanLocalField M :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K M
    letI : Valuation.HasExtension (ValuativeRel.valuation K)
        (ValuativeRel.valuation M) :=
      finiteExtensionSpectralValuation_hasExtension K M
    let base := LocalFieldTheory.localCompleteDVF K
    let middle := LocalFieldTheory.localCompleteDVF M
    letI : base.valuation.HasExtension middle.valuation :=
      explicitLocalCompleteDVFValuation_hasExtension K M
    middle.maximalIdeal.ramificationIdx base.valuationSubring = 1 := by
  let U := localFiniteUnramifiedField K d hd
  let T := standardLubinTateLevelField hπ n
  let M := U ⊓ T
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : FiniteDimensional K M :=
    FiniteDimensional.of_injective
      (M.inclusion (show M ≤ U from inf_le_left)).toLinearMap
      (M.inclusion (show M ≤ U from inf_le_left)).injective
  let : NontriviallyNormedField M :=
    finiteExtensionSpectralNormedField K M
  let : ValuativeRel M :=
    finiteExtensionSpectralValuativeRel K M
  let : IsNonarchimedeanLocalField M :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K M
  let : Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation M) :=
    finiteExtensionSpectralValuation_hasExtension K M
  let : Algebra M U :=
    (M.inclusion (show M ≤ U from inf_le_left)).toRingHom.toAlgebra
  let : IsScalarTower K M U :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : Valuation.HasExtension (ValuativeRel.valuation M)
      (ValuativeRel.valuation U) :=
    finiteExtensionSpectralValuation_hasExtension_of_tower K M U
  let : FiniteDimensional M U :=
    FiniteDimensional.right K M U
  let : Algebra.IsSeparable M U :=
    Algebra.isSeparable_tower_top_of_isSeparable
      (F := K) (L := M) (E := U)
  let base := LocalFieldTheory.localCompleteDVF K
  let middle := LocalFieldTheory.localCompleteDVF M
  let unramified := LocalFieldTheory.localCompleteDVF U
  let : base.valuation.HasExtension middle.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension K M
  let : base.valuation.HasExtension unramified.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension K U
  let : middle.valuation.HasExtension unramified.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension M U
  have hramificationUnramified :
      unramified.maximalIdeal.ramificationIdx base.valuationSubring = 1 := by
    change
      (IsLocalRing.maximalIdeal
          (ValuativeRel.valuation U).integer).ramificationIdx
        (ValuativeRel.valuation K).integer = 1
    exact unramifiedValuation_ramificationIdx_eq_one K U
  exact explicitLocalCompleteDVF_ramificationIdx_eq_one_of_top
    K M U base middle unramified hramificationUnramified

theorem
    localFiniteUnramifiedField_inf_lubinTateLevelField_inertiaDeg
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    let U := localFiniteUnramifiedField K d hd
    let T := standardLubinTateLevelField hπ n
    let M := U ⊓ T
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : FiniteDimensional K M :=
      FiniteDimensional.of_injective
        (M.inclusion (show M ≤ U from inf_le_left)).toLinearMap
        (M.inclusion (show M ≤ U from inf_le_left)).injective
    letI : NontriviallyNormedField M :=
      finiteExtensionSpectralNormedField K M
    letI : ValuativeRel M :=
      finiteExtensionSpectralValuativeRel K M
    letI : IsNonarchimedeanLocalField M :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K M
    letI : Valuation.HasExtension (ValuativeRel.valuation K)
        (ValuativeRel.valuation M) :=
      finiteExtensionSpectralValuation_hasExtension K M
    let base := LocalFieldTheory.localCompleteDVF K
    let middle := LocalFieldTheory.localCompleteDVF M
    letI : base.valuation.HasExtension middle.valuation :=
      explicitLocalCompleteDVFValuation_hasExtension K M
    middle.maximalIdeal.inertiaDeg base.valuationSubring = 1 := by
  let U := localFiniteUnramifiedField K d hd
  let T := standardLubinTateLevelField hπ n
  let M := U ⊓ T
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : FiniteDimensional K M :=
    FiniteDimensional.of_injective
      (M.inclusion (show M ≤ U from inf_le_left)).toLinearMap
      (M.inclusion (show M ≤ U from inf_le_left)).injective
  let : NontriviallyNormedField T :=
    finiteExtensionSpectralNormedField K T
  let : ValuativeRel T :=
    finiteExtensionSpectralValuativeRel K T
  let : IsNonarchimedeanLocalField T :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K T
  let : Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation T) :=
    finiteExtensionSpectralValuation_hasExtension K T
  let : NontriviallyNormedField M :=
    finiteExtensionSpectralNormedField K M
  let : ValuativeRel M :=
    finiteExtensionSpectralValuativeRel K M
  let : IsNonarchimedeanLocalField M :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K M
  let : Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation M) :=
    finiteExtensionSpectralValuation_hasExtension K M
  let : Algebra M T :=
    (M.inclusion (show M ≤ T from inf_le_right)).toRingHom.toAlgebra
  let : IsScalarTower K M T :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : Valuation.HasExtension (ValuativeRel.valuation M)
      (ValuativeRel.valuation T) :=
    finiteExtensionSpectralValuation_hasExtension_of_tower K M T
  let base := LocalFieldTheory.localCompleteDVF K
  let middle := LocalFieldTheory.localCompleteDVF M
  let total := LocalFieldTheory.localCompleteDVF T
  let : base.valuation.HasExtension middle.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension K M
  let : base.valuation.HasExtension total.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension K T
  let : middle.valuation.HasExtension total.valuation :=
    explicitLocalCompleteDVFValuation_hasExtension M T
  let : IsScalarTower base.valuationSubring middle.valuationSubring
      total.valuationSubring :=
    IsScalarTower.of_algebraMap_eq' rfl
  have htotal :
      total.maximalIdeal.inertiaDeg base.valuationSubring = 1 := by
    exact lubinTateLevel_spectral_inertiaDeg_eq_one K hπ n
  have hinertiaDvd :
      middle.maximalIdeal.inertiaDeg base.valuationSubring ∣
        total.maximalIdeal.inertiaDeg base.valuationSubring :=
    middle.maximalIdeal.inertiaDeg_below_dvd total.maximalIdeal
  rw [htotal] at hinertiaDvd
  exact Nat.eq_one_of_dvd_one hinertiaDvd

theorem localFiniteUnramifiedField_inf_lubinTateLevelField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    localFiniteUnramifiedField K d hd ⊓
        standardLubinTateLevelField hπ n =
      ⊥

theorem localFiniteUnramifiedField_linearDisjoint_lubinTateLevelField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    (localFiniteUnramifiedField K d hd).LinearDisjoint
      (standardLubinTateLevelField hπ n)

abbrev lubinTateUniformizerDiagonalCompositumField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IntermediateField K (SeparableClosure K)

theorem lubinTateUniformizerDiagonalCompositumField_finiteDimensional
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    FiniteDimensional K
      (lubinTateUniformizerDiagonalCompositumField K hπ n u)

theorem lubinTateUniformizerDiagonalCompositumField_isGalois
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IsGalois K
      (lubinTateUniformizerDiagonalCompositumField K hπ n u)

theorem explicitRestrictNormalHom_toAlgAut_eq_one
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (B : IntermediateField K C) [Normal K B]
    (δ : Gal(C/B)) :
    AlgEquiv.restrictNormalHom B
        (MulSemiringAction.toAlgAut Gal(C/B) K C δ) =
      1

theorem explicitRestrictNormalHom_mul_inv_eq_one
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A : IntermediateField K C) [Normal K A]
    (σ τ : Gal(C/K)) (ρ : Gal(A/K))
    (hσ : AlgEquiv.restrictNormalHom A σ = ρ)
    (hτ : AlgEquiv.restrictNormalHom A τ = ρ) :
    AlgEquiv.restrictNormalHom A (σ * τ⁻¹) = 1

theorem explicit_mem_fixingSubgroup_of_restrictNormalHom_eq_one
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A : IntermediateField K C) [Normal K A]
    (σ : Gal(C/K))
    (hσ : AlgEquiv.restrictNormalHom A σ = 1) :
    σ ∈ A.fixingSubgroup

theorem explicit_eq_one_of_mem_fixingSubgroup_of_sup_eq_top
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A B : IntermediateField K C) (σ : Gal(C/K))
    (hA : σ ∈ A.fixingSubgroup) (hB : σ ∈ B.fixingSubgroup)
    (hSup : A ⊔ B = ⊤) :
    σ = 1

theorem explicitAlgEquiv_eq_of_restrict_eq_of_sup_eq_top
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A B : IntermediateField K C) [Normal K A] [Normal K B]
    (σ τ : Gal(C/K))
    (hA : AlgEquiv.restrictNormalHom A σ =
      AlgEquiv.restrictNormalHom A τ)
    (hB : AlgEquiv.restrictNormalHom B σ =
      AlgEquiv.restrictNormalHom B τ)
    (hSup : A ⊔ B = ⊤) :
    σ = τ

theorem explicit_orderOf_eq_of_restrict_orders_of_sup_eq_top
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A B : IntermediateField K C) [Normal K A] [Normal K B]
    [Finite (Gal(A/K))] [Finite (Gal(B/K))]
    (σ : Gal(C/K)) (σA : Gal(A/K)) (σB : Gal(B/K)) (d : ℕ)
    (hA : AlgEquiv.restrictNormalHom A σ = σA)
    (hB : AlgEquiv.restrictNormalHom B σ = σB)
    (hAOrder : orderOf σA = d) (hBOrder : orderOf σB = d)
    (hSup : A ⊔ B = ⊤) :
    orderOf σ = d

theorem exists_explicitAlgEquiv_with_disjoint_restrictions
    (K C : Type) [Field K] [Field C] [Algebra K C]
    (A B : IntermediateField K C)
    [Normal K A] [Normal K B] [Normal K C]
    [FiniteDimensional K A] [FiniteDimensional B C] [IsGalois B C]
    (hInf : A ⊓ B = ⊥) (σA : Gal(A/K)) (σB : Gal(B/K)) :
    ∃ σ : Gal(C/K),
      AlgEquiv.restrictNormalHom A σ = σA ∧
        AlgEquiv.restrictNormalHom B σ = σB

theorem exists_lubinTateUniformizerDiagonalAutomorphism
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    let σT : Gal(T/K) :=
      (standardLubinTateUnitParameterEquivGal
        (standardLocalField K) hπ n
        (standardLubinTateUnitParameterClass
          (standardLocalField K) n u))⁻¹
    let d := orderOf σT
    let hd : 0 < d := orderOf_pos σT
    let U := localFiniteUnramifiedField K d hd
    let C := U ⊔ T
    let hUC : U ≤ C := le_sup_left
    let hTC : T ≤ C := le_sup_right
    let A := U.restrict hUC
    let B := T.restrict hTC
    let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
    let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
    letI : IsGalois K A := IsGalois.of_algEquiv eU
    letI : IsGalois K B := IsGalois.of_algEquiv eT
    let φ :=
      arithmeticFrobeniusOfUnramifiedValuation K U
    let σA : Gal(A/K) := (eU.symm.trans φ).trans eU
    let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
    ∃ σ : Gal(C/K),
      AlgEquiv.restrictNormalHom A σ = σA ∧
        AlgEquiv.restrictNormalHom B σ = σB := by
  let T := standardLubinTateLevelField hπ n
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let σT : Gal(T/K) :=
    (standardLubinTateUnitParameterEquivGal
      (standardLocalField K) hπ n
      (standardLubinTateUnitParameterClass
        (standardLocalField K) n u))⁻¹
  let d := orderOf σT
  let hd : 0 < d := orderOf_pos σT
  let U := localFiniteUnramifiedField K d hd
  let C := U ⊔ T
  let hUC : U ≤ C := le_sup_left
  let hTC : T ≤ C := le_sup_right
  let A := U.restrict hUC
  let B := T.restrict hTC
  let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
  let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
  let : IsGalois K U := inferInstance
  let : IsGalois K T :=
    standardLubinTateLevelField_isGalois
      (F := standardLocalField K) hπ n
  let : IsGalois K A := IsGalois.of_algEquiv eU
  let : IsGalois K B := IsGalois.of_algEquiv eT
  let : FiniteDimensional K C :=
    lubinTateUniformizerDiagonalCompositumField_finiteDimensional
      K hπ n u
  let : IsGalois K C :=
    lubinTateUniformizerDiagonalCompositumField_isGalois
      K hπ n u
  let : FiniteDimensional B C :=
    FiniteDimensional.right K B C
  let : IsGalois B C :=
    IsGalois.tower_top_of_isGalois K B C
  let φ :=
    arithmeticFrobeniusOfUnramifiedValuation K U
  let σA : Gal(A/K) := (eU.symm.trans φ).trans eU
  let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
  have hInf : U ⊓ T = ⊥ :=
    localFiniteUnramifiedField_inf_lubinTateLevelField
      K hπ d hd n
  have hInf' : A ⊓ B = ⊥ := by
    rw [← IntermediateField.lift_inj,
      IntermediateField.lift_bot,
      IntermediateField.lift_inf,
      IntermediateField.lift_restrict hUC,
      IntermediateField.lift_restrict hTC,
      hInf]
  exact exists_explicitAlgEquiv_with_disjoint_restrictions
    K C A B hInf' σA σB

def lubinTateUniformizerDiagonalAutomorphism
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    Gal((lubinTateUniformizerDiagonalCompositumField K hπ n u)/K)

theorem lubinTateUniformizerDiagonalAutomorphism_restrict_unramified
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    let σT : Gal(T/K) :=
      (standardLubinTateUnitParameterEquivGal
        (standardLocalField K) hπ n
        (standardLubinTateUnitParameterClass
          (standardLocalField K) n u))⁻¹
    let d := orderOf σT
    let hd : 0 < d := orderOf_pos σT
    let U := localFiniteUnramifiedField K d hd
    let C := U ⊔ T
    let hUC : U ≤ C := le_sup_left
    let A := U.restrict hUC
    let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
    letI : IsGalois K A := IsGalois.of_algEquiv eU
    let φA : Gal(A/K) :=
      (eU.symm.trans
        (arithmeticFrobeniusOfUnramifiedValuation K U)).trans eU
    AlgEquiv.restrictNormalHom A
        (lubinTateUniformizerDiagonalAutomorphism K hπ n u) =
      φA :=
  (Classical.choose_spec
    (exists_lubinTateUniformizerDiagonalAutomorphism K hπ n u)).1

theorem lubinTateUniformizerDiagonalAutomorphism_restrict_level
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    let σT : Gal(T/K) :=
      (standardLubinTateUnitParameterEquivGal
        (standardLocalField K) hπ n
        (standardLubinTateUnitParameterClass
          (standardLocalField K) n u))⁻¹
    let d := orderOf σT
    let hd : 0 < d := orderOf_pos σT
    let U := localFiniteUnramifiedField K d hd
    let C := U ⊔ T
    let hTC : T ≤ C := le_sup_right
    let B := T.restrict hTC
    let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
    letI : IsGalois K B := IsGalois.of_algEquiv eT
    let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
    AlgEquiv.restrictNormalHom B
        (lubinTateUniformizerDiagonalAutomorphism K hπ n u) =
      σB :=
  (Classical.choose_spec
    (exists_lubinTateUniformizerDiagonalAutomorphism K hπ n u)).2

theorem lubinTateUniformizerDiagonalAutomorphism_unique
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ)
    (σ : Gal((lubinTateUniformizerDiagonalCompositumField K hπ n u)/K))
    (hσUnramified :
      let T := standardLubinTateLevelField hπ n
      letI : FiniteDimensional K T :=
        standardLubinTateLevelField_finiteDimensional hπ n
      let σT : Gal(T/K) :=
        (standardLubinTateUnitParameterEquivGal
          (standardLocalField K) hπ n
          (standardLubinTateUnitParameterClass
            (standardLocalField K) n u))⁻¹
      let d := orderOf σT
      let hd : 0 < d := orderOf_pos σT
      let U := localFiniteUnramifiedField K d hd
      let C := U ⊔ T
      let hUC : U ≤ C := le_sup_left
      let A := U.restrict hUC
      let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
      letI : IsGalois K A := IsGalois.of_algEquiv eU
      let φA : Gal(A/K) :=
        (eU.symm.trans
          (arithmeticFrobeniusOfUnramifiedValuation K U)).trans eU
      AlgEquiv.restrictNormalHom A σ = φA)
    (hσLevel :
      let T := standardLubinTateLevelField hπ n
      letI : FiniteDimensional K T :=
        standardLubinTateLevelField_finiteDimensional hπ n
      let σT : Gal(T/K) :=
        (standardLubinTateUnitParameterEquivGal
          (standardLocalField K) hπ n
          (standardLubinTateUnitParameterClass
            (standardLocalField K) n u))⁻¹
      let d := orderOf σT
      let hd : 0 < d := orderOf_pos σT
      let U := localFiniteUnramifiedField K d hd
      let C := U ⊔ T
      let hTC : T ≤ C := le_sup_right
      let B := T.restrict hTC
      let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
      letI : IsGalois K B := IsGalois.of_algEquiv eT
      let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
      AlgEquiv.restrictNormalHom B σ = σB) :
    σ = lubinTateUniformizerDiagonalAutomorphism K hπ n u := by
  let T := standardLubinTateLevelField hπ n
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let σT : Gal(T/K) :=
    (standardLubinTateUnitParameterEquivGal
      (standardLocalField K) hπ n
      (standardLubinTateUnitParameterClass
        (standardLocalField K) n u))⁻¹
  let d := orderOf σT
  let hd : 0 < d := orderOf_pos σT
  let U := localFiniteUnramifiedField K d hd
  let C := U ⊔ T
  let hUC : U ≤ C := le_sup_left
  let hTC : T ≤ C := le_sup_right
  let A := U.restrict hUC
  let B := T.restrict hTC
  let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
  let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
  let : IsGalois K A := IsGalois.of_algEquiv eU
  let : IsGalois K B := IsGalois.of_algEquiv eT
  let φA : Gal(A/K) :=
    (eU.symm.trans
      (arithmeticFrobeniusOfUnramifiedValuation K U)).trans eU
  let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
  let chosen := lubinTateUniformizerDiagonalAutomorphism K hπ n u
  have hσA : AlgEquiv.restrictNormalHom A σ = φA := by
    change AlgEquiv.restrictNormalHom A σ = φA at hσUnramified
    exact hσUnramified
  have hσB : AlgEquiv.restrictNormalHom B σ = σB := by
    change AlgEquiv.restrictNormalHom B σ = σB at hσLevel
    exact hσLevel
  have hchosenA : AlgEquiv.restrictNormalHom A chosen = φA := by
    have h :=
      lubinTateUniformizerDiagonalAutomorphism_restrict_unramified K hπ n u
    change AlgEquiv.restrictNormalHom A chosen = φA at h
    exact h
  have hchosenB : AlgEquiv.restrictNormalHom B chosen = σB := by
    have h := lubinTateUniformizerDiagonalAutomorphism_restrict_level K hπ n u
    change AlgEquiv.restrictNormalHom B chosen = σB at h
    exact h
  have hSup : A ⊔ B = ⊤ := by
    rw [← IntermediateField.lift_inj,
      IntermediateField.lift_top,
      IntermediateField.lift_sup,
      IntermediateField.lift_restrict hUC,
      IntermediateField.lift_restrict hTC]
  exact explicitAlgEquiv_eq_of_restrict_eq_of_sup_eq_top
    K C A B σ chosen (hσA.trans hchosenA.symm)
      (hσB.trans hchosenB.symm) hSup

theorem lubinTateUniformizerDiagonalAutomorphism_order
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    let σT : Gal(T/K) :=
      (standardLubinTateUnitParameterEquivGal
        (standardLocalField K) hπ n
        (standardLubinTateUnitParameterClass
          (standardLocalField K) n u))⁻¹
    orderOf (lubinTateUniformizerDiagonalAutomorphism K hπ n u) =
      orderOf σT := by
  let T := standardLubinTateLevelField hπ n
  let : FiniteDimensional K T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let σT : Gal(T/K) :=
    (standardLubinTateUnitParameterEquivGal
      (standardLocalField K) hπ n
      (standardLubinTateUnitParameterClass
        (standardLocalField K) n u))⁻¹
  let d := orderOf σT
  let hd : 0 < d := orderOf_pos σT
  let U := localFiniteUnramifiedField K d hd
  let C := U ⊔ T
  let hUC : U ≤ C := le_sup_left
  let hTC : T ≤ C := le_sup_right
  let A := U.restrict hUC
  let B := T.restrict hTC
  let eU : U ≃ₐ[K] A := IntermediateField.restrictAlgEquiv hUC
  let eT : T ≃ₐ[K] B := IntermediateField.restrictAlgEquiv hTC
  let : IsGalois K U := inferInstance
  let : IsGalois K T :=
    standardLubinTateLevelField_isGalois
      (F := standardLocalField K) hπ n
  let : IsGalois K A := IsGalois.of_algEquiv eU
  let : IsGalois K B := IsGalois.of_algEquiv eT
  let φ :=
    arithmeticFrobeniusOfUnramifiedValuation K U
  let σA : Gal(A/K) := (eU.symm.trans φ).trans eU
  let σB : Gal(B/K) := (eT.symm.trans σT).trans eT
  let σ := lubinTateUniformizerDiagonalAutomorphism K hπ n u
  let transportU : Gal(U/K) ≃* Gal(A/K) :=
    { AlgEquiv.equivCongr eU eU with
      map_mul' := by
        intro g h
        ext x
        simp }
  let transportT : Gal(T/K) ≃* Gal(B/K) :=
    { AlgEquiv.equivCongr eT eT with
      map_mul' := by
        intro g h
        ext x
        simp }
  have hσAOrder : orderOf σA = d := by
    rw [show σA = transportU φ by rfl, transportU.orderOf_eq,
      localFiniteUnramifiedField_arithmeticFrobenius_order K d hd]
  have hσBOrder : orderOf σB = d := by
    rw [show σB = transportT σT by rfl, transportT.orderOf_eq]
  have hrestrictA :
      AlgEquiv.restrictNormalHom A σ = σA := by
    have h :=
      lubinTateUniformizerDiagonalAutomorphism_restrict_unramified K hπ n u
    change AlgEquiv.restrictNormalHom A σ = σA at h
    exact h
  have hrestrictB :
      AlgEquiv.restrictNormalHom B σ = σB := by
    have h := lubinTateUniformizerDiagonalAutomorphism_restrict_level K hπ n u
    change AlgEquiv.restrictNormalHom B σ = σB at h
    exact h
  have hSup : A ⊔ B = ⊤ := by
    rw [← IntermediateField.lift_inj,
      IntermediateField.lift_top,
      IntermediateField.lift_sup,
      IntermediateField.lift_restrict hUC,
      IntermediateField.lift_restrict hTC]
  exact explicit_orderOf_eq_of_restrict_orders_of_sup_eq_top
    K C A B σ σA σB d hrestrictA hrestrictB hσAOrder hσBOrder hSup

def lubinTateUniformizerDiagonalFixedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IntermediateField K
      (lubinTateUniformizerDiagonalCompositumField K hπ n u)

theorem lubinTateUniformizerDiagonalFixedField_finrank
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {π : (standardLocalField K).valuationSubring}
    (hπ : (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
      (π : K))
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    Module.finrank K
        (lubinTateUniformizerDiagonalFixedField K hπ n u) =
      Module.finrank K (standardLubinTateLevelField hπ n)