Documentation

Mathlib.Algebra.Star.Unitary

Unitary elements of a star monoid #

This file defines unitary R, where R is a star monoid, as the submonoid made of the elements that satisfy star U * U = 1 and U * star U = 1, and these form a group. This includes, for instance, unitary operators on Hilbert spaces.

See also Matrix.UnitaryGroup for specializations to unitary (Matrix n n R).

Tags #

unitary

def unitary (R : Type u_1) [Monoid R] [StarMul R] :

In a *-monoid, unitary R is the submonoid consisting of all the elements U of R such that star U * U = 1 and U * star U = 1.

Equations
Instances For
    theorem unitary.mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
    U unitary R star U * U = 1 U * star U = 1
    @[simp]
    theorem unitary.star_mul_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U unitary R) :
    star U * U = 1
    @[simp]
    theorem unitary.mul_star_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U unitary R) :
    U * star U = 1
    theorem unitary.star_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U unitary R) :
    @[simp]
    theorem unitary.star_mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :
    Equations
    • unitary.instStarSubtypeMemSubmonoid = { star := fun (U : (unitary R)) => star U, }
    @[simp]
    theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : (unitary R)} :
    (star U) = star U
    theorem unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
    star U * U = 1
    theorem unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
    U * (star U) = 1
    @[simp]
    theorem unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
    star U * U = 1
    @[simp]
    theorem unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
    U * star U = 1
    Equations
    • unitary.instGroupSubtypeMemSubmonoid = let __src := (unitary R).toMonoid; Group.mk
    Equations
    Equations
    • unitary.instStarMulSubtypeMemSubmonoid = StarMul.mk
    Equations
    • unitary.instInhabitedSubtypeMemSubmonoid = { default := 1 }
    theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
    theorem unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] :
    star = Inv.inv
    @[simp]
    theorem unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : (unitary R)) :
    (unitary.toUnits x)⁻¹ = x⁻¹
    @[simp]
    theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : (unitary R)) :
    (unitary.toUnits x) = x
    def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
    (unitary R) →* Rˣ

    The unitary elements embed into the units.

    Equations
    • unitary.toUnits = { toFun := fun (x : (unitary R)) => { val := x, inv := x⁻¹, val_inv := , inv_val := }, map_one' := , map_mul' := }
    Instances For
      theorem unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] :
      Function.Injective unitary.toUnits
      theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) (h_mul : star u * u = 1) :
      theorem IsUnit.mem_unitary_of_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) (h_mul : u * star u = 1) :
      instance unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : (unitary R)) :
      Equations
      • =
      instance unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : (unitary R)) :
      Equations
      • =
      theorem isStarNormal_of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u unitary R) :
      theorem unitary.map_mem {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r unitary R) :
      f r unitary S
      @[simp]
      theorem unitary.map_apply {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) :
      ∀ (a : (unitary R)), (unitary.map f) a = Subtype.map f a
      def unitary.map {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) :
      (unitary R) →* (unitary S)

      The group homomorphism between unitary subgroups of star monoids induced by a star homomorphism

      Equations
      Instances For
        theorem unitary.toUnits_comp_map {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) :
        unitary.toUnits.comp (unitary.map f) = (Units.map f).comp unitary.toUnits
        Equations
        theorem unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
        U unitary R star U * U = 1
        theorem unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :
        U unitary R U * star U = 1
        theorem unitary.coe_inv {R : Type u_1} [GroupWithZero R] [StarMul R] (U : (unitary R)) :
        U⁻¹ = (U)⁻¹
        theorem unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ : (unitary R)) (U₂ : (unitary R)) :
        (U₁ / U₂) = U₁ / U₂
        theorem unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : (unitary R)) (z : ) :
        (U ^ z) = U ^ z
        instance unitary.instNegSubtypeMemSubmonoid {R : Type u_1} [Ring R] [StarRing R] :
        Neg (unitary R)
        Equations
        • unitary.instNegSubtypeMemSubmonoid = { neg := fun (U : (unitary R)) => -U, }
        theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : (unitary R)) :
        (-U) = -U
        Equations
        @[simp]
        theorem unitary.spectrum.unitary_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : (unitary A)} :
        spectrum R (u * a * star u) = spectrum R a

        Unitary conjugation preserves the spectrum, star on left.

        @[simp]
        theorem unitary.spectrum.unitary_conjugate' {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : (unitary A)} :
        spectrum R (star u * a * u) = spectrum R a

        Unitary conjugation preserves the spectrum, star on right.