English
If L/K is finite and normal and f is a power-multiplicative, nonarchimedean AlgebraNorm on L extending the norm on K with invariance under algebra automorphisms, then f equals the spectral norm.
Русский
Если L/K — конечномерное нормальное расширение, и f — мощно-множимая неархимедова алгебраическая норма на L, расширяющая норму на K и сохраняющая инвариантность относительно алгебраических автоморфизмов, то f совпадает со спектральной нормой.
LaTeX
$$$\forall f:\ AlgebraNorm\ K L,\; IsPowMul\ f \land IsNonarchimedean f \land (\forall x\in K, f(\mathrm{algebraMap}_{K,L}(x)) = \|x\|_{+}) \land (\forall \sigma:\,L\cong_{K} L, \; \forall x:\,L,\; f(x) = f(\sigma x)) \Rightarrow \forall x:\,L,\; f(x) = \operatorname{spectralNorm}_{K,L}(x)$$$
Lean4
/-- If `L/K` is finite and normal, and `f` is a power-multiplicative `K`-algebra norm on `L`
extending the norm on `K`, then `f = spectralNorm K L`. -/
theorem spectralNorm_unique_of_finiteDimensional_normal {f : AlgebraNorm K L} (hf_pm : IsPowMul f)
(hf_na : IsNonarchimedean f) (hf_ext : ∀ (x : K), f (algebraMap K L x) = ‖x‖₊)
(hf_iso : ∀ (σ : L ≃ₐ[K] L) (x : L), f x = f (σ x)) (x : L) : f x = spectralNorm K L x :=
by
have h_sup : (⨆ σ : L ≃ₐ[K] L, f (σ x)) = f x :=
by
rw [← @ciSup_const _ (L ≃ₐ[K] L) _ _ (f x)]
exact iSup_congr fun σ ↦ by rw [hf_iso σ x]
rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pm hf_na hf_ext, h_sup]
