# Documentation

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 #

• When R is a StarModule R₂ R, then selfAdjoint R has a natural Module (selfAdjoint R₂) (selfAdjoint R) structure. However, doing this literally would be undesirable since in the main case of interest (R₂ = ℂ) we want Module ℝ (selfAdjoint R) and not Module (selfAdjoint ℂ) (selfAdjoint R). We solve this issue by adding the typeclass [TrivialStar R₃], of which ℝ is an instance (registered in Data/Real/Basic), and then add a [Module R₃ (selfAdjoint R)] instance whenever we have [Module R₃ R] [TrivialStar R₃]. (Another approach would have been to define [StarInvariantScalars R₃ R] to express the fact that star (x • v) = x • star v, but this typeclass would have the disadvantage of taking two type arguments.)

## TODO #

• Define IsSkewAdjoint to match IsSelfAdjoint.
• Define fun z x => z * x * star z (i.e. conjugation by z) as a monoid action of R on R (similar to the existing ConjAct for groups), and then state the fact that selfAdjoint R is invariant under it.
def IsSelfAdjoint {R : Type u_1} [Star R] (x : R) :

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

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) [] :
star x * x = x * star x
theorem IsSelfAdjoint.all {R : Type u_1} [Star 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 : ) :
star x = x
theorem isSelfAdjoint_iff {R : Type u_1} [Star R] {x : R} :
star x = x
@[simp]
theorem IsSelfAdjoint.star_iff {R : Type u_1} [] {x : R} :
@[simp]
theorem IsSelfAdjoint.star_mul_self {R : Type u_1} [Mul R] [] (x : R) :
@[simp]
theorem IsSelfAdjoint.mul_star_self {R : Type u_1} [Mul R] [] (x : R) :
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 : ) (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] [StarHomClass F R S] [] (f : F) (x : R) :
theorem isSelfAdjoint_zero (R : Type u_1) [] [] :
theorem IsSelfAdjoint.add {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
@[deprecated]
theorem IsSelfAdjoint.bit0 {R : Type u_1} [] [] {x : R} (hx : ) :
theorem IsSelfAdjoint.neg {R : Type u_1} [] [] {x : R} (hx : ) :
theorem IsSelfAdjoint.sub {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
theorem isSelfAdjoint_add_star_self {R : Type u_1} [] [] (x : R) :
theorem isSelfAdjoint_star_add_self {R : Type u_1} [] [] (x : R) :
theorem IsSelfAdjoint.conjugate {R : Type u_1} [] [] {x : R} (hx : ) (z : R) :
theorem IsSelfAdjoint.conjugate' {R : Type u_1} [] [] {x : R} (hx : ) (z : R) :
theorem IsSelfAdjoint.isStarNormal {R : Type u_1} [] [] {x : R} (hx : ) :
theorem isSelfAdjoint_one (R : Type u_1) [] [] :
theorem IsSelfAdjoint.pow {R : Type u_1} [] [] {x : R} (hx : ) (n : ) :
@[deprecated]
theorem IsSelfAdjoint.bit1 {R : Type u_1} [] [] {x : R} (hx : ) :
@[simp]
theorem isSelfAdjoint_natCast {R : Type u_1} [] [] (n : ) :
theorem IsSelfAdjoint.mul {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
@[simp]
theorem isSelfAdjoint_intCast {R : Type u_1} [Ring R] [] (z : ) :
theorem IsSelfAdjoint.inv {R : Type u_1} [] [] {x : R} (hx : ) :
theorem IsSelfAdjoint.zpow {R : Type u_1} [] [] {x : R} (hx : ) (n : ) :
theorem isSelfAdjoint_ratCast {R : Type u_1} [] [] (x : ) :
theorem IsSelfAdjoint.div {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
theorem IsSelfAdjoint.smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [SMul R A] [] {r : R} (hr : ) {x : A} (hx : ) :
def selfAdjoint (R : Type u_1) [] [] :

Instances For
def skewAdjoint (R : Type u_1) [] [] :

Instances For
theorem selfAdjoint.mem_iff {R : Type u_1} [] [] {x : R} :
x star x = x
@[simp]
theorem selfAdjoint.star_val_eq {R : Type u_1} [] [] {x : { x // x }} :
star x = x
instance selfAdjoint.isStarNormal {R : Type u_1} [] [] (x : { x // x }) :
@[simp]
theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [] :
1 = 1
@[simp]
theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [] (x : { x // x }) (n : ) :
↑(x ^ n) = x ^ n
@[simp]
theorem selfAdjoint.val_mul {R : Type u_1} [] (x : { x // x }) (y : { x // x }) :
↑(x * y) = x * y
@[simp]
theorem selfAdjoint.val_inv {R : Type u_1} [] [] (x : { x // x }) :
x⁻¹ = (x)⁻¹
@[simp]
theorem selfAdjoint.val_div {R : Type u_1} [] [] (x : { x // x }) (y : { x // x }) :
↑(x / y) = x / y
@[simp]
theorem selfAdjoint.val_zpow {R : Type u_1} [] [] (x : { x // x }) (z : ) :
↑(x ^ z) = x ^ z
@[simp]
theorem selfAdjoint.val_ratCast {R : Type u_1} [] [] (x : ) :
x = x
instance selfAdjoint.instQSMul {R : Type u_1} [] [] :
SMul { x // x }
@[simp]
theorem selfAdjoint.val_rat_smul {R : Type u_1} [] [] (x : { x // x }) (a : ) :
↑(a x) = a x
@[simp]
theorem selfAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [SMul R A] [] (r : R) (x : { x // x }) :
↑(r x) = r x
theorem skewAdjoint.mem_iff {R : Type u_1} [] [] {x : R} :
x star x = -x
@[simp]
theorem skewAdjoint.star_val_eq {R : Type u_1} [] [] {x : { x // x }} :
star x = -x
@[deprecated]
theorem skewAdjoint.bit0_mem {R : Type u_1} [] [] {x : R} (hx : x ) :
theorem skewAdjoint.conjugate {R : Type u_1} [Ring R] [] {x : R} (hx : x ) (z : R) :
z * x * star z
theorem skewAdjoint.conjugate' {R : Type u_1} [Ring R] [] {x : R} (hx : x ) (z : R) :
star z * x * z
theorem skewAdjoint.isStarNormal_of_mem {R : Type u_1} [Ring R] [] {x : R} (hx : x ) :
theorem skewAdjoint.smul_mem {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] (r : R) {x : A} (h : x ) :
r x
@[simp]
theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] (r : R) (x : { x // x }) :
↑(r x) = r x
theorem IsSelfAdjoint.smul_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [] [Module R A] [] [] [] {r : R} (hr : r ) {a : A} (ha : ) :
r a