Documentation

Mathlib.Algebra.Star.SelfAdjoint

Self-adjoint, skew-adjoint and normal elements of a star additive group #

This file defines selfAdjoint R (resp. skewAdjoint R), where R is a star additive group, as the additive subgroup containing the elements that satisfy star x = x (resp. star x = -x). This includes, for instance, (skew-)Hermitian operators on Hilbert spaces.

We also define IsStarNormal R, a Prop that states that an element x satisfies star x * x = x * star x.

Implementation notes #

TODO #

def IsSelfAdjoint {R : Type u_1} [Star R] (x : R) :

An element is self-adjoint if it is equal to its star.

Equations
Instances For
    class IsStarNormal {R : Type u_1} [Mul R] [Star R] (x : R) :
    • star_comm_self : Commute (star x) x

      A normal element of a star monoid commutes with its adjoint.

    An element of a star monoid is normal if it commutes with its adjoint.

    Instances
      theorem star_comm_self' {R : Type u_1} [Mul R] [Star R] (x : R) [IsStarNormal x] :
      star x * x = x * star x
      theorem IsSelfAdjoint.all {R : Type u_1} [Star R] [TrivialStar R] (r : R) :

      All elements are self-adjoint when star is trivial.

      theorem IsSelfAdjoint.star_eq {R : Type u_1} [Star R] {x : R} (hx : IsSelfAdjoint x) :
      star x = x
      theorem isSelfAdjoint_iff {R : Type u_1} [Star R] {x : R} :
      @[simp]
      theorem IsSelfAdjoint.star_mul_self {R : Type u_1} [Mul R] [StarMul R] (x : R) :
      @[simp]
      theorem IsSelfAdjoint.mul_star_self {R : Type u_1} [Mul R] [StarMul R] (x : R) :
      theorem IsSelfAdjoint.commute_iff {R : Type u_3} [Mul R] [StarMul R] {x : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

      Self-adjoint elements commute if and only if their product is self-adjoint.

      theorem IsSelfAdjoint.starHom_apply {F : Type u_3} {R : Type u_4} {S : Type u_5} [Star R] [Star S] [StarHomClass F R S] {x : R} (hx : IsSelfAdjoint x) (f : F) :
      IsSelfAdjoint (f x)

      Functions in a StarHomClass preserve self-adjoint elements.

      theorem isSelfAdjoint_starHom_apply {F : Type u_3} {R : Type u_4} {S : Type u_5} [Star R] [Star S] [StarHomClass F R S] [TrivialStar R] (f : F) (x : R) :
      IsSelfAdjoint (f x)
      theorem IsSelfAdjoint.add {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      @[deprecated]
      theorem IsSelfAdjoint.bit0 {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x : R} (hx : IsSelfAdjoint x) :
      theorem IsSelfAdjoint.neg {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} (hx : IsSelfAdjoint x) :
      theorem IsSelfAdjoint.sub {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      theorem IsSelfAdjoint.conjugate {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) :
      theorem IsSelfAdjoint.conjugate' {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) :
      theorem IsSelfAdjoint.pow {R : Type u_1} [Monoid R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ) :
      @[deprecated]
      theorem IsSelfAdjoint.bit1 {R : Type u_1} [Semiring R] [StarRing R] {x : R} (hx : IsSelfAdjoint x) :
      @[simp]
      theorem isSelfAdjoint_natCast {R : Type u_1} [Semiring R] [StarRing R] (n : ) :
      theorem IsSelfAdjoint.mul {R : Type u_1} [CommSemigroup R] [StarMul R] {x : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      @[simp]
      theorem isSelfAdjoint_intCast {R : Type u_1} [Ring R] [StarRing R] (z : ) :
      theorem IsSelfAdjoint.zpow {R : Type u_1} [DivisionSemiring R] [StarRing R] {x : R} (hx : IsSelfAdjoint x) (n : ) :
      theorem IsSelfAdjoint.div {R : Type u_1} [Semifield R] [StarRing R] {x : R} {y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      theorem IsSelfAdjoint.smul {R : Type u_1} {A : Type u_2} [Star R] [AddMonoid A] [StarAddMonoid A] [SMul R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) {x : A} (hx : IsSelfAdjoint x) :

      The self-adjoint elements of a star additive group, as an additive subgroup.

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

        The skew-adjoint elements of a star additive group, as an additive subgroup.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem selfAdjoint.mem_iff {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} :
          @[simp]
          theorem selfAdjoint.star_val_eq {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : { x // x selfAdjoint R }} :
          star x = x
          Equations
          • selfAdjoint.instInhabitedSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { default := 0 }
          @[simp]
          theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [StarRing R] :
          1 = 1
          @[simp]
          theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [StarRing R] (x : { x // x selfAdjoint R }) (n : ) :
          ↑(x ^ n) = x ^ n
          @[simp]
          theorem selfAdjoint.val_mul {R : Type u_1} [NonUnitalCommRing R] [StarRing R] (x : { x // x selfAdjoint R }) (y : { x // x selfAdjoint R }) :
          ↑(x * y) = x * y
          @[simp]
          theorem selfAdjoint.val_inv {R : Type u_1} [Field R] [StarRing R] (x : { x // x selfAdjoint R }) :
          x⁻¹ = (x)⁻¹
          @[simp]
          theorem selfAdjoint.val_div {R : Type u_1} [Field R] [StarRing R] (x : { x // x selfAdjoint R }) (y : { x // x selfAdjoint R }) :
          ↑(x / y) = x / y
          @[simp]
          theorem selfAdjoint.val_zpow {R : Type u_1} [Field R] [StarRing R] (x : { x // x selfAdjoint R }) (z : ) :
          ↑(x ^ z) = x ^ z
          @[simp]
          theorem selfAdjoint.val_ratCast {R : Type u_1} [Field R] [StarRing R] (x : ) :
          x = x
          instance selfAdjoint.instQSMul {R : Type u_1} [Field R] [StarRing R] :
          SMul { x // x selfAdjoint R }
          Equations
          • selfAdjoint.instQSMul = { smul := fun a x => { val := a x, property := (_ : a x selfAdjoint R) } }
          @[simp]
          theorem selfAdjoint.val_rat_smul {R : Type u_1} [Field R] [StarRing R] (x : { x // x selfAdjoint R }) (a : ) :
          ↑(a x) = a x
          Equations
          • selfAdjoint.instSMulSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { smul := fun r x => { val := r x, property := (_ : IsSelfAdjoint (r x)) } }
          @[simp]
          theorem selfAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [SMul R A] [StarModule R A] (r : R) (x : { x // x selfAdjoint A }) :
          ↑(r x) = r x
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem skewAdjoint.star_val_eq {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : { x // x skewAdjoint R }} :
          star x = -x
          Equations
          • skewAdjoint.instInhabitedSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint = { default := 0 }
          @[deprecated]
          theorem skewAdjoint.bit0_mem {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : R} (hx : x skewAdjoint R) :
          theorem skewAdjoint.conjugate {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x skewAdjoint R) (z : R) :
          theorem skewAdjoint.conjugate' {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x skewAdjoint R) (z : R) :
          theorem skewAdjoint.isStarNormal_of_mem {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x skewAdjoint R) :
          theorem skewAdjoint.smul_mem {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A} (h : x skewAdjoint A) :
          Equations
          • skewAdjoint.instSMulSubtypeMemAddSubgroupToAddGroupInstMembershipInstSetLikeAddSubgroupSkewAdjoint = { smul := fun r x => { val := r x, property := (_ : r x skewAdjoint A) } }
          @[simp]
          theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) (x : { x // x skewAdjoint A }) :
          ↑(r x) = r x
          theorem IsSelfAdjoint.smul_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A] [StarModule R A] {r : R} (hr : r skewAdjoint R) {a : A} (ha : IsSelfAdjoint a) :

          Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a skew-adjoint element.

          theorem isSelfAdjoint_smul_of_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A] [StarModule R A] {r : R} (hr : r skewAdjoint R) {a : A} (ha : a skewAdjoint A) :

          Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.