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) [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.

Equations

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

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

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

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

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

@[simp]

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

instance unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] : Star { x // x ∈ unitary R }

Equations

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

@[simp]

theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : { x // x ∈ unitary R }} : ↑(star U) = star ↑U

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

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

@[simp]

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

@[simp]

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

instance unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] : Group { x // x ∈ unitary R }

Equations

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

instance unitary.instInvolutiveStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] : InvolutiveStar { x // x ∈ unitary R }

Equations

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

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

Equations

• unitary.instStarMulSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryMul = StarMul.mk (_ : ∀ (x y : { x // x ∈ unitary R }), star (x * y) = star y * star x)

instance unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] : Inhabited { x // x ∈ unitary R }

Equations

• unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { default := 1 }

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

theorem unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] : star = Inv.inv

@[simp]

theorem unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : { x // x ∈ unitary R }) : ↑(↑unitary.toUnits x)⁻¹ = ↑x⁻¹

@[simp]

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

def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul 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} [Monoid R] [StarMul R] : Function.Injective ↑unitary.toUnits

instance unitary.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [CommMonoid R] [StarMul R] : CommGroup { x // x ∈ unitary R }

Equations

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

theorem unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} : U ∈ unitary R ↔ star U * U = 1

theorem unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} : U ∈ unitary R ↔ U * star U = 1

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

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₂

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

instance unitary.instNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRing {R : Type u_1} [Ring R] [StarRing R] : Neg { x // x ∈ unitary R }

Equations

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

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

instance unitary.instHasDistribNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingMul {R : Type u_1} [Ring R] [StarRing R] : HasDistribNeg { x // x ∈ unitary R }

Equations

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