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) :

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

    • star_comm_self : Commute (star x) x

      A normal element of a star monoid 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] [FunLike F R S] [StarHomClass F R S] {x : R} (hx : IsSelfAdjoint x) (f : F) :

      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] [FunLike F R S] [StarHomClass F R S] [TrivialStar R] (f : F) (x : R) :
      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) :
      @[simp]
      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) :
      theorem IsSelfAdjoint.conj_eq {α : Type u_3} [CommSemiring α] [StarRing α] {a : α} (ha : IsSelfAdjoint a) :
      (starRingEnd α) a = a
      @[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
      • selfAdjoint R = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : R | IsSelfAdjoint x}, add_mem' := }, zero_mem' := }, neg_mem' := }
      Instances For

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

        Equations
        • skewAdjoint R = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : R | star x = -x}, add_mem' := }, zero_mem' := }, neg_mem' := }
        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 : (selfAdjoint R)} :
          star x = x
          Equations
          • selfAdjoint.instInhabitedSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { default := 0 }
          instance selfAdjoint.isStarNormal {R : Type u_1} [NonUnitalRing R] [StarRing R] (x : (selfAdjoint R)) :
          Equations
          • =
          @[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 : (selfAdjoint R)) (n : ) :
          (x ^ n) = x ^ n
          @[simp]
          theorem selfAdjoint.val_mul {R : Type u_1} [NonUnitalCommRing R] [StarRing R] (x : (selfAdjoint R)) (y : (selfAdjoint R)) :
          (x * y) = x * y
          @[simp]
          theorem selfAdjoint.val_inv {R : Type u_1} [Field R] [StarRing R] (x : (selfAdjoint R)) :
          x⁻¹ = (x)⁻¹
          @[simp]
          theorem selfAdjoint.val_div {R : Type u_1} [Field R] [StarRing R] (x : (selfAdjoint R)) (y : (selfAdjoint R)) :
          (x / y) = x / y
          @[simp]
          theorem selfAdjoint.val_zpow {R : Type u_1} [Field R] [StarRing R] (x : (selfAdjoint R)) (z : ) :
          (x ^ z) = x ^ z
          instance selfAdjoint.instRatCast {R : Type u_1} [Field R] [StarRing R] :
          Equations
          • selfAdjoint.instRatCast = { ratCast := fun (q : ) => { val := q, property := } }
          @[simp]
          theorem selfAdjoint.val_ratCast {R : Type u_1} [Field R] [StarRing R] (q : ) :
          q = q
          instance selfAdjoint.instSMulRat {R : Type u_1} [Field R] [StarRing R] :
          Equations
          • selfAdjoint.instSMulRat = { smul := fun (a : ) (x : (selfAdjoint R)) => { val := a x, property := } }
          @[simp]
          theorem selfAdjoint.val_qsmul {R : Type u_1} [Field R] [StarRing R] (q : ) (x : (selfAdjoint R)) :
          (q x) = q x
          instance selfAdjoint.instField {R : Type u_1} [Field R] [StarRing R] :
          Equations
          Equations
          • selfAdjoint.instSMulSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { smul := fun (r : R) (x : (selfAdjoint A)) => { val := r x, property := } }
          @[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 : (selfAdjoint A)) :
          (r x) = r x
          Equations
          @[simp]
          theorem skewAdjoint.star_val_eq {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {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 : R) (x : (skewAdjoint A)) => { val := r x, property := } }
          @[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 : (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.

          instance isStarNormal_zero {R : Type u_1} [Semiring R] [StarRing R] :
          Equations
          • =
          instance isStarNormal_one {R : Type u_1} [MulOneClass R] [StarMul R] :
          Equations
          • =
          instance IsStarNormal.star {R : Type u_1} [Mul R] [StarMul R] {x : R} [IsStarNormal x] :
          Equations
          • =
          instance IsStarNormal.neg {R : Type u_1} [Ring R] [StarAddMonoid R] {x : R} [IsStarNormal x] :
          Equations
          • =
          instance IsStarNormal.map {F : Type u_3} {R : Type u_4} {S : Type u_5} [Mul R] [Star R] [Mul S] [Star S] [FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] :
          Equations
          • =
          instance TrivialStar.isStarNormal {R : Type u_1} [Mul R] [StarMul R] [TrivialStar R] {x : R} :
          Equations
          • =
          instance CommMonoid.isStarNormal {R : Type u_1} [CommMonoid R] [StarMul R] {x : R} :
          Equations
          • =
          theorem Pi.isSelfAdjoint {ι : Type u_3} {α : ιType u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :
          IsSelfAdjoint f ∀ (i : ι), IsSelfAdjoint (f i)
          theorem IsSelfAdjoint.apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :
          IsSelfAdjoint f∀ (i : ι), IsSelfAdjoint (f i)

          Alias of the forward direction of Pi.isSelfAdjoint.