# The ⋆-algebra automorphism given by a unitary element #

This file defines the ⋆-algebra automorphism on `R` given by a unitary `u`, which is `Unitary.conjStarAlgAut S R u`, defined to be `x ↦ u * x * star u`.

source
def Unitary.conjStarAlgAut (S : Type u_1) (R : Type u_2) [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] :
↥(unitary R) →* R ≃⋆ₐ[S] R

Each unitary element `u` defines a ⋆-algebra automorphism such that `x ↦ u * x * star u`.

This is the ⋆-algebra automorphism version of a specialized version of `MulSemiringAction.toAlgAut`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Unitary.conjStarAlgAut_apply {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u : ↥(unitary R)) (x : R) :
((conjStarAlgAut S R) u) x = ↑u * x * star ↑u
source
theorem Unitary.conjStarAlgAut_symm_apply {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u : ↥(unitary R)) (x : R) :
((conjStarAlgAut S R) u).symm x = star ↑u * x * ↑u
source
theorem Unitary.conjStarAlgAut_star_apply {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u : ↥(unitary R)) (x : R) :
((conjStarAlgAut S R) (star u)) x = star ↑u * x * ↑u
source
@[simp]
theorem Unitary.conjStarAlgAut_symm {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u : ↥(unitary R)) :
((conjStarAlgAut S R) u).symm = (conjStarAlgAut S R) (star u)
source
theorem Unitary.conjStarAlgAut_trans_conjStarAlgAut {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u₁ u₂ : ↥(unitary R)) :
((conjStarAlgAut S R) u₁).trans ((conjStarAlgAut S R) u₂) = (conjStarAlgAut S R) (u₂ * u₁)
source
theorem Unitary.conjStarAlgAut_mul_apply {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u₁ u₂ : ↥(unitary R)) (x : R) :
((conjStarAlgAut S R) (u₁ * u₂)) x = ((conjStarAlgAut S R) u₁) (((conjStarAlgAut S R) u₂) x)
source
theorem Unitary.toRingEquiv_conjStarAlgAut {S : Type u_1} {R : Type u_2} [Semiring R] [StarMul R] [SMul S R] [IsScalarTower S R R] [SMulCommClass S R R] (u : ↥(unitary R)) :
((conjStarAlgAut S R) u).toRingEquiv = MulSemiringAction.toRingEquiv (ConjAct R ˣ) R (ConjAct.toConjAct (toUnits u))
source
theorem Unitary.toAlgEquiv_conjStarAlgAut {R : Type u_2} [Semiring R] [StarMul R] {S : Type u_3} [CommSemiring S] [Algebra S R] (u : ↥(unitary R)) :
((conjStarAlgAut S R) u).toAlgEquiv = MulSemiringAction.toAlgEquiv S R (ConjAct.toConjAct (toUnits u))