# 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) [] [] :

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

The unitary elements embed into the units.

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

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

Equations
• = { toFun := Subtype.map f , map_one' := , map_mul' := }
Instances For
theorem unitary.toUnits_comp_map {F : Type u_2} {R : Type u_3} {S : Type u_4} [] [] [] [] [FunLike F R S] [StarHomClass F R S] [] (f : F) :
unitary.toUnits.comp () = ().comp unitary.toUnits
Equations
• unitary.instCommGroupSubtypeMemSubmonoid = let __src := inferInstanceAs (Group ()); let __src_1 := ().toCommMonoid;
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [] [] {U : R} :
U star U * U = 1
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [] [] {U : R} :
U U * star U = 1
theorem unitary.coe_inv {R : Type u_1} [] [] (U : ()) :
U⁻¹ = (U)⁻¹
theorem unitary.coe_div {R : Type u_1} [] [] (U₁ : ()) (U₂ : ()) :
(U₁ / U₂) = U₁ / U₂
theorem unitary.coe_zpow {R : Type u_1} [] [] (U : ()) (z : ) :
(U ^ z) = U ^ z
instance unitary.instNegSubtypeMemSubmonoid {R : Type u_1} [Ring R] [] :
Neg ()
Equations
• unitary.instNegSubtypeMemSubmonoid = { neg := fun (U : ()) => -U, }
theorem unitary.coe_neg {R : Type u_1} [Ring R] [] (U : ()) :
(-U) = -U
Equations