Unitary maps in C⋆-algebras

This file defines some basic maps by unitaries in C⋆-algebras.

noncomputable def Unitary.mulLeft (R : Type u_1) (A : Type u_2) [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] : ↥(unitary A) →* A ≃ₗᵢ[R] A

Left multiplication by a unitary as a linear isometric equivalence.

@[simp]

theorem Unitary.mulLeft_apply (R : Type u_1) {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u : ↥(unitary A)) (x : A) : ((mulLeft R A) u) x = ↑u * x

theorem Unitary.symm_mulLeft_apply (R : Type u_1) {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u : ↥(unitary A)) (x : A) : ((mulLeft R A) u).symm x = star ↑u * x

@[simp]

theorem Unitary.symm_mulLeft {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u : ↥(unitary A)) : ((mulLeft R A) u).symm = (mulLeft R A) (star u)

theorem Unitary.mulLeft_trans_mulLeft {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u v : ↥(unitary A)) : ((mulLeft R A) u).trans ((mulLeft R A) v) = (mulLeft R A) (v * u)

theorem Unitary.mulLeft_mul_apply {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u v : ↥(unitary A)) (x : A) : ((mulLeft R A) (u * v)) x = ((mulLeft R A) u) (((mulLeft R A) v) x)

@[simp]

theorem Unitary.toLinearEquiv_mulLeft {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [SMulCommClass R A A] (u : ↥(unitary A)) : ((mulLeft R A) u).toLinearEquiv = (Units.mulLeftLinearEquiv R A) (toUnits u)

noncomputable def Unitary.mulRight (R : Type u_1) {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) : A ≃ₗᵢ[R] A

Right multiplication by a unitary as a linear isometric equivalence.

@[simp]

theorem Unitary.mulRight_apply (R : Type u_1) {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) (x : A) : (mulRight R u) x = x * ↑u

theorem Unitary.symm_mulRight_apply (R : Type u_1) {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) (x : A) : (mulRight R u).symm x = x * star ↑u

@[simp]

theorem Unitary.symm_mulRight {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) : (mulRight R u).symm = mulRight R (star u)

theorem Unitary.mulRight_trans_mulRight {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u v : ↥(unitary A)) : (mulRight R u).trans (mulRight R v) = mulRight R (u * v)

theorem Unitary.mulRight_mul_apply {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u v : ↥(unitary A)) (x : A) : (mulRight R (u * v)) x = (mulRight R v) ((mulRight R u) x)

@[simp]

theorem Unitary.toLinearMap_mulRight {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) : ↑(mulRight R u).toLinearEquiv = LinearMap.mulRight R ↑u

@[simp]

theorem Unitary.mulRight_one {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] : mulRight R 1 = LinearIsometryEquiv.refl R A

@[simp]

theorem Unitary.toLinearEquiv_mulRight {R : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [CStarRing A] [Ring R] [Module R A] [IsScalarTower R A A] (u : ↥(unitary A)) : (mulRight R u).toLinearEquiv = Units.mulRightLinearEquiv R (toUnits u)