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) [inst : Monoid R] [inst : StarSemigroup 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.
theorem unitary.mem_iff {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup 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} [inst : Monoid R] [inst : StarSemigroup R] {U : R} (hU : U unitary R) :
star U * U = 1
@[simp]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] {U : R} (hU : U unitary R) :
U * star U = 1
theorem unitary.star_mem {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] {U : R} (hU : U unitary R) :
@[simp]
theorem unitary.star_mem_iff {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] {U : R} :
Equations
  • unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { star := fun U => { val := star U, property := (_ : star U unitary R) } }
@[simp]
theorem unitary.coe_star {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] {U : { x // x unitary R }} :
↑(star U) = star U
theorem unitary.coe_star_mul_self {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
star U * U = 1
theorem unitary.coe_mul_star_self {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
U * ↑(star U) = 1
@[simp]
theorem unitary.star_mul_self {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
star U * U = 1
@[simp]
theorem unitary.mul_star_self {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
U * star U = 1
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { default := 1 }
theorem unitary.star_eq_inv {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
theorem unitary.star_eq_inv' {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] :
star = Inv.inv
@[simp]
theorem unitary.toUnits_apply_val {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (x : { x // x unitary R }) :
↑(unitary.toUnits x) = x
@[simp]
theorem unitary.toUnits_apply_inv {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (x : { x // x unitary R }) :
(unitary.toUnits x).inv = x⁻¹
def unitary.toUnits {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] :
{ x // x unitary R } →* Rˣ

The unitary elements embed into the units.

Equations
  • One or more equations did not get rendered due to their size.
theorem unitary.to_units_injective {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup 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} [inst : CommMonoid R] [inst : StarSemigroup R] {U : R} :
U unitary R star U * U = 1
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [inst : CommMonoid R] [inst : StarSemigroup R] {U : R} :
U unitary R U * star U = 1
theorem unitary.coe_inv {R : Type u_1} [inst : GroupWithZero R] [inst : StarSemigroup R] (U : { x // x unitary R }) :
U⁻¹ = (U)⁻¹
theorem unitary.coe_div {R : Type u_1} [inst : GroupWithZero R] [inst : StarSemigroup R] (U₁ : { x // x unitary R }) (U₂ : { x // x unitary R }) :
↑(U₁ / U₂) = U₁ / U₂
theorem unitary.coe_zpow {R : Type u_1} [inst : GroupWithZero R] [inst : StarSemigroup R] (U : { x // x unitary R }) (z : ) :
↑(U ^ z) = U ^ z
theorem unitary.coe_neg {R : Type u_1} [inst : Ring R] [inst : StarRing R] (U : { x // x unitary R }) :
↑(-U) = -U