Multiplicative units in monoids with norms

A multiplicative unit is an invertible element whose left multiplication scales every norm by its own norm. This notion uses only multiplication and a real-valued norm; no addition or norm inequality is required. It singles out the units needed in norm estimates when the norm need not be multiplicative.

Multiplicative units are closed under multiplication and inversion, and norm-preserving multiplicative equivalences preserve and reflect them. Powers of multiplicative units are multiplicative units. In a norm-one monoid, so is one, and the norms of powers are the powers of the norm. In a commutative norm-one monoid, finite products of multiplicative units are multiplicative units, with the product of the norms as norm.

An element of nonzero norm scaling all norms exactly forces ‖1‖ = 1; if it is a unit, its inverse has reciprocal norm.

References

• F. Martin, Overconvergent subanalytic subsets in the framework of Berkovich spaces, J. Eur. Math. Soc. 18 (2016), Definition 1.20 and Lemma 1.21.

Units scaling the norm exactly

theorem TauCeti.NormedRing.norm_one_of_norm_mul {R : Type u_1} [MulOneClass R] [Norm R] {u : R} (hu0 : ‖u‖ ≠ 0) (hu : ∀ (x : R), ‖u * x‖ = ‖u‖ * ‖x‖) : ‖1‖ = 1

An element of nonzero norm by which left multiplication scales the norm exactly forces ‖1‖ = 1.

theorem TauCeti.NormedRing.norm_eq_zero_of_norm_mul {R : Type u_1} [Monoid R] [Norm R] {u : Rˣ} (hu0 : ‖↑u‖ = 0) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) (x : R) : ‖x‖ = 0

A unit of zero norm by which left multiplication scales the norm exactly forces every element to have zero norm.

theorem TauCeti.NormedRing.norm_units_inv_of_norm_mul {R : Type u_1} [Monoid R] [Norm R] {u : Rˣ} (hu0 : ‖↑u‖ ≠ 0) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) : ‖↑u⁻¹‖ = ‖↑u‖⁻¹

A unit of nonzero norm by which left multiplication scales the norm exactly has inverse of norm ‖u‖⁻¹.

def TauCeti.IsNormMulUnit {R : Type u_1} [Monoid R] [Norm R] (u : R) : Prop

A multiplicative unit is a unit whose left multiplication scales norms exactly.

theorem TauCeti.isNormMulUnit_iff {R : Type u_1} [Monoid R] [Norm R] (u : R) : IsNormMulUnit u ↔ IsUnit u ∧ ∀ (x : R), ‖u * x‖ = ‖u‖ * ‖x‖

The characteristic criterion for being a multiplicative unit.

theorem TauCeti.IsNormMulUnit.isUnit {R : Type u_1} [Monoid R] [Norm R] {u : R} (hu : IsNormMulUnit u) : IsUnit u

A multiplicative unit is invertible.

theorem TauCeti.IsNormMulUnit.norm_mul {R : Type u_1} [Monoid R] [Norm R] {u : R} (hu : IsNormMulUnit u) (x : R) : ‖u * x‖ = ‖u‖ * ‖x‖

Left multiplication by a multiplicative unit scales norms exactly.

theorem TauCeti.IsNormMulUnit.mul {R : Type u_1} [Monoid R] [Norm R] {u v : R} (hu : IsNormMulUnit u) (hv : IsNormMulUnit v) : IsNormMulUnit (u * v)

Multiplicative units are closed under multiplication.

@[simp]

theorem TauCeti.isNormMulUnit_one {R : Type u_1} [Monoid R] [Norm R] [NormOneClass R] : IsNormMulUnit 1

One is a multiplicative unit in a norm-one monoid.

theorem TauCeti.IsNormMulUnit.pow {R : Type u_1} [Monoid R] [Norm R] {u : R} (hu : IsNormMulUnit u) (n : ℕ) : IsNormMulUnit (u ^ n)

Powers of a multiplicative unit are multiplicative units.

theorem TauCeti.IsNormMulUnit.norm_pow {R : Type u_1} [Monoid R] [Norm R] [NormOneClass R] {u : R} (hu : IsNormMulUnit u) (n : ℕ) : ‖u ^ n‖ = ‖u‖ ^ n

The norm of a power of a multiplicative unit is the power of its norm.

theorem TauCeti.IsNormMulUnit.units_inv {R : Type u_1} [Monoid R] [Norm R] {u : Rˣ} (hu : IsNormMulUnit ↑u) : IsNormMulUnit ↑u⁻¹

The inverse of a multiplicative unit is again multiplicative.

theorem TauCeti.IsNormMulUnit.prod {ι : Type u_3} {A : Type u_4} [CommMonoid A] [Norm A] [NormOneClass A] {s : Finset ι} {u : ι → A} (hu : ∀ i ∈ s, IsNormMulUnit (u i)) : IsNormMulUnit (∏ i ∈ s, u i)

Finite products of multiplicative units are multiplicative units.

theorem TauCeti.IsNormMulUnit.norm_prod {ι : Type u_3} {A : Type u_4} [CommMonoid A] [Norm A] [NormOneClass A] {s : Finset ι} {u : ι → A} (hu : ∀ i ∈ s, IsNormMulUnit (u i)) : ‖∏ i ∈ s, u i‖ = ∏ i ∈ s, ‖u i‖

The norm of a finite product of multiplicative units is the product of their norms.

theorem TauCeti.isNormMulUnit_iff_isUnit {R : Type u_1} [Monoid R] [Norm R] [NormMulClass R] (u : R) : IsNormMulUnit u ↔ IsUnit u

In a monoid with multiplicative norm every unit is a multiplicative unit.

theorem MulEquiv.isNormMulUnit_iff {R : Type u_1} {S : Type u_2} [Monoid R] [Norm R] [Monoid S] [Norm S] (e : R ≃* S) (he : ∀ (x : R), ‖e x‖ = ‖x‖) (u : R) : TauCeti.IsNormMulUnit (e u) ↔ TauCeti.IsNormMulUnit u

Norm-preserving multiplicative equivalences preserve and reflect multiplicative units.