Basis.norm

In this file, we prove [BGR, Lemma 3.2.1./3][bosch-guntzer-remmert] : if K is a normed field with a nonarchimedean power-multiplicative norm and L/K is a finite extension, then there exists at least one power-multiplicative K-algebra norm on L extending the norm on K.

Main Definitions

• Basis.norm : the function sending an element x : L to the maximum of the norms of its coefficients with respect to the K-basis B of L.

Main Results

• norm_mul_le_const_mul_norm : For any K-basis of L, B.norm is bounded with respect to multiplication. That is, ∃ (c : ℝ), c > 0 such that ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y.
• exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional : if K is a normed field with a nonarchimedean power-multiplicative norm and L/K is a finite extension, then there exists at least one power-multiplicative K-algebra norm on L extending the norm on K. This is [BGR, Lemma 3.2.1./3].

References

• [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert]

Tags

Basis.norm, nonarchimedean

def Basis.norm {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] (B : Basis ι K L) (x : L) : ℝ

The function sending an element x : L to the maximum of the norms of its coefficients with respect to the K-basis B of L.

Equations

• B.norm x = Finset.univ.sup' ⋯ fun (i : ι) => ‖(B.repr x) i‖

theorem Basis.norm_repr_le_norm {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] (B : Basis ι K L) {x : L} (i : ι) : ‖(B.repr x) i‖ ≤ B.norm x

The norm of a coefficient x_i is less than or equal to the norm of x.

theorem Basis.norm_zero {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] (B : Basis ι K L) : B.norm 0 = 0

For any K-basis of L, we have B.norm 0 = 0.

theorem Basis.norm_neg {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] (B : Basis ι K L) (x : L) : B.norm (-x) = B.norm x

For any K-basis of L, and any x : L, we have B.norm (-x) = B.norm x.

theorem Basis.norm_nonneg {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] (B : Basis ι K L) (x : L) : 0 ≤ B.norm x

For any K-basis of L, and any x : L, we have 0 ≤ B.norm x.

theorem Basis.norm_extends {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι} (hBi : B i = 1) (x : K) : B.norm ((algebraMap K L) x) = ‖x‖

For any K-basis B of L containing 1, B.norm extends the norm on K.

theorem Basis.norm_isNonarchimedean {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] {B : Basis ι K L} (hna : IsNonarchimedean Norm.norm) : IsNonarchimedean B.norm

For any K-basis of L, if the norm on K is nonarchimedean, then so is B.norm.

theorem Basis.norm_mul_le_const_mul_norm {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_3} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι} (hBi : B i = 1) (hna : IsNonarchimedean Norm.norm) : ∃ (c : ℝ) (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y

For any K-basis of L, B.norm is bounded with respect to multiplication. That is, ∃ (c : ℝ), c > 0 such that ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y.

theorem Basis.norm_smul {K : Type u_1} {L : Type u_2} [NormedField K] [Ring L] [Algebra K L] {ι : Type u_4} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι} (hBi : B i = 1) (k : K) (y : L) : B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y

For any k : K, y : L, we have B.norm ((algebra_map K L) k * y) = B.norm ((algebra_map K L) k) * B.norm y.

theorem exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional {K : Type u_1} {L : Type u_2} [NormedField K] [Field L] [Algebra K L] (hfd : FiniteDimensional K L) (hna : IsNonarchimedean norm) : ∃ (f : AlgebraNorm K L), IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f

If K is a nonarchimedean normed field L/K is a finite extension, then there exists a power-multiplicative nonarchimedean K-algebra norm on L extending the norm on K.