English
If L/K is finite and normal and f is a pow-multiplicative, nonarchimedean AlgebraNorm on L, then f = spectralNorm.
Русский
Если L/K конечномерно и нормально, и f — степенно-множимая неархимедова алгебраическая норма на L, то f совпадает со спектральной нормой.
LaTeX
$$$\text{If } hf\_pm : \IsPowMul f \text{ and } hf\_na : \IsNonarchimedean f, \text{ and } \text{ext conditions}, \ \forall x\in L,\ f(x) = \operatorname{spectralNorm}_{K,L}(x)$$$
Lean4
/-- The spectral norm is power-multiplicative. -/
theorem isPowMul_spectralNorm : IsPowMul (spectralNorm K L) :=
by
intro x n hn
set E := K⟮x⟯
haveI h_finiteDimensional_E : FiniteDimensional K E :=
IntermediateField.adjoin.finiteDimensional (h_alg.isAlgebraic x).isIntegral
set g := IntermediateField.AdjoinSimple.gen K x with hg
have h_map : algebraMap E L g ^ n = x ^ n := rfl
rw [← spectralNorm.eq_of_normalClosure _ (IntermediateField.AdjoinSimple.algebraMap_gen K x), ←
spectralNorm.eq_of_normalClosure (g ^ n) h_map, map_pow, ← hg]
exact
isPowMul_spectralNorm_of_finiteDimensional_normal _ _
((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) g) hn
