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
star x * x = x * star x.
Implementation notes #
StarModule R₂ R, then
selfAdjoint Rhas 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.)
Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a skew-adjoint element.
Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.