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 isStarNormal_iff {R : Type u_1} [Mul R] [Star R] (x : R) :
      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 y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

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

      theorem IsSelfAdjoint.map {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.

      @[deprecated IsSelfAdjoint.map]
      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) :

      Alias of IsSelfAdjoint.map.


      Functions in a StarHomClass preserve self-adjoint elements.

      theorem isSelfAdjoint_map {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) :
      @[deprecated isSelfAdjoint_map]
      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) :

      Alias of isSelfAdjoint_map.

      theorem IsSelfAdjoint.add {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      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 y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
      @[simp]
      @[simp]
      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.conjugate_self {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) {z : R} (hz : IsSelfAdjoint z) :
      IsSelfAdjoint (z * x * z)
      @[simp]
      theorem IsSelfAdjoint.pow {R : Type u_1} [Monoid R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ) :
      @[simp]
      theorem IsSelfAdjoint.natCast {R : Type u_1} [Semiring R] [StarRing R] (n : ) :
      @[simp]
      theorem IsSelfAdjoint.ofNat {R : Type u_1} [Semiring R] [StarRing R] (n : ) [n.AtLeastTwo] :
      theorem IsSelfAdjoint.mul {R : Type u_1} [CommSemigroup R] [StarMul R] {x 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.inv {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) :
      theorem IsSelfAdjoint.zpow {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ) :
      theorem IsSelfAdjoint.zpow₀ {R : Type u_1} [GroupWithZero R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ) :
      @[simp]
      theorem IsSelfAdjoint.ratCast {R : Type u_1} [DivisionRing R] [StarRing R] (x : ) :
      theorem IsSelfAdjoint.div {R : Type u_1} [Semifield R] [StarRing R] {x 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) :
      theorem IsSelfAdjoint.smul_iff {R : Type u_1} {A : Type u_2} [Monoid R] [StarMul R] [AddMonoid A] [StarAddMonoid A] [MulAction R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) (hu : IsUnit r) {x : A} :

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

      Equations
      Instances For

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

        Equations
        • skewAdjoint R = { 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.instInhabitedSubtypeMemAddSubgroup = { default := 0 }
          Equations
          • selfAdjoint.instOneSubtypeMemAddSubgroup = { one := 1, }
          @[simp]
          theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [StarRing R] :
          1 = 1
          Equations
          • selfAdjoint.instNatCastSubtypeMemAddSubgroup = { natCast := fun (n : ) => n, }
          Equations
          • selfAdjoint.instIntCastSubtypeMemAddSubgroup = { intCast := fun (n : ) => n, }
          Equations
          • selfAdjoint.instPowSubtypeMemAddSubgroupNat = { pow := fun (x : (selfAdjoint R)) (n : ) => x ^ n, }
          @[simp]
          theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [StarRing R] (x : (selfAdjoint R)) (n : ) :
          (x ^ n) = x ^ n
          Equations
          • selfAdjoint.instMulSubtypeMemAddSubgroup = { mul := fun (x y : (selfAdjoint R)) => x * y, }
          @[simp]
          theorem selfAdjoint.val_mul {R : Type u_1} [NonUnitalCommRing R] [StarRing R] (x y : (selfAdjoint R)) :
          (x * y) = x * y
          Equations
          Equations
          • selfAdjoint.instInvSubtypeMemAddSubgroup = { inv := fun (x : (selfAdjoint R)) => (↑x)⁻¹, }
          @[simp]
          theorem selfAdjoint.val_inv {R : Type u_1} [Field R] [StarRing R] (x : (selfAdjoint R)) :
          x⁻¹ = (↑x)⁻¹
          Equations
          • selfAdjoint.instDivSubtypeMemAddSubgroup = { div := fun (x y : (selfAdjoint R)) => x / y, }
          @[simp]
          theorem selfAdjoint.val_div {R : Type u_1} [Field R] [StarRing R] (x y : (selfAdjoint R)) :
          (x / y) = x / y
          Equations
          • selfAdjoint.instPowSubtypeMemAddSubgroupInt = { pow := fun (x : (selfAdjoint R)) (z : ) => x ^ z, }
          @[simp]
          theorem selfAdjoint.val_zpow {R : Type u_1} [Field R] [StarRing R] (x : (selfAdjoint R)) (z : ) :
          (x ^ z) = x ^ z
          Equations
          • selfAdjoint.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q, }
          instance selfAdjoint.instRatCast {R : Type u_1} [Field R] [StarRing R] :
          Equations
          • selfAdjoint.instRatCast = { ratCast := fun (q : ) => q, }
          @[simp]
          theorem selfAdjoint.val_nnratCast {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) :
          q = q
          @[simp]
          theorem selfAdjoint.val_ratCast {R : Type u_1} [Field R] [StarRing R] (q : ) :
          q = q
          Equations
          instance selfAdjoint.instSMulRat {R : Type u_1} [Field R] [StarRing R] :
          Equations
          • selfAdjoint.instSMulRat = { smul := fun (a : ) (x : (selfAdjoint R)) => a x, }
          @[simp]
          theorem selfAdjoint.val_nnqsmul {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) (x : (selfAdjoint R)) :
          (q x) = q x
          @[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.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : (selfAdjoint A)) => 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 : (selfAdjoint A)) :
          (r x) = r x
          Equations
          Equations
          Equations
          @[simp]
          theorem skewAdjoint.star_val_eq {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : (skewAdjoint R)} :
          star x = -x
          Equations
          • skewAdjoint.instInhabitedSubtypeMemAddSubgroup = { default := 0 }
          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.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : (skewAdjoint A)) => r x, }
          @[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
          Equations
          Equations
          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.

          theorem IsStarNormal.star {R : Type u_1} [Mul R] [StarMul R] {x : R} [IsStarNormal x] :
          theorem IsStarNormal.neg {R : Type u_1} [Ring R] [StarAddMonoid R] {x : R} [IsStarNormal x] :
          theorem 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] :
          theorem TrivialStar.isStarNormal {R : Type u_1} [Mul R] [StarMul R] [TrivialStar R] {x : R} :
          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.