Seminorms and norms on rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines seminorms and norms on rings. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

Main declarations #

For a ring R:

ring_seminorm: A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.
ring_norm: A seminorm f is a norm if f x = 0 if and only if x = 0.
mul_ring_seminorm: A multiplicative seminorm on a ring R is a ring seminorm that preserves multiplication.
mul_ring_norm: A multiplicative norm on a ring R is a ring norm that preserves multiplication.

Notes #

The corresponding hom classes are defined in analysis.order.hom.basic to be used by absolute values.

References #

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

Tags #

ring_seminorm, ring_norm

source

structure ring_seminorm (R : Type u_4) [non_unital_non_assoc_ring R] :

Type u_4

to_fun : R → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : R), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : R), self.to_fun (-r) = self.to_fun r
mul_le' : ∀ (x y : R), self.to_fun (x * y) ≤ self.to_fun x * self.to_fun y

A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.

Instances for ring_seminorm

source

@[nolint]

def ring_seminorm.to_add_group_seminorm {R : Type u_4} [non_unital_non_assoc_ring R] (self : ring_seminorm R) :

add_group_seminorm R

source

@[nolint]

def ring_norm.to_add_group_norm {R : Type u_4} [non_unital_non_assoc_ring R] (self : ring_norm R) :

add_group_norm R

source

structure ring_norm (R : Type u_4) [non_unital_non_assoc_ring R] :

Type u_4

to_fun : R → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : R), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : R), self.to_fun (-r) = self.to_fun r
mul_le' : ∀ (x y : R), self.to_fun (x * y) ≤ self.to_fun x * self.to_fun y
eq_zero_of_map_eq_zero' : ∀ (x : R), self.to_fun x = 0 → x = 0

A function f : R → ℝ is a norm on a (nonunital) ring if it is a seminorm and f x = 0 implies x = 0.

Instances for ring_norm

source

@[nolint]

def ring_norm.to_ring_seminorm {R : Type u_4} [non_unital_non_assoc_ring R] (self : ring_norm R) :

ring_seminorm R

source

@[nolint]

def mul_ring_seminorm.to_add_group_seminorm {R : Type u_4} [non_assoc_ring R] (self : mul_ring_seminorm R) :

add_group_seminorm R

source

structure mul_ring_seminorm (R : Type u_4) [non_assoc_ring R] :

Type u_4

to_fun : R → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : R), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : R), self.to_fun (-r) = self.to_fun r
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : R), self.to_fun (x * y) = self.to_fun x * self.to_fun y

A multiplicative seminorm on a ring R is a function f : R → ℝ that preserves zero and multiplication, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.

Instances for mul_ring_seminorm

mul_ring_seminorm.has_sizeof_inst
mul_ring_seminorm.mul_ring_seminorm_class
mul_ring_seminorm.has_coe_to_fun
mul_ring_seminorm.has_one
mul_ring_seminorm.inhabited

source

@[nolint]

def mul_ring_seminorm.to_monoid_with_zero_hom {R : Type u_4} [non_assoc_ring R] (self : mul_ring_seminorm R) :

R →*₀ ℝ

source

@[nolint]

def mul_ring_norm.to_mul_ring_seminorm {R : Type u_4} [non_assoc_ring R] (self : mul_ring_norm R) :

mul_ring_seminorm R

source

@[nolint]

def mul_ring_norm.to_add_group_norm {R : Type u_4} [non_assoc_ring R] (self : mul_ring_norm R) :

add_group_norm R

source

structure mul_ring_norm (R : Type u_4) [non_assoc_ring R] :

Type u_4

to_fun : R → ℝ
map_zero' : self.to_fun 0 = 0
add_le' : ∀ (r s : R), self.to_fun (r + s) ≤ self.to_fun r + self.to_fun s
neg' : ∀ (r : R), self.to_fun (-r) = self.to_fun r
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : R), self.to_fun (x * y) = self.to_fun x * self.to_fun y
eq_zero_of_map_eq_zero' : ∀ (x : R), self.to_fun x = 0 → x = 0

A multiplicative norm on a ring R is a multiplicative ring seminorm such that f x = 0 implies x = 0.

Instances for mul_ring_norm

source

@[protected, instance]

def ring_seminorm.ring_seminorm_class {R : Type u_2} [non_unital_ring R] :

ring_seminorm_class (ring_seminorm R) R ℝ

Equations

ring_seminorm.ring_seminorm_class = {coe := λ (f : ring_seminorm R), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul_le_mul := _}

source

@[protected, instance]

def ring_seminorm.has_coe_to_fun {R : Type u_2} [non_unital_ring R] :

has_coe_to_fun (ring_seminorm R) (λ (_x : ring_seminorm R), R → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

ring_seminorm.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem ring_seminorm.to_fun_eq_coe {R : Type u_2} [non_unital_ring R] (p : ring_seminorm R) :

p.to_fun = ⇑p

source

@[ext]

theorem ring_seminorm.ext {R : Type u_2} [non_unital_ring R] {p q : ring_seminorm R} :

(∀ (x : R), ⇑p x = ⇑q x) → p = q

source

@[protected, instance]

def ring_seminorm.has_zero {R : Type u_2} [non_unital_ring R] :

has_zero (ring_seminorm R)

Equations

ring_seminorm.has_zero = {zero := {to_fun := 0.to_fun, map_zero' := _, add_le' := _, neg' := _, mul_le' := _}}

source

theorem ring_seminorm.eq_zero_iff {R : Type u_2} [non_unital_ring R] {p : ring_seminorm R} :

p = 0 ↔ ∀ (x : R), ⇑p x = 0

source

theorem ring_seminorm.ne_zero_iff {R : Type u_2} [non_unital_ring R] {p : ring_seminorm R} :

p ≠ 0 ↔ ∃ (x : R), ⇑p x ≠ 0

source

@[protected, instance]

def ring_seminorm.inhabited {R : Type u_2} [non_unital_ring R] :

inhabited (ring_seminorm R)

Equations

ring_seminorm.inhabited = {default := 0}

source

@[protected, instance]

def ring_seminorm.has_one {R : Type u_2} [non_unital_ring R] [decidable_eq R] :

has_one (ring_seminorm R)

The trivial seminorm on a ring R is the ring_seminorm taking value 0 at 0 and 1 at every other element.

Equations

ring_seminorm.has_one = {one := {to_fun := 1.to_fun, map_zero' := _, add_le' := _, neg' := _, mul_le' := _}}

source

@[simp]

theorem ring_seminorm.apply_one {R : Type u_2} [non_unital_ring R] [decidable_eq R] (x : R) :

⇑1 x = ite (x = 0) 0 1

source

theorem ring_seminorm.seminorm_one_eq_one_iff_ne_zero {R : Type u_2} [ring R] (p : ring_seminorm R) (hp : ⇑p 1 ≤ 1) :

⇑p 1 = 1 ↔ p ≠ 0

source

def norm_ring_seminorm (R : Type u_1) [non_unital_semi_normed_ring R] :

ring_seminorm R

The norm of a non_unital_semi_normed_ring as a ring_seminorm.

Equations

norm_ring_seminorm R = {to_fun := has_norm.norm non_unital_semi_normed_ring.to_has_norm, map_zero' := _, add_le' := _, neg' := _, mul_le' := _}

source

@[protected, instance]

def ring_norm.ring_norm_class {R : Type u_2} [non_unital_ring R] :

ring_norm_class (ring_norm R) R ℝ

Equations

ring_norm.ring_norm_class = {coe := λ (f : ring_norm R), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul_le_mul := _, eq_zero_of_map_eq_zero := _}

source

@[protected, instance]

def ring_norm.has_coe_to_fun {R : Type u_2} [non_unital_ring R] :

has_coe_to_fun (ring_norm R) (λ (_x : ring_norm R), R → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

ring_norm.has_coe_to_fun = {coe := λ (p : ring_norm R), p.to_fun}

source

@[simp]

theorem ring_norm.to_fun_eq_coe {R : Type u_2} [non_unital_ring R] (p : ring_norm R) :

p.to_fun = ⇑p

source

@[ext]

theorem ring_norm.ext {R : Type u_2} [non_unital_ring R] {p q : ring_norm R} :

(∀ (x : R), ⇑p x = ⇑q x) → p = q

source

@[protected, instance]

def ring_norm.has_one (R : Type u_2) [non_unital_ring R] [decidable_eq R] :

has_one (ring_norm R)

The trivial norm on a ring R is the ring_norm taking value 0 at 0 and 1 at every other element.

Equations

ring_norm.has_one R = {one := {to_fun := 1.to_fun, map_zero' := _, add_le' := _, neg' := _, mul_le' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp]

theorem ring_norm.apply_one (R : Type u_2) [non_unital_ring R] [decidable_eq R] (x : R) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def ring_norm.inhabited (R : Type u_2) [non_unital_ring R] [decidable_eq R] :

inhabited (ring_norm R)

Equations

ring_norm.inhabited R = {default := 1}

source

@[protected, instance]

def mul_ring_seminorm.mul_ring_seminorm_class {R : Type u_2} [non_assoc_ring R] :

mul_ring_seminorm_class (mul_ring_seminorm R) R ℝ

Equations

mul_ring_seminorm.mul_ring_seminorm_class = {coe := λ (f : mul_ring_seminorm R), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul := _, map_one := _}

source

@[protected, instance]

def mul_ring_seminorm.has_coe_to_fun {R : Type u_2} [non_assoc_ring R] :

has_coe_to_fun (mul_ring_seminorm R) (λ (_x : mul_ring_seminorm R), R → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

mul_ring_seminorm.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem mul_ring_seminorm.to_fun_eq_coe {R : Type u_2} [non_assoc_ring R] (p : mul_ring_seminorm R) :

p.to_fun = ⇑p

source

@[ext]

theorem mul_ring_seminorm.ext {R : Type u_2} [non_assoc_ring R] {p q : mul_ring_seminorm R} :

(∀ (x : R), ⇑p x = ⇑q x) → p = q

source

@[protected, instance]

def mul_ring_seminorm.has_one {R : Type u_2} [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] :

has_one (mul_ring_seminorm R)

The trivial seminorm on a ring R is the mul_ring_seminorm taking value 0 at 0 and 1 at every other element.

Equations

mul_ring_seminorm.has_one = {one := {to_fun := 1.to_fun, map_zero' := _, add_le' := _, neg' := _, map_one' := _, map_mul' := _}}

source

@[simp]

theorem mul_ring_seminorm.apply_one {R : Type u_2} [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] (x : R) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def mul_ring_seminorm.inhabited {R : Type u_2} [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] :

inhabited (mul_ring_seminorm R)

Equations

mul_ring_seminorm.inhabited = {default := 1}

source

@[protected, instance]

def mul_ring_norm.mul_ring_norm_class {R : Type u_2} [non_assoc_ring R] :

mul_ring_norm_class (mul_ring_norm R) R ℝ

Equations

mul_ring_norm.mul_ring_norm_class = {coe := λ (f : mul_ring_norm R), f.to_fun, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul := _, map_one := _, eq_zero_of_map_eq_zero := _}

source

@[protected, instance]

def mul_ring_norm.has_coe_to_fun {R : Type u_2} [non_assoc_ring R] :

has_coe_to_fun (mul_ring_norm R) (λ (_x : mul_ring_norm R), R → ℝ)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations

mul_ring_norm.has_coe_to_fun = {coe := λ (p : mul_ring_norm R), p.to_fun}

source

@[simp]

theorem mul_ring_norm.to_fun_eq_coe {R : Type u_2} [non_assoc_ring R] (p : mul_ring_norm R) :

p.to_fun = ⇑p

source

@[ext]

theorem mul_ring_norm.ext {R : Type u_2} [non_assoc_ring R] {p q : mul_ring_norm R} :

(∀ (x : R), ⇑p x = ⇑q x) → p = q

source

@[protected, instance]

def mul_ring_norm.has_one (R : Type u_2) [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] :

has_one (mul_ring_norm R)

The trivial norm on a ring R is the mul_ring_norm taking value 0 at 0 and 1 at every other element.

Equations

mul_ring_norm.has_one R = {one := {to_fun := 1.to_fun, map_zero' := _, add_le' := _, neg' := _, map_one' := _, map_mul' := _, eq_zero_of_map_eq_zero' := _}}

source

@[simp]

theorem mul_ring_norm.apply_one (R : Type u_2) [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] (x : R) :

⇑1 x = ite (x = 0) 0 1

source

@[protected, instance]

def mul_ring_norm.inhabited (R : Type u_2) [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] :

inhabited (mul_ring_norm R)

Equations

mul_ring_norm.inhabited R = {default := 1}

source

def ring_seminorm.to_ring_norm {K : Type u_1} [field K] (f : ring_seminorm K) (hnt : f ≠ 0) :

ring_norm K

A nonzero ring seminorm on a field K is a ring norm.

Equations

f.to_ring_norm hnt = {to_fun := f.to_fun, map_zero' := _, add_le' := _, neg' := _, mul_le' := _, eq_zero_of_map_eq_zero' := _}

source

@[simp]

theorem norm_ring_norm_to_fun (R : Type u_1) [non_unital_normed_ring R] (ᾰ : R) :

(norm_ring_norm R).to_fun ᾰ = (norm_add_group_norm R).to_fun ᾰ

source

def norm_ring_norm (R : Type u_1) [non_unital_normed_ring R] :

ring_norm R

The norm of a normed_ring as a ring_norm.

Equations

norm_ring_norm R = {to_fun := (norm_add_group_norm R).to_fun, map_zero' := _, add_le' := _, neg' := _, mul_le' := _, eq_zero_of_map_eq_zero' := _}