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

ink

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

One or more equations did not get rendered due to their size.

source

ink

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

source

ink

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

source

ink

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

source

ink

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

star U ∈ unitary R

source

ink

@[simp]

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

star U ∈ unitary R ↔ U ∈ unitary R

source

ink

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

Star { x // x ∈ unitary R }

Equations

unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { star := fun U => { val := star ↑U, property := (_ : star ↑U ∈ unitary R) } }

source

ink

@[simp]

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

↑(star U) = star ↑U

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

Group { x // x ∈ unitary R }

Equations

One or more equations did not get rendered due to their size.

source

ink

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

InvolutiveStar { x // x ∈ unitary R }

Equations

unitary.instInvolutiveStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = InvolutiveStar.mk (_ : ∀ (x : { x // x ∈ unitary R }), star (star x) = x)

source

ink

instance unitary.instStarSemigroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryToSemigroupToSemigroupToMulMemClassInstSubmonoidClassSubmonoidInstSetLikeSubmonoid {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] :

StarSemigroup { x // x ∈ unitary R }

Equations

One or more equations did not get rendered due to their size.

source

ink

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

Inhabited { x // x ∈ unitary R }

Equations

unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { default := 1 }

source

ink

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

star U = U⁻¹

source

ink

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

star = Inv.inv

source

ink

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

source

ink

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

source

ink

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.

source

ink

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

Function.Injective ↑unitary.toUnits

source

ink

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

CommGroup { x // x ∈ unitary R }

Equations

One or more equations did not get rendered due to their size.

source

ink

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

source

ink

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

source

ink

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

↑U⁻¹ = (↑U)⁻¹

source

ink

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₂

source

ink