The left-regular representation is an isometry for Cā-algebras #
@[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] :
isometry ā(continuous_linear_map.mul š 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.