The commutativity of valuation and Galois group action

Stream: Is there code for X?

[Junjie Bai]

Let L/K be a finite extension of valuation fields. I'm trying to proof the commutativity of valuation and Galois group action using the theorem 'spectralNorm_eq_of_equiv'. For this, I need to use the theorem 'spectralNorm_unique' to show that the Norm over L is equivalance to the spectralNorm. However, it only shows that the 'AlgebraNorm' is equal to the spectralNorm. I'm not familiar with the 'AlgebraNorm' structure. Can anyone show me that how to proof the Norm over L induced by valuation is equivalence to an 'AlgebraNorm', or should I change a way to proof this?
Here is a #mwe :

import Mathlib

open Valued Valuation AlgEquiv
instance : LinearOrderedCommGroupWithZero ℤₘ₀ := sorry

variable (K L : Type*) [Field K] [Field L]  [vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀] [Algebra K L] [FiniteDimensional K L] [Normal K L] [Algebra.IsSeparable K L] [Valuation.HasExtension vK.v vL.v] [CompleteSpace K]
variable (σ : (L ≃ₐ[K] L)) {x : L} (hx : x ∈ vL.v.integer)

#check spectralNorm_unique
#check spectralNorm_eq_of_equiv
example : vL.v (x) = vL.v (σ (x)) := by sorry

[Yakov Pechersky]

This isn't going to be easy to prove from your assumptions, especially given that you have an arbitrary ℤₘ₀. When it should be open WithZero [...] ℤᵐ⁰.

[Yakov Pechersky]

Also, note the arguments to docs#spectralNorm.normedField:

(K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K]

So that part of the library works over ultrametric fields, not valued fields.

[Yakov Pechersky]

But putting it together:

import Mathlib

open Valued Valuation AlgEquiv

open WithZero

lemma norm_eq_iff {X : Type*} (N N' : NormedField X) {x y : X} :
    (letI := N; ‖x‖ = ‖y‖) ↔ (letI := N'; ‖x‖ = ‖y‖) := by
  sorry

variable (K L : Type*) [Field K] [Field L]  [vK : Valued K ℤᵐ⁰] [vL : Valued L ℤᵐ⁰] [Algebra K L] [FiniteDimensional K L] [Normal K L] [Algebra.IsSeparable K L] [Valuation.HasExtension vK.v vL.v] [CompleteSpace K] [vK.v.IsNontrivial] [vL.v.IsNontrivial]
variable (σ : (L ≃ₐ[K] L)) {x : L} (hx : x ∈ vL.v.integer)

open NormedField in
example : vL.v x = vL.v (σ x) := by
  letI : vK.v.RankOne := (Valuation.nonempty_rankOne_iff_mulArchimedean.mpr inferInstance).some
  letI : vL.v.RankOne := (Valuation.nonempty_rankOne_iff_mulArchimedean.mpr inferInstance).some
  suffices ‖x‖ = ‖σ x‖ by
    simpa [le_antisymm_iff] using this
  exact (norm_eq_iff _ (spectralNorm.normedField K L)).mpr (spectralNorm_eq_of_equiv σ _)

[Junjie Bai]

Thanks a lot!

[Yakov Pechersky]

There are some extra assumptions listed there

[Junjie Bai]

I see, these seems necessary. I think I have to add them. Thanks a lot!

[Yakov Pechersky]

Please excuse the rough normed field equals lemma, I think you know what lemma I'm implying about compatibility between nontrivial normed structures on fields

[Junjie Bai]

Yes, I know, this is the hard part. I'm trying to figure out which condition is needed and searching for some relevant theorems.

[Yakov Pechersky]

Interpret L as a NormedSpace over K, and then we need the theorem described here
https://kskedlaya.org/18.787/absolute-values.pdf

[Yakov Pechersky]

Or https://kconrad.math.uconn.edu/blurbs/gradnumthy/equivnorms.pdf, or the equivalent absolute values pdf also

[Junjie Bai]

Exactly! I find the theorem SpectralNorm_unique provides a proof, but it needs an Algebra Norm. The norm over L induced by valuation seems not to be a Algebra Norm.

[Yakov Pechersky]

From what we currently have, can you construct NormedAlgebra K L?

[Yakov Pechersky]

And also that for any NormedAlgebra, then the norm is an AlgebraNorm?

[Yakov Pechersky]

Following that, also convert HasExtension to a NormedAlgebra via docs#Valuation.HasExtension.val_algebraMap and docs#Valued.toNormedField.norm_le_iff, like how I did it with le_antisymm_iff?

[Yakov Pechersky]

Then you can apply the uniqueness lemma iiuc

[Junjie Bai]

I can't construct NormedAlgebra K L. The field 'norm_smul_le' ask that

‖a • b‖ ≤ ‖a‖ * ‖b‖

It seems not correct because a • b = (algebraMap K L a) * b and by the multiplicity of norm we can get the opposite inequality(I hope I didn't get the direction of the inequality sign wrong.)

[Filippo A. E. Nuccio]

Pinging @María Inés de Frutos Fernández