Documentation

Mathlib.Algebra.Star.UnitaryStarAlgAut

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))
    source
    theorem Unitary.conjStarAlgAut_ext_iff {R : Type u_2} [Semiring R] [StarMul R] {S : Type u_3} [CommSemiring S] [Algebra S R] [Algebra.IsCentral S R] (u v : ↥(unitary R)) :
    (conjStarAlgAut S R) u = (conjStarAlgAut S R) v ↔ ∃ (α : S), ↑u = α • ↑v
    source
    theorem Unitary.conjStarAlgAut_ext_iff' {R : Type u_3} {S : Type u_4} [Ring R] [StarMul R] [CommRing S] [StarMul S] [Algebra S R] [StarModule S R] [Algebra.IsCentral S R] [IsCancelMulZero S] [Module.IsTorsionFree S R] (u v : ↥(unitary R)) :
    (conjStarAlgAut S R) u = (conjStarAlgAut S R) v ↔ ∃ (α : ↥(unitary S)), u = α • v