FiniteNormExtension.lean

abbrev finiteStandardRealAbsoluteValue : AbsoluteValue ℝ ℝ

abbrev finiteStandardComplexAbsoluteValue : AbsoluteValue ℂ ℝ

theorem finiteRpowUniformSpaceEq
    {F : Type*} [Field F] (v : AbsoluteValue F ℝ)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    (AbsoluteValue.rpow v s hs0 hs1).uniformSpace =
      v.uniformSpace

theorem finiteRpowCompleteIff
    {F : Type*} [Field F] (v : AbsoluteValue F ℝ)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    IsCompleteForAbsoluteValue
        (AbsoluteValue.rpow v s hs0 hs1) ↔
      IsCompleteForAbsoluteValue v

theorem finiteStandardComplete
    (F : Type*) [NormedField F] [CompleteSpace F] :
    IsCompleteForAbsoluteValue (NormedField.toAbsoluteValue F)

theorem finiteStandardRealComplete :
    IsCompleteForAbsoluteValue finiteStandardRealAbsoluteValue

theorem finiteStandardComplexComplete :
    IsCompleteForAbsoluteValue finiteStandardComplexAbsoluteValue

theorem finiteStandardRealRpowComplete
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    IsCompleteForAbsoluteValue
      (AbsoluteValue.rpow
        finiteStandardRealAbsoluteValue s hs0 hs1)

theorem finiteStandardComplexRpowComplete
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    IsCompleteForAbsoluteValue
      (AbsoluteValue.rpow
        finiteStandardComplexAbsoluteValue s hs0 hs1)

theorem finiteStandardComplexExtendsReal
    (x : ℝ) :
    finiteStandardComplexAbsoluteValue (algebraMap ℝ ℂ x) =
      finiteStandardRealAbsoluteValue x

theorem finiteCompAlgEquivComplete
    {K L E : Type*} [Field K] [Field L] [Field E]
    [Algebra K L] [Algebra K E] (e : L ≃ₐ[K] E)
    (w : AbsoluteValue E ℝ)
    (hwcomplete : IsCompleteForAbsoluteValue w) :
    IsCompleteForAbsoluteValue
      (AbsoluteValue.compAlgEquiv e w)

theorem finiteRealAlgEquivRealUniqueRpowExtension
    {L : Type*} [Field L] [Algebra ℝ L] (e : L ≃ₐ[ℝ] ℝ)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1)
    (w : AbsoluteValue L ℝ)
    (hw : ∀ x : ℝ, w (algebraMap ℝ L x) =
      finiteStandardRealAbsoluteValue x ^ s) :
    w = AbsoluteValue.rpow
      (AbsoluteValue.compAlgEquiv
        e finiteStandardRealAbsoluteValue)
      s hs0 hs1

theorem finiteRealAlgEquivComplexUniqueRpowExtension
    {L : Type*} [Field L] [Algebra ℝ L] (e : L ≃ₐ[ℝ] ℂ)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1)
    (w : AbsoluteValue L ℝ)
    (hw : ∀ x : ℝ, w (algebraMap ℝ L x) =
      finiteStandardRealAbsoluteValue x ^ s) :
    w = AbsoluteValue.rpow
      (AbsoluteValue.compAlgEquiv
        e finiteStandardComplexAbsoluteValue)
      s hs0 hs1

theorem finiteComplexAlgEquivComplexUniqueRpowExtension
    {L : Type*} [Field L] [Algebra ℂ L] (e : L ≃ₐ[ℂ] ℂ)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1)
    (w : AbsoluteValue L ℝ)
    (hw : ∀ z : ℂ, w (algebraMap ℂ L z) =
      finiteStandardComplexAbsoluteValue z ^ s) :
    w = AbsoluteValue.rpow
      (AbsoluteValue.compAlgEquiv
        e finiteStandardComplexAbsoluteValue)
      s hs0 hs1

theorem finiteNormExtension_real_self_normFormulaValue_eq_standard
    (x : ℝ) :
    finiteExtensionNormFormulaValue (K := ℝ) (L := ℝ)
      finiteStandardRealAbsoluteValue x =
      finiteStandardRealAbsoluteValue x

theorem finiteNormExtension_complex_self_normFormulaValue_eq_standard
    (z : ℂ) :
    finiteExtensionNormFormulaValue (K := ℂ) (L := ℂ)
      finiteStandardComplexAbsoluteValue z =
      finiteStandardComplexAbsoluteValue z

theorem finiteNormExtension_real_complex_normFormulaValue_eq_standard
    (z : ℂ) :
    finiteExtensionNormFormulaValue (K := ℝ) (L := ℂ)
      finiteStandardRealAbsoluteValue z =
      finiteStandardComplexAbsoluteValue z

theorem finiteNormExtension_finite_normFormulaValue_rpow
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1)
    (x : L) :
    finiteExtensionNormFormulaValue
        (AbsoluteValue.rpow v s hs0 hs1) x =
      finiteExtensionNormFormulaValue v x ^ s

theorem finiteNormExtension_finite_normFormulaValue_algEquiv
    {K L E : Type*} [Field K] [Field L] [Field E]
    [Algebra K L] [Algebra K E]
    [FiniteDimensional K L] [FiniteDimensional K E]
    (v : AbsoluteValue K ℝ) (e : L ≃ₐ[K] E) (x : L) :
    finiteExtensionNormFormulaValue v x =
      finiteExtensionNormFormulaValue v (e x)

theorem finiteNormExtension_real_self_normFormulaValue_eq_rpow
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) (x : ℝ) :
    finiteExtensionNormFormulaValue (K := ℝ) (L := ℝ)
      (AbsoluteValue.rpow
        finiteStandardRealAbsoluteValue s hs0 hs1) x =
      finiteStandardRealAbsoluteValue x ^ s

theorem finiteNormExtension_complex_self_normFormulaValue_eq_rpow
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) (z : ℂ) :
    finiteExtensionNormFormulaValue (K := ℂ) (L := ℂ)
      (AbsoluteValue.rpow
        finiteStandardComplexAbsoluteValue s hs0 hs1) z =
      finiteStandardComplexAbsoluteValue z ^ s

theorem finiteNormExtension_real_complex_normFormulaValue_eq_rpow
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) (z : ℂ) :
    finiteExtensionNormFormulaValue (K := ℝ) (L := ℂ)
      (AbsoluteValue.rpow
        finiteStandardRealAbsoluteValue s hs0 hs1) z =
      finiteStandardComplexAbsoluteValue z ^ s

def finiteWithAbsNontriviallyNormedField
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (hv : v.IsNontrivial) :
    NontriviallyNormedField (WithAbs v)

instance finiteWithAbsAlgebraIsAlgebraic
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] (v : AbsoluteValue K ℝ) :
    Algebra.IsAlgebraic (WithAbs v) L

theorem finiteWithAbsIsUltrametricDist
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    IsUltrametricDist (WithAbs v)

theorem finiteSpectralNormExtendsBase
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (x : K) :
    _root_.spectralNorm (WithAbs v) L (algebraMap K L x) = v x

theorem finiteSpectralNormStrongTriangle
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) (x y : L) :
    _root_.spectralNorm (WithAbs v) L (x + y) ≤
      max (_root_.spectralNorm (WithAbs v) L x)
        (_root_.spectralNorm (WithAbs v) L y)

theorem finiteSpectralNormEqZeroIff
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    _root_.spectralNorm (WithAbs v) L x = 0 ↔ x = 0

theorem finiteSpectralNormMul
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x y : L) :
    _root_.spectralNorm (WithAbs v) L (x * y) =
      _root_.spectralNorm (WithAbs v) L x *
        _root_.spectralNorm (WithAbs v) L y

theorem finiteBaseIsNonarchimedean
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    IsNonarchimedean (v : K → ℝ)

def finiteSpectralExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) : AbsoluteValue L ℝ

theorem finiteSpectralExtension_extends_base
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : K) :
    finiteSpectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv (algebraMap K L x) = v x

theorem finiteSpectralNormCompleteSpace
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) :
    letI : NontriviallyNormedField (WithAbs v) :=
      finiteWithAbsNontriviallyNormedField v hv
    letI : Algebra (WithAbs v) L :=
      WithAbs.algebraLeft L v
    letI : CompleteSpace (WithAbs v) :=
      completeSpace_withAbs_of_isCompleteForAbsoluteValue v hcomplete
    letI : IsUltrametricDist (WithAbs v) :=
      finiteWithAbsIsUltrametricDist v hnonarch
    letI : Algebra.IsAlgebraic (WithAbs v) L :=
      finiteWithAbsAlgebraIsAlgebraic v
    @CompleteSpace L (_root_.spectralNorm.uniformSpace (WithAbs v) L) := by
  let : NontriviallyNormedField (WithAbs v) :=
    finiteWithAbsNontriviallyNormedField v hv
  let : Algebra (WithAbs v) L :=
    WithAbs.algebraLeft L v
  let : CompleteSpace (WithAbs v) :=
    completeSpace_withAbs_of_isCompleteForAbsoluteValue v hcomplete
  let : IsUltrametricDist (WithAbs v) :=
    finiteWithAbsIsUltrametricDist v hnonarch
  let : Algebra.IsAlgebraic (WithAbs v) L :=
    finiteWithAbsAlgebraIsAlgebraic v
  infer_instance

theorem finiteSpectralExtensionComplete
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) :
    IsCompleteForAbsoluteValue
      (finiteSpectralExtension (K := K) (L := L)
        v hcomplete hnonarch hv)

theorem finiteSpectralNormEqMinpolyCoeffZeroRpow
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : L) :
    _root_.spectralNorm (WithAbs v) L x =
      v ((minpoly K x).coeff 0) ^
        (1 / ((minpoly K x).natDegree : ℝ))

theorem finiteSpectralExtensionEqMinpolyCoeffZeroRpow
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : L) :
    finiteSpectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv x =
      v ((minpoly K x).coeff 0) ^
        (1 / ((minpoly K x).natDegree : ℝ))

theorem finiteNormExtension_abs_norm_eq_minpoly_coeff_zero_pow_relfinrank
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (x : L) :
    v (Algebra.norm K x) =
      v ((minpoly K x).coeff 0) ^
        (Module.finrank (IntermediateField.adjoin K ({x} : Set L)) L)

theorem finiteNatPowRpowInvMulCancel
    {a : ℝ} (ha : 0 ≤ a) {m n : ℕ} (hm : 0 < m) (hn : 0 < n) :
    (a ^ n) ^ (1 / ((m * n : ℕ) : ℝ)) = a ^ (1 / (m : ℝ))

theorem finiteNatPowRpowInvMulCancelLeft
    {a : ℝ} (ha : 0 ≤ a) {m n : ℕ} (hm : 0 < m) (hn : 0 < n) :
    (a ^ m) ^ (1 / ((m * n : ℕ) : ℝ)) = a ^ (1 / (n : ℝ))

theorem finiteNormExtension_finite_normFormulaValue_eq_spectralAbsoluteValue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : L) :
    finiteExtensionNormFormulaValue v x =
      finiteSpectralExtension (K := K) (L := L)
        v hcomplete hnonarch hv x

theorem finiteNormExtension_finite_normFormulaValue_strong_triangle
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x y : L) :
    finiteExtensionNormFormulaValue v (x + y) ≤
      max (finiteExtensionNormFormulaValue v x)
        (finiteExtensionNormFormulaValue v y)

def finiteNormExtension_finite_normFormulaAbsoluteValue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) : AbsoluteValue L ℝ where
  toFun := finiteExtensionNormFormulaValue v
  map_mul' x y := by
    rw [finiteNormExtension_finite_normFormulaValue_eq_spectralAbsoluteValue
        v hcomplete hnonarch hv (x * y),
      finiteNormExtension_finite_normFormulaValue_eq_spectralAbsoluteValue
        v hcomplete hnonarch hv x,
      finiteNormExtension_finite_normFormulaValue_eq_spectralAbsoluteValue
        v hcomplete hnonarch hv y]
    exact (finiteSpectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv).map_mul x y
  nonneg' x := finiteExtensionNormFormulaValue_nonneg v x
  eq_zero' x := by
    rw [finiteNormExtension_finite_normFormulaValue_eq_spectralAbsoluteValue
      v hcomplete hnonarch hv x]
    exact (finiteSpectralExtension (K := K) (L := L)
      v hcomplete hnonarch hv).eq_zero' x
  add_le' x y := by
    have hstrong :=
      finiteNormExtension_finite_normFormulaValue_strong_triangle
        v hcomplete hnonarch hv x y
    have hx_nonneg : 0 ≤ finiteExtensionNormFormulaValue v x :=
      finiteExtensionNormFormulaValue_nonneg v x
    have hy_nonneg : 0 ≤ finiteExtensionNormFormulaValue v y :=
      finiteExtensionNormFormulaValue_nonneg v y
    exact hstrong.trans
      (max_le
        (le_add_of_nonneg_right hy_nonneg)
        (le_add_of_nonneg_left hx_nonneg))

theorem finiteNormExtension_finite_normFormulaAbsoluteValue_apply
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : L) :
    finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
      v hcomplete hnonarch hv x =
      finiteExtensionNormFormulaValue v x

theorem finiteNormExtension_finite_normFormulaAbsoluteValue_eq_spectralAbsoluteValue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) :
    finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
      v hcomplete hnonarch hv =
      finiteSpectralExtension (K := K) (L := L)
        v hcomplete hnonarch hv

theorem finiteNormExtension_finite_normFormulaAbsoluteValue_extends_base
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) (x : K) :
    finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
      v hcomplete hnonarch hv (algebraMap K L x) = v x

theorem finiteNormExtension_finite_normFormulaAbsoluteValue_complete
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) :
    IsCompleteForAbsoluteValue
      (finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
        v hcomplete hnonarch hv)

theorem finiteNormExtension_unique_extension_finite_normFormulaAbsoluteValue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial)
    (w : AbsoluteValue L ℝ)
    (hw_ext : ∀ x : K, w (algebraMap K L x) = v x) :
    w = finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
      v hcomplete hnonarch hv

structure FiniteNormExtensionFiniteExtensionResult
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) where
  /-- The distinguished absolute value on the finite extension. -/
  extension : AbsoluteValue L ℝ
  /-- The distinguished absolute value restricts to the given base absolute value. -/
  extends_base : ∀ x : K, extension (algebraMap K L x) = v x
  /-- Every extension of the base absolute value equals the distinguished extension. -/
  unique :
    ∀ w : AbsoluteValue L ℝ,
      (∀ x : K, w (algebraMap K L x) = v x) → w = extension
  /-- The distinguished extension is given by the finite-extension norm formula. -/
  norm_formula : ∀ x : L, extension x = finiteExtensionNormFormulaValue v x
  /-- The distinguished extension is complete. -/
  complete_extension : IsCompleteForAbsoluteValue extension

theorem FiniteNormExtensionFiniteExtensionResult.ext_unique
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    {v : AbsoluteValue K ℝ}
    (R S : FiniteNormExtensionFiniteExtensionResult (K := K) (L := L) v) :
    R = S

def finiteNormExtension_real_finite_rpow_extension
    {L : Type*} [Field L] [Algebra ℝ L]
    [FiniteDimensional ℝ L]
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    FiniteNormExtensionFiniteExtensionResult (K := ℝ) (L := L)
      (AbsoluteValue.rpow
        finiteStandardRealAbsoluteValue s hs0 hs1)

def finiteNormExtension_complex_finite_rpow_extension
    {L : Type*} [Field L] [Algebra ℂ L]
    [FiniteDimensional ℂ L]
    (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) :
    FiniteNormExtensionFiniteExtensionResult (K := ℂ) (L := L)
      (AbsoluteValue.rpow
        finiteStandardComplexAbsoluteValue s hs0 hs1)

theorem finiteIsAlgebraicOfBaseRingEquiv
    {K E L : Type*} [Field K] [Field E] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L] (σ : K ≃+* E) :
    letI : Algebra E K := RingHom.toAlgebra σ.symm.toRingHom
    letI : Algebra E L :=
      RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
    Algebra.IsAlgebraic E L := by
  let : Algebra E K := RingHom.toAlgebra σ.symm.toRingHom
  let : Algebra E L :=
    RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
  have : IsScalarTower E K L :=
    IsScalarTower.of_algebraMap_eq (fun r => by
      simp [RingHom.algebraMap_toAlgebra])
  let e : K ≃ₐ[E] E := AlgEquiv.ofRingEquiv (f := σ) (by
    intro r
    simp [RingHom.algebraMap_toAlgebra])
  have : Algebra.IsAlgebraic E K := e.symm.isAlgebraic
  exact Algebra.IsAlgebraic.trans E K L

theorem finiteNormExtension_finiteDimensional_of_base_ringEquiv
    {K E L : Type*} [Field K] [Field E] [Field L] [Algebra K L]
    [FiniteDimensional K L] (σ : K ≃+* E) :
    letI : Algebra E L :=
      RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
    FiniteDimensional E L := by
  let : Algebra E K := RingHom.toAlgebra σ.symm.toRingHom
  let : Algebra E L :=
    RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
  have : IsScalarTower E K L :=
    IsScalarTower.of_algebraMap_eq (fun r => by
      simp [RingHom.algebraMap_toAlgebra])
  let e : K ≃ₐ[E] E := AlgEquiv.ofRingEquiv (f := σ) (by
    intro r
    simp [RingHom.algebraMap_toAlgebra])
  have : Module.Finite E K := Module.Finite.equiv e.symm.toLinearEquiv
  exact FiniteDimensional.trans E K L

theorem finiteNormExtension_finite_normFormulaValue_base_ringEquiv
    {K E L : Type*} [Field K] [Field E] [Field L] [Algebra K L]
    [FiniteDimensional K L] (σ : K ≃+* E)
    (vK : AbsoluteValue K ℝ) (vE : AbsoluteValue E ℝ)
    (hvσ : ∀ x : K, vE (σ x) = vK x)
    (x : L) :
    letI : Algebra E L :=
      RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
    letI : FiniteDimensional E L :=
      finiteNormExtension_finiteDimensional_of_base_ringEquiv (K := K)
        (E := E) (L := L) σ
    finiteExtensionNormFormulaValue (K := E) (L := L) vE x =
      finiteExtensionNormFormulaValue (K := K) (L := L) vK x := by
  let : Algebra E K := RingHom.toAlgebra σ.symm.toRingHom
  let : Algebra E L :=
    RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
  have : IsScalarTower E K L :=
    IsScalarTower.of_algebraMap_eq (fun r => by
      simp [RingHom.algebraMap_toAlgebra])
  let e : K ≃ₐ[E] E := AlgEquiv.ofRingEquiv (f := σ) (by
    intro r
    simp [RingHom.algebraMap_toAlgebra])
  have : Module.Finite E K := Module.Finite.equiv e.symm.toLinearEquiv
  have : FiniteDimensional E L := FiniteDimensional.trans E K L
  have hfinEK : Module.finrank E K = 1 := by
    rw [e.toLinearEquiv.finrank_eq]
    simp
  have hfin : Module.finrank K L = Module.finrank E L := by
    have hmul := Module.finrank_mul_finrank E K L
    rwa [hfinEK, one_mul] at hmul
  have he : (algebraMap E L).comp σ.toRingHom = algebraMap K L := by
    ext x
    simp [RingHom.algebraMap_toAlgebra]
  have hnorm : Algebra.norm E x = σ (Algebra.norm K x) :=
    (Algebra.norm_eq_of_ringEquiv σ he x).symm
  rw [finiteExtensionNormFormulaValue, finiteExtensionNormFormulaValue]
  rw [hnorm, hvσ, ← hfin]

def finiteNormExtension_finiteExtensionResult_base_ringEquiv
    {K E L : Type*} [Field K] [Field E] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (σ : K ≃+* E) (vK : AbsoluteValue K ℝ) (vE : AbsoluteValue E ℝ)
    (hvσ : ∀ x : K, vE (σ x) = vK x)
    (R :
      letI : Algebra E L :=
        RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
      letI : FiniteDimensional E L :=
        finiteNormExtension_finiteDimensional_of_base_ringEquiv
          (K := K) (E := E) (L := L) σ
      FiniteNormExtensionFiniteExtensionResult (K := E) (L := L) vE) :
    FiniteNormExtensionFiniteExtensionResult (K := K) (L := L) vK := by
  letI : Algebra E L :=
    RingHom.toAlgebra ((algebraMap K L).comp σ.symm.toRingHom)
  letI : FiniteDimensional E L :=
    finiteNormExtension_finiteDimensional_of_base_ringEquiv
      (K := K) (E := E) (L := L) σ
  exact
    { extension := R.extension
      extends_base := by
        intro x
        have hbase := R.extends_base (σ x)
        have hmap :
            algebraMap E L (σ x) = algebraMap K L x := by
          simp [RingHom.algebraMap_toAlgebra]
        calc
          R.extension (algebraMap K L x)
              = R.extension (algebraMap E L (σ x)) := by rw [hmap]
          _ = vE (σ x) := hbase
          _ = vK x := hvσ x
      unique := by
        intro w hw
        apply R.unique w
        intro z
        have hmap :
            algebraMap E L z = algebraMap K L (σ.symm z) := by
          simp [RingHom.algebraMap_toAlgebra]
        calc
          w (algebraMap E L z)
              = w (algebraMap K L (σ.symm z)) := by rw [hmap]
          _ = vK (σ.symm z) := hw (σ.symm z)
          _ = vE z := by
            simpa using (hvσ (σ.symm z)).symm
      norm_formula := by
        intro x
        calc
          R.extension x
              = finiteExtensionNormFormulaValue (K := E) (L := L) vE x :=
                R.norm_formula x
          _ = finiteExtensionNormFormulaValue (K := K) (L := L) vK x := by
                exact finiteNormExtension_finite_normFormulaValue_base_ringEquiv
                  (K := K) (E := E) (L := L) σ vK vE hvσ x
      complete_extension := R.complete_extension }

def finiteNormExtension_nonarchimedean_finite_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : v.IsNontrivial) :
    FiniteNormExtensionFiniteExtensionResult (K := K) (L := L) v where
  extension :=
    finiteNormExtension_finite_normFormulaAbsoluteValue (K := K) (L := L)
      v hcomplete hnonarch hv
  extends_base :=
    finiteNormExtension_finite_normFormulaAbsoluteValue_extends_base
      (K := K) (L := L) v hcomplete hnonarch hv
  unique :=
    finiteNormExtension_unique_extension_finite_normFormulaAbsoluteValue
      (K := K) (L := L) v hcomplete hnonarch hv
  norm_formula :=
    finiteNormExtension_finite_normFormulaAbsoluteValue_apply
      (K := K) (L := L) v hcomplete hnonarch hv
  complete_extension :=
    finiteNormExtension_finite_normFormulaAbsoluteValue_complete
      (K := K) (L := L) v hcomplete hnonarch hv

def finiteNormExtension_archimedean_finite_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (harch : LubinTate.Valuations.ArchimedeanAbsoluteValue v) :
    FiniteNormExtensionFiniteExtensionResult (K := K) (L := L) v

def finiteNormExtension_finite_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hv : v.IsNontrivial) :
    FiniteNormExtensionFiniteExtensionResult (K := K) (L := L) v