English
Equality of spectral norm values when passing to the normal closure in a tower of fields.
Русский
Согласованность спектральной нормы при переходе к нормальному замыканию в башне полей.
LaTeX
$$$$\operatorname{spectralNorm}(K,\text{normalClosure}(K,E,\text{AlgebraicClosure}(E)))(g)=\operatorname{spectralNorm}(K,L)(x)$$$$
Lean4
/-- If `L/K` is finite and normal, then `spectralNorm K L x = supr (λ (σ : L ≃ₐ[K] L), f (σ x))`. -/
theorem spectralNorm_eq_iSup_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‖) (x : L) :
spectralNorm K L x = ⨆ σ : L ≃ₐ[K] L, f (σ x) := by
classical
have hf1 : f 1 = 1 := by
rw [← (algebraMap K L).map_one, hf_ext]
simp
refine
le_antisymm ?_
(ciSup_le fun σ ↦
norm_root_le_spectralValue hf_pm hf_na (minpoly.monic (hn.isIntegral x)) (minpoly.aeval_algHom _ σ.toAlgHom _))
· set p := minpoly K x
have hp_sp : Splits (algebraMap K L) (minpoly K x) := hn.splits x
obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).mp hp_sp
have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by rw [minpoly.monic (hn.isIntegral x), map_one]
rw [h_lc, map_one, one_mul] at hs
simp only [spectralNorm]
rw [← max_norm_root_eq_spectralValue hf_pm hf_na hf1 _ _ hs]
apply ciSup_le
intro y
split_ifs with h
· obtain ⟨σ, hσ⟩ : ∃ σ : L ≃ₐ[K] L, σ x = y :=
minpoly.exists_algEquiv_of_root' (Algebra.IsAlgebraic.isAlgebraic x)
(aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)
rw [← hσ]
convert le_ciSup (Finite.bddAbove_range _) σ
· rfl
· exact instNonemptyOfInhabited
· exact SemilatticeSup.to_isDirected_le
· exact iSup_nonneg fun σ ↦ apply_nonneg _ _
