The spectral norm and the norm extension theorem

This file shows that if K is a nonarchimedean normed field and L/K is an algebraic extension, then there is a natural extension of the norm on K to a K-algebra norm on L, the so-called spectral norm. The spectral norm of an element of L only depends on its minimal polynomial over K, so for K ⊆ L ⊆ M are two extensions of K, the spectral norm on M restricts to the spectral norm on L. This work can be used to uniquely extend the p-adic norm on ℚ_[p] to an algebraic closure of ℚ_[p], for example.

Details

We define the spectral value and the spectral norm. We prove the norm extension theorem [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Theorem 3.2.1/2)] [BGR84] : given a nonarchimedean normed field K and an algebraic extension L/K, the spectral norm is a power-multiplicative K-algebra norm on L extending the norm on K. All K-algebra automorphisms of L are isometries with respect to this norm. If L/K is finite, we get a formula relating the spectral norm on L with any other power-multiplicative norm on L extending the norm on K.

Moreover, we also prove the unique norm extension theorem: if K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then the spectral norm on L is a nonarchimedean multiplicative norm, and any power-multiplicative K-algebra norm on L coincides with the spectral norm. More over, if L/K is finite, then L is a complete space. This result is S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Theorem 3.2.4/2).

As a prerequisite, we formalize the proof of S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1).

Main Definitions

• spectralValue : the spectral value of a polynomial in R[X].
• spectralNorm : the spectral norm |y|_sp is the spectral value of the minimal polynomial of y : L over K.
• spectralAlgNorm : the spectral norm is a K-algebra norm on L.
• spectralMulAlgNorm : the spectral norm is a multiplicative K-algebra norm on L.

Main Results

• norm_le_spectralNorm : if f is a power-multiplicative K-algebra norm on L, then f is bounded above by spectralNorm K L.
• spectralNorm_eq_of_equiv : the K-algebra automorphisms of L are isometries with respect to the spectral norm.
• spectralNorm_eq_iSup_of_finiteDimensional_normal : if L/K is finite and normal, then spectralNorm K L x = iSup (fun (σ : Gal(L/K)) ↦ f (σ x)).
• isPowMul_spectralNorm : the spectral norm is power-multiplicative.
• isNonarchimedean_spectralNorm : the spectral norm is nonarchimedean.
• spectralNorm_extends : the spectral norm extends the norm on K.
• spectralNorm_unique : any power-multiplicative K-algebra norm on L coincides with the spectral norm.
• spectralAlgNorm_mul : the spectral norm on L is multiplicative.
• spectralNorm.completeSpace : if L/K is finite dimensional, then L is a complete space with respect to topology induced by the spectral norm.

References

• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis

Tags

spectral, spectral norm, spectral value, seminorm, norm, nonarchimedean

def spectralValueTerms {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : ℕ → ℝ

The function ℕ → ℝ sending n to ‖ p.coeff n ‖^(1/(p.natDegree - n : ℝ)), if n < p.natDegree, or to 0 otherwise.

Equations

• spectralValueTerms p n = if n < p.natDegree then ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) else 0

theorem spectralValueTerms_of_lt_natDegree {R : Type u_1} [SeminormedRing R] (p : Polynomial R) {n : ℕ} (hn : n < p.natDegree) : spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))

theorem spectralValueTerms_of_natDegree_le {R : Type u_1} [SeminormedRing R] (p : Polynomial R) {n : ℕ} (hn : p.natDegree ≤ n) : spectralValueTerms p n = 0

def spectralValue {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : ℝ

The spectral value of a polynomial in R[X], where R is a seminormed ring. One motivation for the spectral value: if the norm on R is nonarchimedean, and if a monic polynomial splits into linear factors, then its spectral value is the norm of its largest root. See max_norm_root_eq_spectralValue.

Equations

• spectralValue p = iSup (spectralValueTerms p)

theorem spectralValueTerms_finite_range {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : (Set.range (spectralValueTerms p)).Finite

The range of spectralValue_terms p is a finite set.

theorem spectralValueTerms_bddAbove {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : BddAbove (Set.range (spectralValueTerms p))

The sequence spectralValue_terms p is bounded above.

theorem spectralValueTerms_nonneg {R : Type u_1} [SeminormedRing R] (p : Polynomial R) (n : ℕ) : 0 ≤ spectralValueTerms p n

The sequence spectralValue_terms p is nonnegative.

theorem spectralValue_nonneg {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : 0 ≤ spectralValue p

The spectral value of a polynomial is nonnegative.

theorem spectralValue_X_sub_C {R : Type u_1} [SeminormedRing R] [Nontrivial R] (r : R) : spectralValue (Polynomial.X - Polynomial.C r) = ‖r‖

The polynomial X - r has spectral value ‖ r ‖.

theorem spectralValue_X_pow {R : Type u_1} [SeminormedRing R] [Nontrivial R] (n : ℕ) : spectralValue (Polynomial.X ^ n) = 0

The polynomial X ^ n has spectral value 0.

theorem spectralValue_eq_zero_iff {R : Type u_1} [NormedRing R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) : spectralValue p = 0 ↔ p = Polynomial.X ^ p.natDegree

The spectral value of p equals zero if and only if p is of the form X ^ n.

theorem spectralValue_le_one_iff {R : Type u_1} [NormedDivisionRing R] {P : Polynomial R} (hP : P.Monic) : spectralValue P ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

The spectral value of a monic polynomial P is less than or equal to one if and only if all of its coefficients have norm less than or equal to 1.

theorem norm_root_le_spectralValue {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) {p : Polynomial K} (hp : p.Monic) {x : L} (hx : (Polynomial.aeval x) p = 0) : f x ≤ spectralValue p

The norm of any root of p is bounded by the spectral value of p. See [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1(1))] [BGR84].

theorem max_norm_root_eq_spectralValue {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [DecidableEq L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hf1 : f 1 = 1) (p : Polynomial K) (s : Multiset L) (hp : (Polynomial.mapAlg K L) p = (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod) : (⨆ (x : L), 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)).

def spectralNorm (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] (y : L) : ℝ

If L is an algebraic extension of a normed field K and y : L then the spectral norm spectralNorm K y : ℝ of y (written |y|_sp in the textbooks) is the spectral value of the minimal polynomial of y over K.

Equations

• spectralNorm K L y = spectralValue (minpoly K y)

theorem spectralNorm.eq_of_tower {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {E : Type u_4} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (x : E) : spectralNorm K E x = spectralNorm K L ((algebraMap E L) x)

If L/E/K is a tower of fields, then the spectral norm of x : E equals its spectral norm when regarding x as an element of L.

theorem spectralNorm.eq_of_normalClosure' {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (E : IntermediateField K L) (x : ↥E) : spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) x) = spectralNorm K L ((algebraMap (↥E) L) x)

If L/E/K is a tower of fields, then the spectral norm of x : E when regarded as an element of the normal closure of E equals its spectral norm when regarding x as an element of L.

theorem spectralNorm.eq_of_normalClosure {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {E : IntermediateField K L} {x : L} (g : ↥E) (h_map : (algebraMap (↥E) L) g = x) : spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) g) = spectralNorm K L x

If L/E/K is a tower of fields and x = algebraMap E L g, then the spectral norm of g : E when regarded as an element of the normal closure of E equals the spectral norm of x : L.

theorem spectralNorm_zero {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] : spectralNorm K L 0 = 0

spectralNorm K L (0 : L) = 0.

theorem spectralNorm_nonneg {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (y : L) : 0 ≤ spectralNorm K L y

spectralNorm K L y is nonnegative.

theorem spectralNorm_zero_lt {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {y : L} (hy : y ≠ 0) (hy_alg : IsAlgebraic K y) : 0 < spectralNorm K L y

spectralNorm K L y is positive if y ≠ 0.

theorem eq_zero_of_map_spectralNorm_eq_zero {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : spectralNorm K L x = 0) (hx_alg : IsAlgebraic K x) : x = 0

If spectralNorm K L x = 0, then x = 0.

theorem norm_le_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) {x : L} (hx_alg : IsAlgebraic K x) : f x ≤ spectralNorm K L x

If f is a power-multiplicative K-algebra norm on L, then f is bounded above by spectralNorm K L.

theorem spectralNorm_eq_of_equiv {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (σ : Gal(L/K)) (x : L) : spectralNorm K L x = spectralNorm K L (σ x)

The K-algebra automorphisms of L are isometries with respect to the spectral norm.

theorem spectralNorm_eq_iSup_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] {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 = ⨆ (σ : Gal(L/K)), f (σ x)

If L/K is finite and normal, then spectralNorm K L x = supr (λ (σ : Gal(L/K)), f (σ x)).

theorem spectralNorm_eq_invariantExtension (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [hu : IsUltrametricDist K] : spectralNorm K L = ⇑(IsUltrametricDist.invariantExtension K L)

If L/K is finite and normal, then spectralNorm K L = invariantExtension K L.

theorem isPowMul_spectralNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : IsPowMul (spectralNorm K L)

If L/K is finite and normal, then spectralNorm K L is power-multiplicative. See also the more general result isPowMul_spectralNorm.

def spectralAlgNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : AlgebraNorm K L

The spectral norm is a K-algebra norm on L when L/K is finite and normal. See also spectralAlgNorm for a more general construction.

Equations

• spectralAlgNorm_of_finiteDimensional_normal K L = { toFun := spectralNorm K L, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }

theorem spectralAlgNorm_of_finiteDimensional_normal_def (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] (x : L) : (spectralAlgNorm_of_finiteDimensional_normal K L) x = spectralNorm K L x

theorem isNonarchimedean_spectralNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : IsNonarchimedean (spectralNorm K L)

The spectral norm is nonarchimedean when L/K is finite and normal. See also isNonarchimedean_spectralNorm for a more general result.

theorem spectralNorm_extends_of_finiteDimensional (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] (x : K) : spectralNorm K L ((algebraMap K L) x) = ‖x‖

The spectral norm extends the norm on K when L/K is finite and normal. See also spectralNorm_extends for a more general result.

theorem spectralNorm_unique_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊) (hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)) (x : L) : f x = spectralNorm K L x

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.

instance instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (E : IntermediateField K L) : SeminormClass (AlgebraNorm K ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) K ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))

theorem spectralNorm_extends {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (k : K) : spectralNorm K L ((algebraMap K L) k) = ‖k‖

The spectral norm extends the norm on K.

theorem spectralNorm_one {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] : spectralNorm K L 1 = 1

theorem spectralNorm_neg {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] {y : L} (hy : IsAlgebraic K y) : spectralNorm K L (-y) = spectralNorm K L y

spectralNorm K L (-y) = spectralNorm K L y .

theorem spectralNorm_smul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] (k : K) {y : L} (hy : IsAlgebraic K y) : spectralNorm K L (k • y) = ↑‖k‖₊ * spectralNorm K L y

The spectral norm is compatible with the action of K.

theorem spectralNorm_mul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] {x y : L} (hx : IsAlgebraic K x) (hy : IsAlgebraic K y) : spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

The spectral norm is submultiplicative.

theorem isPowMul_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsPowMul (spectralNorm K L)

The spectral norm is power-multiplicative.

theorem isNonarchimedean_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsNonarchimedean (spectralNorm K L)

The spectral norm is nonarchimedean.

def spectralAlgNorm (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : AlgebraNorm K L

The spectral norm is a K-algebra norm on L.

Equations

• spectralAlgNorm K L = { toFun := spectralNorm K L, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }

theorem spectralAlgNorm_def {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (x : L) : (spectralAlgNorm K L) x = spectralNorm K L x

theorem spectralAlgNorm_extends {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (k : K) : (spectralAlgNorm K L) ((algebraMap K L) k) = ‖k‖

theorem spectralAlgNorm_one {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : (spectralAlgNorm K L) 1 = 1

theorem spectralAlgNorm_isPowMul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsPowMul ⇑(spectralAlgNorm K L)

theorem spectralNorm_unique {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) : f = spectralAlgNorm K L

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then any power-multiplicative K-algebra norm on L coincides with the spectral norm.

theorem spectralNorm_unique_field_norm_ext {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AbsoluteValue L ℝ} (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖) (x : L) : f x = spectralNorm K L x

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.

def algNormFromConst {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1) {x : L} (hx : x ≠ 0) : AlgebraNorm K L

Given a nonzero x : L, and assuming that (spectralAlgNorm h_alg hna) 1 ≤ 1, this is the real-valued function sending y ∈ L to the limit of (f (y * x^n))/((f x)^n), regarded as an algebra norm.

Equations

• algNormFromConst h1 hx = { toRingNorm := normFromConst h1 ⋯ ⋯, smul' := ⋯ }

theorem algNormFromConst_def {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1) {x y : L} (hx : x ≠ 0) : (algNormFromConst h1 hx) y = (seminormFromConst h1 ⋯ ⋯) y

theorem spectralAlgNorm_mul {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x y : L) : (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then the spectral norm on L is multiplicative.

def spectralMulAlgNorm (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : MulAlgebraNorm K L

The spectral norm is a multiplicative K-algebra norm on L.

Equations

• spectralMulAlgNorm K L = { toAddGroupSeminorm := (spectralAlgNorm K L).toAddGroupSeminorm, map_one' := ⋯, map_mul' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }

theorem spectralMulAlgNorm_def {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) : (spectralMulAlgNorm K L) x = spectralNorm K L x

def spectralNorm.normedField (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedField L

L with the spectral norm is a NormedField.

Equations

• One or more equations did not get rendered due to their size.

def spectralNorm.nontriviallyNormedField (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NontriviallyNormedField L

L with the spectral norm is a NontriviallyNormedField.

Equations

• spectralNorm.nontriviallyNormedField K L = { toNormedField := spectralNorm.normedField K L, non_trivial := ⋯ }

def spectralNorm.normedAddCommGroup (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedAddCommGroup L

L with the spectral norm is a normed_add_comm_group.

Equations

• spectralNorm.normedAddCommGroup K L = inferInstance

def spectralNorm.seminormedAddCommGroup (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : SeminormedAddCommGroup L

L with the spectral norm is a seminormed_add_comm_group.

Equations

• spectralNorm.seminormedAddCommGroup K L = inferInstance

def spectralNorm.normedSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedSpace K L

L with the spectral norm is a normed_space over K.

Equations

• spectralNorm.normedSpace K L = { toModule := inferInstance, norm_smul_le := ⋯ }

def spectralNorm.metricSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : MetricSpace L

The metric space structure on L induced by the spectral norm.

Equations

• spectralNorm.metricSpace K L = (spectralNorm.normedField K L).toMetricSpace

def spectralNorm.uniformSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : UniformSpace L

The uniform space structure on L induced by the spectral norm.

Equations

• spectralNorm.uniformSpace K L = PseudoMetricSpace.toUniformSpace

@[instance 100]

instance spectralNorm.completeSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] [h_fin : FiniteDimensional K L] : CompleteSpace L

If L/K is finite dimensional, then L is a complete space with respect to topology induced by the spectral norm.

theorem spectralNorm.spectralMulAlgNorm_eq_of_mem_roots (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) {E : Type u_2} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic K E] {a : E} (ha : a ∈ ((Polynomial.mapAlg K E) (minpoly K x)).roots) : (spectralMulAlgNorm K E) a = (spectralMulAlgNorm K E) ((algebraMap L E) x)

theorem spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) {E : Type u_2} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Polynomial.IsSplittingField L E ((Polynomial.mapAlg K L) (minpoly K x))] [Algebra.IsAlgebraic K E] : (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree = (spectralMulAlgNorm K E) ((Polynomial.mapAlg K E) (minpoly K x)).roots.prod

Given an algebraic tower of fields E/L/K and an element x : L whose minimal polynomial f over K splits into linear factors over E, the degree(f)th power of the spectral norm of x, considered as an element of E, is equal to the spectral norm of the product of the E-valued roots of f.

theorem spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) : spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / ↑(minpoly K x).natDegree)

For x : L with minimal polynomial f(X) := X^n + a_{n-1}X^{n-1} + ... + a_0 over K, the spectral norm of x is equal to ‖a_0‖^(1/(degree(f(X)))).