Documentation

Mathlib.Algebra.Star.Unitary

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.

Equations
  • One or more equations did not get rendered due to their size.
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 ↥(unitary R)
    Equations
    • unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { star := fun (U : ↥(unitary R)) => { val := star ↑U, property := (_ : star ↑U ∈ unitary R) } }
    source
    @[simp]
    theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :
    ↑(star U) = star ↑U
    source
    theorem unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
    star ↑U * ↑U = 1
    source
    theorem unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
    ↑U * ↑(star U) = 1
    source
    @[simp]
    theorem unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
    star U * U = 1
    source
    @[simp]
    theorem unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :
    U * star U = 1
    source
    instance unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    Group ↥(unitary R)
    Equations
    source
    instance unitary.instInvolutiveStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    InvolutiveStar ↥(unitary R)
    Equations
    source
    instance unitary.instStarMulSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryMul {R : Type u_1} [Monoid R] [StarMul R] :
    StarMul ↥(unitary R)
    Equations
    • unitary.instStarMulSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryMul = StarMul.mk (_ : ∀ (x y : ↥(unitary R)), star (x * y) = star y * star x)
    source
    instance unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    Inhabited ↥(unitary R)
    Equations
    • unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { default := 1 }
    source
    theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(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 : ↥(unitary R)) :
    ↑(unitary.toUnits x)⁻¹ = ↑x⁻¹
    source
    @[simp]
    theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
    ↑(unitary.toUnits x) = ↑x
    source
    def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
    ↥(unitary R) →* Rˣ

    The unitary elements embed into the units.

    Equations
    • One or more equations did not get rendered due to their size.
    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 ↥(unitary R)
      Equations
      • One or more equations did not get rendered due to their size.
      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 : ↥(unitary R)) :
      ↑U⁻¹ = (↑U)⁻¹
      source
      theorem unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ : ↥(unitary R)) (U₂ : ↥(unitary R)) :
      ↑(U₁ / U₂) = ↑U₁ / ↑U₂
      source
      theorem unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) (z : ℤ) :
      ↑(U ^ z) = ↑U ^ z
      source
      instance unitary.instNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRing {R : Type u_1} [Ring R] [StarRing R] :
      Neg ↥(unitary R)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : ↥(unitary R)) :
      ↑(-U) = -↑U
      source
      instance unitary.instHasDistribNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarMulToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingMul {R : Type u_1} [Ring R] [StarRing R] :
      HasDistribNeg ↥(unitary R)
      Equations
      • One or more equations did not get rendered due to their size.