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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines self_adjoint R (resp. skew_adjoint 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 is_star_normal R, a Prop that states that an element x satisfies star x * x = x * star x.

Implementation notes #

• When R is a star_module R₂ R, then self_adjoint R has a natural module (self_adjoint R₂) (self_adjoint R) structure. However, doing this literally would be undesirable since in the main case of interest (R₂ = ℂ) we want module ℝ (self_adjoint R) and not module (self_adjoint ℂ) (self_adjoint R). We solve this issue by adding the typeclass [has_trivial_star R₃], of which ℝ is an instance (registered in data/real/basic), and then add a [module R₃ (self_adjoint R)] instance whenever we have [module R₃ R] [has_trivial_star R₃]. (Another approach would have been to define [star_invariant_scalars 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 is_skew_adjoint to match is_self_adjoint.
• Define λ z x, z * x * star z (i.e. conjugation by z) as a monoid action of R on R (similar to the existing conj_act for groups), and then state the fact that self_adjoint R is invariant under it.