seminormFromBounded

In this file, we prove BGR, Proposition 1.2.1/2 : given a nonzero additive group seminorm on a commutative ring R such that for some c : ℝ and every x y : R, the inequality f (x * y) ≤ c * f x * f y) is satisfied, we create a ring seminorm on R.

In the file comments, we will use the expression f is multiplicatively bounded to indicate that this condition holds.

Main Definitions

• seminormFromBounded' : the real-valued function sending x ∈ R to the supremum of f(x*y)/f(y), where y runs over the elements of R.
• seminormFromBounded : the function seminormFromBounded' as a RingSeminorm on R.
• normFromBounded :seminormFromBounded' f as a RingNorm on R, provided that f is nonnegative, multiplicatively bounded and subadditive, that it preserves 0 and negation, and that f has trivial kernel.

Main Results

• seminormFromBounded_isNonarchimedean : if f : R → ℝ is a nonnegative, multiplicatively bounded, nonarchimedean function, then seminormFromBounded' f is nonarchimedean.
• seminormFromBounded_of_mul_is_mul : if f : R → ℝ is a nonnegative, multiplicatively bounded function and x : R is multiplicative for f, then x is multiplicative for seminormFromBounded' f.

References

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

Tags

seminormFromBounded, RingSeminorm, Nonarchimedean

def seminormFromBounded' {R : Type u_1} [CommRing R] (f : R → ℝ) : R → ℝ

The real-valued function sending x ∈ R to the supremum of f(x*y)/f(y), where y runs over the elements of R.

Equations

• seminormFromBounded' f x = ⨆ (y : R), f (x * y) / f y

theorem map_one_ne_zero {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : f 1 ≠ 0

If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then f 1 ≠ 0.

theorem map_pow_ne_zero {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) {x : R} (hx : IsUnit x) (hfx : f x ≠ 0) (n : ℕ) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : f (x ^ n) ≠ 0

If f : R → ℝ is a nonnegative multiplicatively bounded function and x : R is a unit with f x ≠ 0, then for every n : ℕ, we have f (x ^ n) ≠ 0.

theorem map_mul_zero_of_map_zero {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) {x : R} (hx : f x = 0) (y : R) : f (x * y) = 0

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then given x y : R with f x = 0, we have f (x * y) = 0.

theorem seminormFromBounded_zero {R : Type u_1} [CommRing R] {f : R → ℝ} (f_zero : f 0 = 0) : seminormFromBounded' f 0 = 0

seminormFromBounded' f preserves 0.

theorem seminormFromBounded_aux {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) : 0 ≤ c * f x

theorem seminormFromBounded_bddAbove_range {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) : BddAbove (Set.range fun (y : R) => f (x * y) / f y)

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, the image of y ↦ f (x * y) / f y is bounded above.

theorem seminormFromBounded_le {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) : seminormFromBounded' f x ≤ c * f x

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, seminormFromBounded' f x is bounded above by some multiple of f x.

theorem seminormFromBounded_ge {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) : f x ≤ f 1 * seminormFromBounded' f x

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, f x ≤ f 1 * seminormFromBounded' f x.

theorem seminormFromBounded_nonneg {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : 0 ≤ seminormFromBounded' f

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f is nonnegative.

theorem seminormFromBounded_eq_zero_iff {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) : seminormFromBounded' f x = 0 ↔ f x = 0

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f x = 0 if and only if f x = 0.

theorem seminormFromBounded_neg {R : Type u_1} [CommRing R] {f : R → ℝ} (f_neg : ∀ (x : R), f (-x) = f x) (x : R) : seminormFromBounded' f (-x) = seminormFromBounded' f x

If f is invariant under negation of x, then so is seminormFromBounded'.

theorem seminormFromBounded_mul {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (x : R) (y : R) : seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f is submultiplicative.

theorem seminormFromBounded_one {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : seminormFromBounded' f 1 = 1

If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then seminormFromBounded' f 1 = 1.

theorem seminormFromBounded_one_le {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : seminormFromBounded' f 1 ≤ 1

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f 1 ≤ 1.

theorem seminormFromBounded_add {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (f_add : ∀ (a b : R), f (a + b) ≤ f a + f b) (x : R) (y : R) : seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y

If f : R → ℝ is a nonnegative, multiplicatively bounded, subadditive function, then seminormFromBounded' f is subadditive.

def seminormFromBounded {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (f_add : ∀ (a b : R), f (a + b) ≤ f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) : RingSeminorm R

seminormFromBounded' is a ring seminorm on R.

Equations

• seminormFromBounded f_zero f_nonneg f_mul f_add f_neg = { toFun := seminormFromBounded' f, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯ }

theorem seminormFromBounded_isNonarchimedean {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (hna : IsNonarchimedean f) : IsNonarchimedean (seminormFromBounded' f)

If f : R → ℝ is a nonnegative, multiplicatively bounded, nonarchimedean function, then seminormFromBounded' f is nonarchimedean.

theorem seminormFromBounded_of_mul_apply {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) : seminormFromBounded' f x = f x

If f : R → ℝ is a nonnegative, multiplicatively bounded function and x : R is multiplicative for f, then seminormFromBounded' f x = f x.

theorem seminormFromBounded_of_mul_le {R : Type u_1} [CommRing R] {f : R → ℝ} (f_nonneg : 0 ≤ f) {x : R} (hx : ∀ (y : R), f (x * y) ≤ f x * f y) (h_one : f 1 ≤ 1) : seminormFromBounded' f x = f x

If f : R → ℝ is a nonnegative function and x : R is submultiplicative for f, then seminormFromBounded' f x = f x.

theorem seminormFromBounded_nonzero {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : seminormFromBounded' f ≠ 0

If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then seminormFromBounded' f is nonzero.

theorem seminormFromBounded_ker {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) : seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}

If f : R → ℝ is a nonnegative, multiplicatively bounded function, then the kernel of seminormFromBounded' f equals the kernel of f.

theorem seminormFromBounded_is_norm_iff {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (f_add : ∀ (a b : R), f (a + b) ≤ f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) : (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}

If f : R → ℝ is a nonnegative, multiplicatively bounded, subadditive function that preserves zero and negation, then seminormFromBounded' f is a norm if and only if f⁻¹' {0} = {0}.

def normFromBounded {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (f_add : ∀ (a b : R), f (a + b) ≤ f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) (f_ker : f ⁻¹' {0} = {0}) : RingNorm R

seminormFromBounded' f as a RingNorm on R, provided that f is nonnegative, multiplicatively bounded and subadditive, that it preserves 0 and negation, and that f has trivial kernel.

Equations

• normFromBounded f_zero f_nonneg f_mul f_add f_neg f_ker = let __src := seminormFromBounded f_zero f_nonneg f_mul f_add f_neg; { toRingSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ }

theorem seminormFromBounded_of_mul_is_mul {R : Type u_1} [CommRing R] {f : R → ℝ} {c : ℝ} (f_nonneg : 0 ≤ f) (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) (y : R) : seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y

If f : R → ℝ is a nonnegative, multiplicatively bounded function and x : R is multiplicative for f, then x is multiplicative for seminormFromBounded' f.