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

• unitary R = { carrier := {U : R | star U * U = 1 ∧ U * star U = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

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.instStarSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] : Star { x : R // x ∈ unitary R }

Equations

• unitary.instStarSubtypeMemSubmonoid = { star := fun (U : { x : R // x ∈ unitary R }) => ⟨star ↑U, ⋯⟩ }

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

Equations

• unitary.instGroupSubtypeMemSubmonoid = Group.mk ⋯

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

Equations

• unitary.instInvolutiveStarSubtypeMemSubmonoid = InvolutiveStar.mk ⋯

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

Equations

• unitary.instStarMulSubtypeMemSubmonoid = StarMul.mk ⋯

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

Equations

• unitary.instInhabitedSubtypeMemSubmonoid = { default := 1 }

theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : { x : R // 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_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : { x : R // x ∈ unitary R }) : ↑(unitary.toUnits x) = ↑x

@[simp]

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

def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] : { x : R // x ∈ unitary R } →* Rˣ

The unitary elements embed into the units.

Equations

• unitary.toUnits = { toFun := fun (x : { x : R // x ∈ unitary R }) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

theorem unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] : Function.Injective ⇑unitary.toUnits

theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) (h_mul : star u * u = 1) : u ∈ unitary R

theorem IsUnit.mem_unitary_of_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) (h_mul : u * star u = 1) : u ∈ unitary R

instance unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : { x : R // x ∈ unitary R }) : IsStarNormal u

Equations

• ⋯ = ⋯

instance unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : { x : R // x ∈ unitary R }) : IsStarNormal ↑u

Equations

• ⋯ = ⋯

theorem isStarNormal_of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u ∈ unitary R) : IsStarNormal u

theorem unitary.map_mem {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r ∈ unitary R) : f r ∈ unitary S

@[simp]

theorem unitary.map_apply {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) : ∀ (a : { x : R // x ∈ unitary R }), (unitary.map f) a = Subtype.map ⇑f ⋯ a

def unitary.map {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) : { x : R // x ∈ unitary R } →* { x : S // x ∈ unitary S }

The group homomorphism between unitary subgroups of star monoids induced by a star homomorphism

Equations

• unitary.map f = { toFun := Subtype.map ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem unitary.toUnits_comp_map {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) : unitary.toUnits.comp (unitary.map f) = (Units.map ↑f).comp unitary.toUnits

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

Equations

• unitary.instCommGroupSubtypeMemSubmonoid = CommGroup.mk ⋯

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 : R // x ∈ unitary R }) : ↑U⁻¹ = (↑U)⁻¹

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

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

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

Equations

• unitary.instNegSubtypeMemSubmonoid = { neg := fun (U : { x : R // x ∈ unitary R }) => ⟨-↑U, ⋯⟩ }

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

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

Equations

• unitary.instHasDistribNegSubtypeMemSubmonoid = Function.Injective.hasDistribNeg (fun (a : { x : R // x ∈ unitary R }) => ↑a) ⋯ ⋯ ⋯

@[simp]

theorem unitary.spectrum.unitary_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : { x : A // x ∈ unitary A }} : spectrum R (↑u * a * star ↑u) = spectrum R a

Unitary conjugation preserves the spectrum, star on left.

@[simp]

theorem unitary.spectrum.unitary_conjugate' {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : { x : A // x ∈ unitary A }} : spectrum R (star ↑u * a * ↑u) = spectrum R a

Unitary conjugation preserves the spectrum, star on right.