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
        @[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
          theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : (unitary R)) :
          def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
          (unitary R) →* Rˣ

          The unitary elements embed into the units.

          Equations
            Instances For
              @[simp]
              theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : (unitary R)) :
              (toUnits x) = x
              @[simp]
              theorem unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : (unitary R)) :
              (toUnits x)⁻¹ = x⁻¹
              theorem IsUnit.mem_unitary_iff_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
              u unitary R star u * u = 1
              theorem IsUnit.mem_unitary_iff_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
              u unitary R u * star u = 1
              theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
              star u * u = 1u unitary R

              Alias of the reverse direction of IsUnit.mem_unitary_iff_star_mul_self.

              theorem IsUnit.mem_unitary_of_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
              u * star u = 1u unitary R

              Alias of the reverse direction of IsUnit.mem_unitary_iff_mul_star_self.

              theorem unitary.mul_inv_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
              a * b⁻¹ unitary G star a * a = star b * b
              theorem unitary.inv_mul_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
              a⁻¹ * b unitary G a * star a = b * star b
              theorem Units.mul_inv_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :
              a * b⁻¹ unitary R star a * a = star b * b

              In a star monoid, the product a * b⁻¹ of units is unitary if star a * a = star b * b.

              theorem Units.inv_mul_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :
              a⁻¹ * b unitary R a * star a = b * star b

              In a star monoid, the product a⁻¹ * b of units is unitary if a * star a = b * star b.

              instance unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : (unitary R)) :
              instance unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : (unitary R)) :
              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
              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
                  @[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)) :
                  (map f) a✝ = Subtype.map f a✝
                  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) :
                  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₁ 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
                    theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : (unitary R)) :
                    ↑(-U) = -U
                    @[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.