Valuation extension formular

Stream: Is there code for X?

[Junjie Bai]

Is there code for the valuation extension formular?
Specifically, Let L/K be a finite Galois extension of valued field, with Galois group G. Suppose K is complete with respect to the valuation. we have :

$$v_L (x) = (1 / [L : K]) * v_K (Norm_{L/K} (x)), for\ all x \in L$$

Or is there any relevant theorems has been formulated?

[Michael Stoll]

I think @María Inés de Frutos Fernández might have something along these lines.

[Kevin Buzzard]

Hopefully the results in her file Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean will contain everything you need to make this easy.

[Junjie Bai]

Thank you! With this file, I'm now lacking the theorem stating the relevance between SpectralNorm and Norm over the field. Because my goal is to proof the valuation is commutative with the Galois group action and this can be done by checking the norm. I'm not that familiar with the math of this file. How can I relate the spectral norm and norm? Or is there any theorem for this?

[Junjie Bai]

If spectral norm is equivalence with norm, then I can finish my proof. I want to know if this is correct.

[Kevin Buzzard]

I think your question would be much easier to answer if you posted a #mwe showing how far you've got.

[Kevin Buzzard]

Are you looking for docs#spectralNorm_unique ?

[Junjie Bai]

Sorry, I should post a #mwe. Here is what I got now:

import Mathlib

open Valued Valuation AlgEquiv

open WithZero

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
  let f : AlgebraNorm K L := sorry
  have hna : IsNonarchimedean (Norm.norm (E := K)) := IsUltrametricDist.isNonarchimedean_norm
  have h : f x = f (σ x) := by
    rw [spectralNorm_unique (f := f) ?_, spectralAlgNorm_def _, spectralAlgNorm_def _, spectralNorm_eq_of_equiv]
    sorry
  have h1 : ‖x‖ = ‖σ x‖ := by
    sorry
  apply le_antisymm
  · apply Valued.toNormedField.norm_le_iff.1
    apply le_of_eq h1
  · apply Valued.toNormedField.norm_le_iff.1
    apply le_of_eq h1.symm

I want to show the valuation is commutative with Galois group action by counting the norm. And to show the norm has this property, I try to use spectralNorm_unique to show that the norm over the field is equivalent with the spectralNorm. But this thoerem need to fill a AlgebraNorm, and I don't know what is the relevance with an AlgebraNorm and norm, or how can I construct a AlgebraNorm with a norm.

[Junjie Bai]

I find it hard for me to construct a AlgebraNorm by a norm, because the condition 'smul' ' need to show that (assume the field extension is L/K):

$$|| k * l ||_L = ||k||_K * ||l||_L, for\ all k \in K, l \in L$$

And the norm of L is extension the norm of K by:

$$||x||_L = e_{L/K}*||x||_K, for\ all x \in K$$

[María Inés de Frutos Fernández]

docs#spectralMulAlgNorm is already a multiplicative algebra norm.

[Junjie Bai]

Thanks a lot!