Theorems · Theorem · commutative algebra

max_norm_root_eq_spectralValue

∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : DecidableEq L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f →
      f 1 = 1 →
        ∀ (p : Polynomial K) (s : Multiset L),
          (Polynomial.mapAlg K L) p = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod →
            (⨆ x, if x ∈ s then f x else 0) = spectralValue p

If f is a nonarchimedean, power-multiplicative K-algebra norm on L, then the spectral value of a polynomial p : K[X] that decomposes into linear factors in L is equal to the maximum of the norms of the roots. See [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1(2))][bosch-guntzer-remmert].

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

1 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldFieldAlgebraDecidableEq