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.

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
    @[implicit_reducible]
    instance Unitary.instStarSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    Star ↥(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
    @[implicit_reducible]
    instance Unitary.instGroupSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    Group ↥(unitary R)
    source
    @[implicit_reducible]
    instance Unitary.instInvolutiveStarSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    InvolutiveStar ↥(unitary R)
    source
    @[implicit_reducible]
    instance Unitary.instStarMulSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    StarMul ↥(unitary R)
    source
    @[implicit_reducible]
    instance Unitary.instInhabitedSubtypeMemSubmonoidUnitary {R : Type u_1} [Monoid R] [StarMul R] :
    Inhabited ↥(unitary R)
    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
    def Unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :
    ↥(unitary R) →* Rˣ

    The unitary elements embed into the units.

    Instances For
      source
      @[simp]
      theorem Unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
      ↑(toUnits x) = ↑x
      source
      @[simp]
      theorem Unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :
      ↑(toUnits x)⁻¹ = ↑x⁻¹
      source
      theorem Unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] :
      Function.Injective ⇑toUnits
      source
      theorem IsUnit.mem_unitary_iff_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
      u ∈ unitary R ↔ star u * u = 1
      source
      theorem IsUnit.mem_unitary_iff_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
      u ∈ unitary R ↔ u * star u = 1
      source
      theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :
      star u * u = 1 → u ∈ unitary R

      Alias of the reverse direction of IsUnit.mem_unitary_iff_star_mul_self.

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

      Alias of the reverse direction of IsUnit.mem_unitary_iff_mul_star_self.

      source
      theorem Unitary.isUnit_coe {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :
      IsUnit ↑U
      source
      theorem Unitary.mul_left_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
      x * ↑U = y * ↑U ↔ x = y

      For unitary U in a star-monoid R, x * U = y * U if and only if x = y for all x and y in R.

      source
      theorem Unitary.mul_right_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :
      ↑U * x = ↑U * y ↔ x = y

      For unitary U in a star-monoid R, U * x = U * y if and only if x = y for all x and y in R.

      source
      theorem Unitary.mul_inv_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
      a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b
      source
      theorem Unitary.inv_mul_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :
      a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b
      source
      theorem Units.unitary_eq {R : Type u_1} [Monoid R] [StarMul R] :
      unitary Rˣ = Submonoid.comap (coeHom R) (unitary R)
      source
      theorem Units.mul_inv_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :
      ↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

      In a star monoid, the product a * b⁻¹ of units is unitary if star a * a = star b * b.

      source
      theorem Units.inv_mul_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :
      ↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b

      In a star monoid, the product a⁻¹ * b of units is unitary if a * star a = b * star b.

      source
      instance Unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :
      IsStarNormal u
      source
      instance Unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :
      IsStarNormal ↑u
      source
      theorem isStarNormal_of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u ∈ unitary R) :
      IsStarNormal u
      source
      theorem Unitary.inv_mem {G : Type u_2} [Group G] [StarMul G] {g : G} (hg : g ∈ unitary G) :
      g⁻¹ ∈ unitary G
      source
      def unitarySubgroup (G : Type u_2) [Group G] [StarMul G] :
      Subgroup G

      unitary as a Subgroup of a group.

      Note the group structure on this type is not defeq to the one on unitary. This situation naturally arises when considering the unitary elements as a subgroup of the group of units of a star monoid.

      Instances For
        source
        @[simp]
        theorem unitarySubgroup_toSubmonoid {G : Type u_2} [Group G] [StarMul G] :
        (unitarySubgroup G).toSubmonoid = unitary G
        source
        @[simp]
        theorem mem_unitarySubgroup_iff {G : Type u_2} [Group G] [StarMul G] {g : G} :
        g ∈ unitarySubgroup G ↔ g ∈ unitary G
        source
        theorem Unitary.inv_mem_iff {G : Type u_2} [Group G] [StarMul G] {g : G} :
        g⁻¹ ∈ unitary G ↔ g ∈ unitary G
        source
        theorem Unitary.smul_mem_of_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] {r : R} {a : A} (hr : r ∈ unitary R) (ha : a ∈ unitary A) :
        r • a ∈ unitary A
        source
        theorem Unitary.smul_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) {a : A} (ha : a ∈ unitary A) :
        r • a ∈ unitary A
        source
        @[implicit_reducible]
        instance Unitary.instSMulSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
        SMul ↥(unitary R) ↥(unitary A)
        source
        @[simp]
        theorem Unitary.coe_smul {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) (a : ↥(unitary A)) :
        ↑(r • a) = r • ↑a
        source
        @[implicit_reducible]
        instance Unitary.instMulActionSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
        MulAction ↥(unitary R) ↥(unitary A)
        source
        instance Unitary.instStarModuleSubtypeMemSubmonoidUnitary {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :
        StarModule ↥(unitary R) ↥(unitary A)
        source
        instance Unitary.instSMulCommClassSubtypeMemSubmonoidUnitary {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R A] [MulAction S A] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [SMulCommClass R S A] :
        SMulCommClass ↥(unitary R) ↥(unitary S) ↥(unitary A)
        source
        instance Unitary.instIsScalarTowerSubtypeMemSubmonoidUnitary {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R S] [MulAction R A] [MulAction S A] [StarModule R S] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [IsScalarTower R S S] [SMulCommClass R S S] [IsScalarTower R S A] :
        IsScalarTower ↥(unitary R) ↥(unitary S) ↥(unitary A)
        source
        theorem Unitary.map_mem {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {F : Type u_5} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r ∈ unitary R) :
        f r ∈ unitary S
        source
        def Unitary.map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
        ↥(unitary R) →⋆* ↥(unitary S)

        The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of the underlying star monoids.

        Instances For
          source
          @[simp]
          theorem Unitary.map_coe {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (a✝ : ↥(unitary R)) :
          (map f) a✝ = Subtype.map ⇑f ⋯ a✝
          source
          @[simp]
          theorem Unitary.coe_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
          ↑((map f) x) = f ↑x
          source
          @[simp]
          theorem Unitary.coe_map_star {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :
          ↑((map f) (star x)) = f (star ↑x)
          source
          @[simp]
          theorem Unitary.map_id {R : Type u_2} [Monoid R] [StarMul R] :
          map (StarMonoidHom.id R) = StarMonoidHom.id ↥(unitary R)
          source
          theorem Unitary.map_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (g : S →⋆* T) (f : R →⋆* S) :
          map (g.comp f) = (map g).comp (map f)
          source
          @[simp]
          theorem Unitary.map_injective {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {f : R →⋆* S} (hf : Function.Injective ⇑f) :
          Function.Injective ⇑(map f)
          source
          theorem Unitary.toUnits_comp_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :
          toUnits.comp (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits
          source
          def Unitary.mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
          ↥(unitary R) ≃⋆* ↥(unitary S)

          The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.

          Instances For
            source
            @[simp]
            theorem Unitary.mapEquiv_symm_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary S)) :
            (mapEquiv f).symm a = (map f.symm.toStarMonoidHom) a
            source
            @[simp]
            theorem Unitary.mapEquiv_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary R)) :
            (mapEquiv f) a = (map f.toStarMonoidHom) a
            source
            @[simp]
            theorem Unitary.mapEquiv_refl {R : Type u_2} [Monoid R] [StarMul R] :
            mapEquiv (StarMulEquiv.refl R) = StarMulEquiv.refl ↥(unitary R)
            source
            @[simp]
            theorem Unitary.mapEquiv_symm {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
            mapEquiv f.symm = (mapEquiv f).symm
            source
            @[simp]
            theorem Unitary.mapEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (f : R ≃⋆* S) (g : S ≃⋆* T) :
            mapEquiv (f.trans g) = (mapEquiv f).trans (mapEquiv g)
            source
            @[simp]
            theorem Unitary.toMonoidHom_mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :
            (mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom
            source
            def unitarySubgroupUnitsEquiv {M : Type u_5} [Monoid M] [StarMul M] :
            ↥(unitarySubgroup Mˣ) ≃* ↥(unitary M)

            The unitary subgroup of the units is equivalent to the unitary elements of the monoid.

            Instances For
              source
              @[simp]
              theorem val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitary M)) :
              ↑(↑(unitarySubgroupUnitsEquiv.symm x))⁻¹ = star ↑x
              source
              @[simp]
              theorem val_unitarySubgroupUnitsEquiv_symm_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitary M)) :
              ↑↑(unitarySubgroupUnitsEquiv.symm x) = ↑x
              source
              @[simp]
              theorem unitarySubgroupUnitsEquiv_apply_coe {M : Type u_5} [Monoid M] [StarMul M] (x : ↥(unitarySubgroup Mˣ)) :
              ↑(unitarySubgroupUnitsEquiv x) = ↑↑x
              source
              @[implicit_reducible]
              instance Unitary.instCommGroupSubtypeMemSubmonoidUnitary {R : Type u_1} [CommMonoid R] [StarMul R] :
              CommGroup ↥(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 : ↥(unitary R)) :
              ↑U⁻¹ = (↑U)⁻¹
              source
              theorem Unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ 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
              @[implicit_reducible]
              instance Unitary.instNegSubtypeMemSubmonoidUnitary {R : Type u_1} [Ring R] [StarRing R] :
              Neg ↥(unitary R)
              source
              theorem Unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : ↥(unitary R)) :
              ↑(-U) = -↑U
              source
              @[implicit_reducible]
              instance Unitary.instHasDistribNegSubtypeMemSubmonoidUnitary {R : Type u_1} [Ring R] [StarRing R] :
              HasDistribNeg ↥(unitary R)
              source
              @[simp]
              theorem Unitary.spectrum_star_right_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
              spectrum R (↑U * a * star ↑U) = spectrum R a

              Unitary conjugation preserves the spectrum, star on right.

              source
              @[simp]
              theorem Unitary.spectrum_star_left_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {U : ↥(unitary A)} :
              spectrum R (star ↑U * a * ↑U) = spectrum R a

              Unitary conjugation preserves the spectrum, star on left.

              source
              theorem IsStarProjection.two_mul_sub_one_mem_unitary {R : Type u_2} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :
              2 * p - 1 ∈ unitary R