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
  • One or more equations did not get rendered due to their size.
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.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { star := fun (U : (unitary R)) => { val := star U, property := (_ : star U unitary R) } }
    @[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
    Equations
    Equations
    • unitary.instStarMulSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryMul = StarMul.mk (_ : ∀ (x y : (unitary R)), star (x * y) = star y * star x)
    Equations
    • unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { 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
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem unitary.to_units_injective {R : Type u_1} [Monoid R] [StarMul R] :
      Function.Injective unitary.toUnits
      Equations
      • One or more equations did not get rendered due to their size.
      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
      theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : (unitary R)) :
      (-U) = -U