Norms on completions of seminormed rings

The norm of the completion of a seminormed ring extends the norm of the ring by continuity, so identities and inequalities between continuous functions of the norm pass from the ring to its completion. This file records that submultiplicativity without a unit, multiplicativity, ‖x * y‖ = ‖x‖ * ‖y‖, and power-multiplicativity, ‖x ^ n‖ = ‖x‖ ^ n, are such properties. Completing a nonunital seminormed ring, such as an L¹ convolution algebra on compactly supported functions, therefore gives a complete nonunital normed ring. Isometry of a star operation passes to the completion by UniformSpace.Completion.instNormedStarGroup in TauCeti.Analysis.CStarAlgebra.Completion. A power-multiplicative norm determines the power-bounded elements of a normed ring with a pseudouniformizer: they are exactly the elements of norm at most one (TauCeti.Huber.IsPseudoUniformizer.isPowerBounded_iff_norm_le_one).

Main results

• IsPowMul.completion: the norm of the completion of a seminormed ring with a power-multiplicative norm is power-multiplicative.
• UniformSpace.Completion.instNormMulClass: the norm of the completion of a nonunital seminormed ring with a multiplicative norm is multiplicative.
• UniformSpace.Completion.instNormOneClass: the completion of a seminormed ring in which 1 has norm 1 has the same property.
• UniformSpace.Completion.instNonUnitalNormedRing: the completion of a nonunital seminormed ring is a nonunital normed ring.

theorem IsPowMul.completion {R : Type u_1} [SeminormedRing R] (h : IsPowMul fun (x : R) => ‖x‖) : IsPowMul fun (x : UniformSpace.Completion R) => ‖x‖

The completion of a seminormed ring with a power-multiplicative norm has a power-multiplicative norm.

instance UniformSpace.Completion.instNormMulClass {R : Type u_1} [NonUnitalSeminormedRing R] [NormMulClass R] : NormMulClass (Completion R)

The completion of a nonunital seminormed ring with a multiplicative norm has a multiplicative norm.

instance UniformSpace.Completion.instNormOneClass {R : Type u_1} [SeminormedRing R] [NormOneClass R] : NormOneClass (Completion R)

The completion of a seminormed ring in which 1 has norm 1 has the same property.

@[instance_reducible]

noncomputable instance UniformSpace.Completion.instNonUnitalNormedRing {R : Type u_1} [NonUnitalSeminormedRing R] : NonUnitalNormedRing (Completion R)

The completion of a nonunital seminormed ring is a nonunital normed ring. For a ring with unit this is the nonunital part of Mathlib's NormedRing instance on the completion.