# 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.

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 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.commute_iff {R : Type u_3} [Mul R] [] {x : R} {y : R} (hx : ) (hy : ) :

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 : ) (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] [FunLike F R S] [StarHomClass F R S] [] (f : F) (x : R) :
@[simp]
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 : ) :
@[simp]
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 : ) :
@[simp]
theorem isSelfAdjoint_ofNat {R : Type u_1} [] [] (n : ) [] :
theorem IsSelfAdjoint.mul {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
theorem IsSelfAdjoint.conj_eq {α : Type u_3} [] [] {a : α} (ha : ) :
() a = a
@[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) [] [] :

Equations
• = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : R | }, add_mem' := }, zero_mem' := }, neg_mem' := }
Instances For
def skewAdjoint (R : Type u_1) [] [] :

Equations
• = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : R | star x = -x}, add_mem' := }, zero_mem' := }, neg_mem' := }
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 : ()} :
star x = x
Equations
instance selfAdjoint.isStarNormal {R : Type u_1} [] [] (x : ()) :
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [] :
1 = 1
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [] (x : ()) (n : ) :
(x ^ n) = x ^ n
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_mul {R : Type u_1} [] (x : ()) (y : ()) :
(x * y) = x * y
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_inv {R : Type u_1} [] [] (x : ()) :
x⁻¹ = (x)⁻¹
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_div {R : Type u_1} [] [] (x : ()) (y : ()) :
(x / y) = x / y
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem selfAdjoint.val_zpow {R : Type u_1} [] [] (x : ()) (z : ) :
(x ^ z) = x ^ z
instance selfAdjoint.instRatCast {R : Type u_1} [] [] :
RatCast ()
Equations
• selfAdjoint.instRatCast = { ratCast := fun (q : ) => { val := q, property := } }
@[simp]
theorem selfAdjoint.val_ratCast {R : Type u_1} [] [] (q : ) :
q = q
instance selfAdjoint.instSMulRat {R : Type u_1} [] [] :
SMul ()
Equations
• selfAdjoint.instSMulRat = { smul := fun (a : ) (x : ()) => { val := a x, property := } }
@[simp]
theorem selfAdjoint.val_qsmul {R : Type u_1} [] [] (q : ) (x : ()) :
(q x) = q x
instance selfAdjoint.instField {R : Type u_1} [] [] :
Field ()
Equations
• selfAdjoint.instField = Function.Injective.field (fun (a : ()) => a)
Equations
• selfAdjoint.instSMulSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupSelfAdjoint = { smul := fun (r : R) (x : ()) => { val := r x, property := } }
@[simp]
theorem selfAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [SMul R A] [] (r : R) (x : ()) :
(r x) = r x
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
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 : ()} :
star x = -x
Equations
@[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
Equations
@[simp]
theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] (r : R) (x : ()) :
(r x) = r x
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
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

theorem isSelfAdjoint_smul_of_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [] [Module R A] [] [] [] {r : R} (hr : r ) {a : A} (ha : a ) :

instance isStarNormal_zero {R : Type u_1} [] [] :
Equations
• =
instance isStarNormal_one {R : Type u_1} [] [] :
Equations
• =
instance IsStarNormal.star {R : Type u_1} [Mul R] [] {x : R} [] :
Equations
• =
instance IsStarNormal.neg {R : Type u_1} [Ring R] [] {x : R} [] :
Equations
• =
instance 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 : ] :
Equations
• =
instance TrivialStar.isStarNormal {R : Type u_1} [Mul R] [] [] {x : R} :
Equations
• =
instance CommMonoid.isStarNormal {R : Type u_1} [] [] {x : R} :
Equations
• =
theorem Pi.isSelfAdjoint {ι : Type u_3} {α : ιType u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :
∀ (i : ι), IsSelfAdjoint (f i)
theorem IsSelfAdjoint.apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :
∀ (i : ι), IsSelfAdjoint (f i)

Alias of the forward direction of Pi.isSelfAdjoint.