English
Given a suitable constant bound, algNormFromConst constructs an AlgebraNorm on L from a constant parameter, using spectralNorm as a guide.
Русский
При заданной допустимой константе строится алгебраическая норма на L через algNormFromConst с опорой на spectralNorm.
LaTeX
$$$\text{algNormFromConst}(h1,hx,y) \; := \; \text{построение AlgebraNorm на } L$$$
Lean4
/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
`L/K` is an algebraic extension, then any multiplicative ring norm on `L` extending the norm on
`K` coincides with the spectral norm. -/
theorem spectralNorm_unique_field_norm_ext [CompleteSpace K] {f : AbsoluteValue L ℝ}
(hf_ext : ∀ (x : K), f (algebraMap K L x) = ‖x‖) (x : L) : f x = spectralNorm K L x :=
by
set g : AlgebraNorm K L :=
{
MulRingNorm.mulRingNormEquivAbsoluteValue.invFun
f with
smul' k
x := by
simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe]
rw [Algebra.smul_def, map_mul]
congr
rw [← hf_ext k]
rfl
mul_le' x y := by simp [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe] }
have hg_pow : IsPowMul g := MulRingNorm.isPowMul _
have hgx : f x = g x := rfl
rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]
