mathlib3 documentation

algebra.star.unitary

Unitary elements of a star monoid #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.unitary_group for specializations to unitary (matrix n n R).

Tags #

unitary

source
def unitary (R : Type u_1) [monoid R] [star_semigroup R] :
submonoid 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 ↥unitary
source
theorem unitary.mem_iff {R : Type u_1} [monoid R] [star_semigroup R] {U : R} :
U ∈ unitary R ↔ has_star.star U * U = 1 ∧ U * has_star.star U = 1
source
@[simp]
theorem unitary.star_mul_self_of_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U ∈ unitary R) :
has_star.star U * U = 1
source
@[simp]
theorem unitary.mul_star_self_of_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U ∈ unitary R) :
U * has_star.star U = 1
source
theorem unitary.star_mem {R : Type u_1} [monoid R] [star_semigroup R] {U : R} (hU : U ∈ unitary R) :
has_star.star U ∈ unitary R
source
@[simp]
theorem unitary.star_mem_iff {R : Type u_1} [monoid R] [star_semigroup R] {U : R} :
has_star.star U ∈ unitary R ↔ U ∈ unitary R
source
@[protected, instance]
def unitary.has_star {R : Type u_1} [monoid R] [star_semigroup R] :
has_star ↥(unitary R)
Equations
source
@[simp, norm_cast]
theorem unitary.coe_star {R : Type u_1} [monoid R] [star_semigroup R] {U : ↥(unitary R)} :
↑(has_star.star U) = has_star.star ↑U
source
theorem unitary.coe_star_mul_self {R : Type u_1} [monoid R] [star_semigroup R] (U : ↥(unitary R)) :
has_star.star ↑U * ↑U = 1
source
theorem unitary.coe_mul_star_self {R : Type u_1} [monoid R] [star_semigroup R] (U : ↥(unitary R)) :
↑U * has_star.star ↑U = 1
source
@[simp]
theorem unitary.star_mul_self {R : Type u_1} [monoid R] [star_semigroup R] (U : ↥(unitary R)) :
has_star.star U * U = 1
source
@[simp]
theorem unitary.mul_star_self {R : Type u_1} [monoid R] [star_semigroup R] (U : ↥(unitary R)) :
U * has_star.star U = 1
source
@[protected, instance]
def unitary.group {R : Type u_1} [monoid R] [star_semigroup R] :
group ↥(unitary R)
Equations
source
@[protected, instance]
def unitary.has_involutive_star {R : Type u_1} [monoid R] [star_semigroup R] :
has_involutive_star ↥(unitary R)
Equations
source
@[protected, instance]
def unitary.star_semigroup {R : Type u_1} [monoid R] [star_semigroup R] :
star_semigroup ↥(unitary R)
Equations
source
@[protected, instance]
def unitary.inhabited {R : Type u_1} [monoid R] [star_semigroup R] :
inhabited ↥(unitary R)
Equations
source
theorem unitary.star_eq_inv {R : Type u_1} [monoid R] [star_semigroup R] (U : ↥(unitary R)) :
has_star.star U = U⁻¹
source
theorem unitary.star_eq_inv' {R : Type u_1} [monoid R] [star_semigroup R] :
has_star.star = has_inv.inv
source
@[simp]
theorem unitary.coe_to_units_apply {R : Type u_1} [monoid R] [star_semigroup R] (x : ↥(unitary R)) :
↑(⇑unitary.to_units x) = ↑x
source
def unitary.to_units {R : Type u_1} [monoid R] [star_semigroup R] :
↥(unitary R) →* Rˣ

The unitary elements embed into the units.

Equations
source
@[simp]
theorem unitary.coe_inv_to_units_apply {R : Type u_1} [monoid R] [star_semigroup R] (x : ↥(unitary R)) :
↑(⇑unitary.to_units x)⁻¹ = ↑x⁻¹
source
theorem unitary.to_units_injective {R : Type u_1} [monoid R] [star_semigroup R] :
function.injective ⇑unitary.to_units
source
@[protected, instance]
def unitary.comm_group {R : Type u_1} [comm_monoid R] [star_semigroup R] :
comm_group ↥(unitary R)
Equations
source
theorem unitary.mem_iff_star_mul_self {R : Type u_1} [comm_monoid R] [star_semigroup R] {U : R} :
U ∈ unitary R ↔ has_star.star U * U = 1
source
theorem unitary.mem_iff_self_mul_star {R : Type u_1} [comm_monoid R] [star_semigroup R] {U : R} :
U ∈ unitary R ↔ U * has_star.star U = 1
source
@[norm_cast]
theorem unitary.coe_inv {R : Type u_1} [group_with_zero R] [star_semigroup R] (U : ↥(unitary R)) :
↑U⁻¹ = (↑U)⁻¹
source
@[norm_cast]
theorem unitary.coe_div {R : Type u_1} [group_with_zero R] [star_semigroup R] (U₁ U₂ : ↥(unitary R)) :
↑(U₁ / U₂) = ↑U₁ / ↑U₂
source
@[norm_cast]
theorem unitary.coe_zpow {R : Type u_1} [group_with_zero R] [star_semigroup R] (U : ↥(unitary R)) (z : ℤ) :
↑(U ^ z) = ↑U ^ z
source
@[protected, instance]
def unitary.has_neg {R : Type u_1} [ring R] [star_ring R] :
has_neg ↥(unitary R)
Equations
source
@[norm_cast]
theorem unitary.coe_neg {R : Type u_1} [ring R] [star_ring R] (U : ↥(unitary R)) :
↑-U = -↑U
source
@[protected, instance]
def unitary.has_distrib_neg {R : Type u_1} [ring R] [star_ring R] :
has_distrib_neg ↥(unitary R)
Equations