# mathlib3documentation

algebra.star.self_adjoint

# 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.
def is_self_adjoint {R : Type u_1} [has_star R] (x : R) :
Prop

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

Equations
@[class]
structure is_star_normal {R : Type u_1} [has_mul R] [has_star R] (x : R) :
Prop
• star_comm_self : x

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

Instances of this typeclass
theorem star_comm_self' {R : Type u_1} [has_mul R] [has_star R] (x : R)  :
=
theorem is_self_adjoint.all {R : Type u_1} [has_star R] (r : R) :

All elements are self-adjoint when star is trivial.

theorem is_self_adjoint.star_eq {R : Type u_1} [has_star R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint_iff {R : Type u_1} [has_star R] {x : R} :
@[simp]
theorem is_self_adjoint.star_iff {R : Type u_1} {x : R} :
@[simp]
theorem is_self_adjoint.star_mul_self {R : Type u_1} [semigroup R] (x : R) :
@[simp]
theorem is_self_adjoint.mul_star_self {R : Type u_1} [semigroup R] (x : R) :
theorem is_self_adjoint.star_hom_apply {F : Type u_1} {R : Type u_2} {S : Type u_3} [has_star R] [has_star S] [ S] {x : R} (hx : is_self_adjoint x) (f : F) :

Functions in a star_hom_class preserve self-adjoint elements.

theorem is_self_adjoint_zero (R : Type u_1) [add_monoid R]  :
theorem is_self_adjoint.add {R : Type u_1} [add_monoid R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.bit0 {R : Type u_1} [add_monoid R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.neg {R : Type u_1} [add_group R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.sub {R : Type u_1} [add_group R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint_add_star_self {R : Type u_1} (x : R) :
theorem is_self_adjoint_star_add_self {R : Type u_1} (x : R) :
theorem is_self_adjoint.conjugate {R : Type u_1} [semigroup R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.conjugate' {R : Type u_1} [semigroup R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.is_star_normal {R : Type u_1} [semigroup R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint_one (R : Type u_1) [monoid R]  :
theorem is_self_adjoint.pow {R : Type u_1} [monoid R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.bit1 {R : Type u_1} [semiring R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
@[simp]
theorem is_self_adjoint_nat_cast {R : Type u_1} [semiring R] [star_ring R] (n : ) :
theorem is_self_adjoint.mul {R : Type u_1} {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
@[simp]
theorem is_self_adjoint_int_cast {R : Type u_1} [ring R] [star_ring R] (z : ) :
theorem is_self_adjoint.inv {R : Type u_1} [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.zpow {R : Type u_1} [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint_rat_cast {R : Type u_1} [star_ring R] (x : ) :
theorem is_self_adjoint.div {R : Type u_1} [semifield R] [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.smul {R : Type u_1} {A : Type u_2} [has_star R] [add_monoid A] [ A] [ A] {r : R} (hr : is_self_adjoint r) {x : A} (hx : is_self_adjoint x) :
def self_adjoint (R : Type u_1) [add_group R]  :

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

Equations
Instances for ↥self_adjoint
def skew_adjoint (R : Type u_1)  :

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

Equations
Instances for ↥skew_adjoint
theorem self_adjoint.mem_iff {R : Type u_1} [add_group R] {x : R} :
@[simp, norm_cast]
theorem self_adjoint.star_coe_eq {R : Type u_1} [add_group R] {x : (self_adjoint R)} :
@[protected, instance]
def self_adjoint.inhabited {R : Type u_1} [add_group R]  :
Equations
@[protected, instance]
def self_adjoint.has_one {R : Type u_1} [ring R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_one {R : Type u_1} [ring R] [star_ring R] :
1 = 1
@[protected, instance]
def self_adjoint.nontrivial {R : Type u_1} [ring R] [star_ring R] [nontrivial R] :
@[protected, instance]
def self_adjoint.has_nat_cast {R : Type u_1} [ring R] [star_ring R] :
Equations
@[protected, instance]
def self_adjoint.has_int_cast {R : Type u_1} [ring R] [star_ring R] :
Equations
@[protected, instance]
def self_adjoint.nat.has_pow {R : Type u_1} [ring R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_pow {R : Type u_1} [ring R] [star_ring R] (x : (self_adjoint R)) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def self_adjoint.has_mul {R : Type u_1} [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_mul {R : Type u_1} [star_ring R] (x y : (self_adjoint R)) :
(x * y) = x * y
@[protected, instance]
def self_adjoint.comm_ring {R : Type u_1} [comm_ring R] [star_ring R] :
Equations
• self_adjoint.comm_ring = self_adjoint.comm_ring._proof_1 self_adjoint.comm_ring._proof_2 self_adjoint.comm_ring._proof_3 self_adjoint.comm_ring._proof_4 self_adjoint.comm_ring._proof_5 self_adjoint.comm_ring._proof_6 self_adjoint.comm_ring._proof_7 self_adjoint.comm_ring._proof_8 self_adjoint.comm_ring._proof_9 self_adjoint.comm_ring._proof_10 self_adjoint.comm_ring._proof_11 self_adjoint.comm_ring._proof_12
@[protected, instance]
def self_adjoint.has_inv {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_inv {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) :
@[protected, instance]
def self_adjoint.has_div {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_div {R : Type u_1} [field R] [star_ring R] (x y : (self_adjoint R)) :
(x / y) = x / y
@[protected, instance]
def self_adjoint.int.has_pow {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_zpow {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) (z : ) :
(x ^ z) = x ^ z
@[protected, instance]
def self_adjoint.has_rat_cast {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_rat_cast {R : Type u_1} [field R] [star_ring R] (x : ) :
@[protected, instance]
def self_adjoint.has_qsmul {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_rat_smul {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) (a : ) :
(a x) = a x
@[protected, instance]
def self_adjoint.field {R : Type u_1} [field R] [star_ring R] :
Equations
@[protected, instance]
def self_adjoint.has_smul {R : Type u_1} {A : Type u_2} [has_star R] [add_group A] [ A] [ A] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_smul {R : Type u_1} {A : Type u_2} [has_star R] [add_group A] [ A] [ A] (r : R) (x : (self_adjoint A)) :
(r x) = r x
@[protected, instance]
def self_adjoint.mul_action {R : Type u_1} {A : Type u_2} [has_star R] [add_group A] [monoid R] [ A] [ A] :
Equations
@[protected, instance]
def self_adjoint.distrib_mul_action {R : Type u_1} {A : Type u_2} [has_star R] [add_group A] [monoid R] [ A] [ A] :
Equations
@[protected, instance]
def self_adjoint.module {R : Type u_1} {A : Type u_2} [has_star R] [semiring R] [ A] [ A] :
Equations
theorem skew_adjoint.mem_iff {R : Type u_1} {x : R} :
@[simp, norm_cast]
theorem skew_adjoint.star_coe_eq {R : Type u_1} {x : (skew_adjoint R)} :
@[protected, instance]
def skew_adjoint.inhabited {R : Type u_1}  :
Equations
theorem skew_adjoint.bit0_mem {R : Type u_1} {x : R} (hx : x ) :
theorem skew_adjoint.conjugate {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x ) (z : R) :
z * x *
theorem skew_adjoint.conjugate' {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x ) (z : R) :
* z
theorem skew_adjoint.is_star_normal_of_mem {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x ) :
@[protected, instance]
def skew_adjoint.is_star_normal {R : Type u_1} [ring R] [star_ring R] (x : (skew_adjoint R)) :
theorem skew_adjoint.smul_mem {R : Type u_1} {A : Type u_2} [has_star R] [monoid R] [ A] [ A] (r : R) {x : A} (h : x ) :
r x
@[protected, instance]
def skew_adjoint.has_smul {R : Type u_1} {A : Type u_2} [has_star R] [monoid R] [ A] [ A] :
Equations
@[simp, norm_cast]
theorem skew_adjoint.coe_smul {R : Type u_1} {A : Type u_2} [has_star R] [monoid R] [ A] [ A] (r : R) (x : (skew_adjoint A)) :
(r x) = r x
@[protected, instance]
def skew_adjoint.distrib_mul_action {R : Type u_1} {A : Type u_2} [has_star R] [monoid R] [ A] [ A] :
Equations
@[protected, instance]
def skew_adjoint.module {R : Type u_1} {A : Type u_2} [has_star R] [semiring R] [ A] [ A] :
Equations
theorem is_self_adjoint.smul_mem_skew_adjoint {R : Type u_1} {A : Type u_2} [ring R] [ A] [ A] {r : R} (hr : r ) {a : A} (ha : is_self_adjoint a) :
r a

Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a skew-adjoint element.

theorem is_self_adjoint_smul_of_mem_skew_adjoint {R : Type u_1} {A : Type u_2} [ring R] [ A] [ A] {r : R} (hr : r ) {a : A} (ha : a ) :

Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.

@[protected, instance]
def is_star_normal_zero {R : Type u_1} [semiring R] [star_ring R] :
@[protected, instance]
def is_star_normal_one {R : Type u_1} [monoid R]  :
@[protected, instance]
def is_star_normal_star_self {R : Type u_1} [monoid R] {x : R}  :
@[protected, instance]
def has_trivial_star.is_star_normal {R : Type u_1} [monoid R] {x : R} :
@[protected, instance]
def comm_monoid.is_star_normal {R : Type u_1} [comm_monoid R] {x : R} :