Equivalent power-multiplicative norms

In this file, we prove BGR, Proposition 3.1.5/1: if R is a normed commutative ring and f₁ and f₂ are two power-multiplicative R-algebra norms on S, then if f₁ and f₂ are equivalent on every subring R[y] for y : S, it follows that f₁ = f₂.

Main Results

• eq_of_powMul_faithful : the proof of BGR, Proposition 3.1.5/1.

References

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

Tags

norm, equivalent, power-multiplicative

theorem contraction_of_isPowMul_of_boundedWrt {F : Type u_1} {α : outParam (Type u_2)} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {β : Type u_3} [Ring β] (nα : F) {nβ : β → ℝ} (hβ : IsPowMul nβ) {f : α →+* β} (hf : RingHom.IsBoundedWrt (⇑nα) nβ f) (x : α) : nβ (f x) ≤ nα x

If f : α →+* β is bounded with respect to a ring seminorm nα on α and a power-multiplicative function nβ : β → ℝ, then ∀ x : α, nβ (f x) ≤ nα x.

theorem contraction_of_isPowMul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedRing β] (hβ : IsPowMul norm) {f : α →+* β} (hf : f.IsBounded) (x : α) : ‖f x‖ ≤ ‖x‖

Given a bounded f : α →+* β between seminormed rings, is the seminorm on β is power-multiplicative, then f is a contraction.

theorem eq_seminorms {F : Type u_1} {α : outParam (Type u_2)} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f g : F} (hfpm : IsPowMul ⇑f) (hgpm : IsPowMul ⇑g) (hfg : ∃ (r : ℝ) (_ : 0 < r), ∀ (a : α), f a ≤ r * g a) (hgf : ∃ (r : ℝ) (_ : 0 < r), ∀ (a : α), g a ≤ r * f a) : f = g

Given two power-multiplicative ring seminorms f, g on α, if f is bounded by a positive multiple of g and vice versa, then f = g.

theorem eq_of_powMul_faithful {R : Type u_1} {S : Type u_2} [NormedCommRing R] [CommRing S] [Algebra R S] (f₁ : AlgebraNorm R S) (hf₁_pm : IsPowMul ⇑f₁) (f₂ : AlgebraNorm R S) (hf₂_pm : IsPowMul ⇑f₂) (h_eq : ∀ (y : S), ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x) : f₁ = f₂

If R is a normed commutative ring and f₁ and f₂ are two power-multiplicative R-algebra norms on S, then if f₁ and f₂ are equivalent on every subring R[y] for y : S, it follows that f₁ = f₂ BGR, Proposition 3.1.5/1.