SeminormFromConst

In this file, we prove [BGR, Proposition 1.3.2/2][bosch-guntzer-remmert] : starting from a power-multiplicative seminorm on a commutative ring R and a nonzero c : R, we create a new power-multiplicative seminorm for which c is multiplicative.

Main Definitions

• seminormFromConst' : the real-valued function sending x ∈ R to the limit of (f (x * c^n))/((f c)^n).
• seminormFromConst : the function seminormFromConst' as a RingSeminorm on R.

Main Results

• seminormFromConst_isNonarchimedean : the function seminormFromConst' hf1 hc hpm is nonarchimedean when f is nonarchimedean.
• seminormFromConst_isPowMul : the function seminormFromConst' hf1 hc hpm is power-multiplicative.
• seminormFromConst_const_mul : for every x : R, seminormFromConst' hf1 hc hpm (c * x) equals the product seminormFromConst' hf1 hc hpm c * SeminormFromConst' hf1 hc hpm x.

References

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

Tags

SeminormFromConst, Seminorm, Nonarchimedean

def seminormFromConst_seq {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) : ℕ → ℝ

For a ring seminorm f on R and c ∈ R, the sequence given by (f (x * c^n))/((f c)^n).

Equations

• seminormFromConst_seq c f x n = f (x * c ^ n) / f c ^ n

theorem seminormFromConst_seq_def {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) : seminormFromConst_seq c f x = fun (n : ℕ) => f (x * c ^ n) / f c ^ n

theorem seminormFromConst_seq_nonneg {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) : 0 ≤ seminormFromConst_seq c f x

The terms in the sequence seminormFromConst_seq c f x are nonnegative.

theorem seminormFromConst_bddBelow {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) : BddBelow (Set.range (seminormFromConst_seq c f x))

The image of seminormFromConst_seq c f x is bounded below by zero.

theorem seminormFromConst_seq_zero {R : Type u_1} [CommRing R] (c : R) {f : RingSeminorm R} (hf : f 0 = 0) : seminormFromConst_seq c f 0 = 0

seminormFromConst_seq c f 0 is the constant sequence zero.

theorem seminormFromConst_seq_one {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (n : ℕ) (hn : 1 ≤ n) : seminormFromConst_seq c f 1 n = 1

If 1 ≤ n, then seminormFromConst_seq c f 1 n = 1.

theorem seminormFromConst_seq_antitone {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : Antitone (seminormFromConst_seq c f x)

seminormFromConst_seq c f x is antitone.

def seminormFromConst' {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : ℝ

The real-valued function sending x ∈ R to the limit of (f (x * c^n))/((f c)^n).

Equations

• seminormFromConst' hf1 hc hpm x = ⋯.choose

theorem seminormFromConst_isLimit {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (nhds (seminormFromConst' hf1 hc hpm x))

We prove that seminormFromConst' hf1 hc hpm x is the limit of the sequence seminormFromConst_seq c f x as n tends to infinity.

theorem seminormFromConst_one {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) : seminormFromConst' hf1 hc hpm 1 = 1

seminormFromConst' hf1 hc hpm 1 = 1.

def seminormFromConst {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) : RingSeminorm R

The function seminormFromConst is a RingSeminorm on R.

Equations

• seminormFromConst hf1 hc hpm = { toFun := seminormFromConst' hf1 hc hpm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯ }

theorem seminormFromConst_def {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : (seminormFromConst hf1 hc hpm) x = seminormFromConst' hf1 hc hpm x

theorem seminormFromConst_one_le {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) : seminormFromConst' hf1 hc hpm 1 ≤ 1

seminormFromConst' hf1 hc hpm 1 ≤ 1.

theorem seminormFromConst_isNonarchimedean {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (hna : IsNonarchimedean ⇑f) : IsNonarchimedean (seminormFromConst' hf1 hc hpm)

The function seminormFromConst' hf1 hc hpm is nonarchimedean.

theorem seminormFromConst_isPowMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) : IsPowMul (seminormFromConst' hf1 hc hpm)

The function seminormFromConst' hf1 hc hpm is power-multiplicative.

theorem seminormFromConst_le_seminorm {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : seminormFromConst' hf1 hc hpm x ≤ f x

The function seminormFromConst' hf1 hc hpm is bounded above by f.

theorem seminormFromConst_apply_of_isMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) : seminormFromConst' hf1 hc hpm x = f x

If x : R is multiplicative for f, then seminormFromConst' hf1 hc hpm x = f x.

theorem seminormFromConst_isMul_of_isMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) (y : R) : seminormFromConst' hf1 hc hpm (x * y) = seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y

If x : R is multiplicative for f, then it is multiplicative for seminormFromConst' hf1 hc hpm.

theorem seminormFromConst_apply_c {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) : seminormFromConst' hf1 hc hpm c = f c

seminormFromConst' hf1 hc hpm c = f c.

theorem seminormFromConst_const_mul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 ≤ 1) (hc : f c ≠ 0) (hpm : IsPowMul ⇑f) (x : R) : seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

For every x : R, seminormFromConst' hf1 hc hpm (c * x) equals the product seminormFromConst' hf1 hc hpm c * SeminormFromConst' hf1 hc hpm x.

def normFromConst {K : Type u_1} [Field K] {k : K} {g : RingSeminorm K} (hg1 : g 1 ≤ 1) (hg_k : g k ≠ 0) (hg_pm : IsPowMul ⇑g) : RingNorm K

If K is a field, the function seminormFromConst is a RingNorm on K.

Equations

• normFromConst hg1 hg_k hg_pm = (seminormFromConst hg1 hg_k hg_pm).toRingNorm ⋯

theorem seminormFromConstRingNormOfField_def {K : Type u_1} [Field K] {k : K} {g : RingSeminorm K} (hg1 : g 1 ≤ 1) (hg_k : g k ≠ 0) (hg_pm : IsPowMul ⇑g) (x : K) : (normFromConst hg1 hg_k hg_pm) x = seminormFromConst' hg1 hg_k hg_pm x