English
In a tower L/E/K of fields, the spectral norm of an element x ∈ E equals the spectral norm of its image in L.
Русский
В башне полей L/E/K, спектральная норма элемента x ∈ E равна спектральной норме его образа в L.
LaTeX
$$$$\operatorname{spectralNorm}(K,E,x)=\operatorname{spectralNorm}(K,L,\text{algebraMap}_E^L(x)).$$$$
Lean4
/-- If `L/K` is finite and normal, then `spectralNorm K L = invariantExtension K L`. -/
theorem spectralNorm_eq_invariantExtension [hu : IsUltrametricDist K] : spectralNorm K L = invariantExtension K L :=
by
ext x
have hna := hu.isNonarchimedean_norm
set f := Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna) with hf
have hf_pow : IsPowMul f :=
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).1
have hf_ext : ∀ (x : K), f (algebraMap K L x) = ‖x‖ :=
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.1
have hf_na : IsNonarchimedean f :=
(Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hna)).2.2
rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pow hf_na hf_ext]
simp only [invariantExtension_apply, algNormOfAlgEquiv_apply, hf]
/- Note that the main results below are reproved without the finite dimensionality and normality
assumptions later on in this file. -/
