The left-regular representation is an isometry for C⋆-algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
op_nnnorm_mul
(𝕜 : Type u_1)
{E : Type u_2}
[densely_normed_field 𝕜]
[non_unital_normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_space 𝕜 E]
[is_scalar_tower 𝕜 E E]
[smul_comm_class 𝕜 E E]
(a : E) :
In a C⋆-algebra E, either unital or non-unital, multiplication on the left by a : E has
norm equal to the norm of a.
@[simp]
theorem
op_nnnorm_mul_flip
(𝕜 : Type u_1)
{E : Type u_2}
[densely_normed_field 𝕜]
[non_unital_normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_space 𝕜 E]
[is_scalar_tower 𝕜 E E]
[smul_comm_class 𝕜 E E]
(a : E) :
In a C⋆-algebra E, either unital or non-unital, multiplication on the right by a : E has
norm eqaul to the norm of a.
theorem
mul_isometry
(𝕜 : Type u_1)
(E : Type u_2)
[densely_normed_field 𝕜]
[non_unital_normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_space 𝕜 E]
[is_scalar_tower 𝕜 E E]
[smul_comm_class 𝕜 E E] :
In a C⋆-algebra E, either unital or non-unital, the left regular representation is an
isometry.
theorem
mul_flip_isometry
(𝕜 : Type u_1)
(E : Type u_2)
[densely_normed_field 𝕜]
[non_unital_normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_space 𝕜 E]
[is_scalar_tower 𝕜 E E]
[smul_comm_class 𝕜 E E] :
isometry ⇑((continuous_linear_map.mul 𝕜 E).flip)
In a C⋆-algebra E, either unital or non-unital, the right regular anti-representation is an
isometry.