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

source

def unitary (R : Type u_1) [Monoid R] [StarMul 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.

Instances For

source

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

source

@[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

source

@[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

source

theorem unitary.star_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :

star U ∈ unitary R

source

@[simp]

theorem unitary.star_mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :

star U ∈ unitary R ↔ U ∈ unitary R

source

instance unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :

Star { x // x ∈ unitary R }

source

@[simp]

theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : { x // x ∈ unitary R }} :

↑(star U) = star ↑U

source

theorem unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : { x // x ∈ unitary R }) :

star ↑U * ↑U = 1

source

theorem unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : { x // x ∈ unitary R }) :

↑U * ↑(star U) = 1

source

@[simp]

theorem unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : { x // x ∈ unitary R }) :

star U * U = 1

source

@[simp]

theorem unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : { x // x ∈ unitary R }) :

U * star U = 1

source

instance unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :

Group { x // x ∈ unitary R }

source

instance unitary.instInvolutiveStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :

InvolutiveStar { x // x ∈ unitary R }

source

instance unitary.instStarMulSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryMul {R : Type u_1} [Monoid R] [StarMul R] :

StarMul { x // x ∈ unitary R }

source

instance unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :

Inhabited { x // x ∈ unitary R }

source

theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : { x // x ∈ unitary R }) :

star U = U⁻¹

source

theorem unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] :

star = Inv.inv

source

@[simp]

theorem unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : { x // x ∈ unitary R }) :

↑(↑unitary.toUnits x)⁻¹ = ↑x⁻¹

source

@[simp]

theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : { x // x ∈ unitary R }) :

↑(↑unitary.toUnits x) = ↑x

source

def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :

{ x // x ∈ unitary R } →* Rˣ

The unitary elements embed into the units.

Instances For

source

theorem unitary.to_units_injective {R : Type u_1} [Monoid R] [StarMul R] :

Function.Injective ↑unitary.toUnits

source

instance unitary.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [CommMonoid R] [StarMul R] :

CommGroup { x // x ∈ unitary R }

source

theorem unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :

U ∈ unitary R ↔ star U * U = 1

source

theorem unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :

U ∈ unitary R ↔ U * star U = 1

source

theorem unitary.coe_inv {R : Type u_1} [GroupWithZero R] [StarMul R] (U : { x // x ∈ unitary R }) :

↑U⁻¹ = (↑U)⁻¹

source

theorem unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ : { x // x ∈ unitary R }) (U₂ : { x // x ∈ unitary R }) :

↑(U₁ / U₂) = ↑U₁ / ↑U₂

source

theorem unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : { x // x ∈ unitary R }) (z : ℤ) :

↑(U ^ z) = ↑U ^ z

source

instance unitary.instNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRing {R : Type u_1} [Ring R] [StarRing R] :

Neg { x // x ∈ unitary R }

source

theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : { x // x ∈ unitary R }) :

↑(-U) = -↑U

source

instance unitary.instHasDistribNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingMul {R : Type u_1} [Ring R] [StarRing R] :

HasDistribNeg { x // x ∈ unitary R }