# 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
theorem isStarNormal_iff {R : Type u_1} [Mul R] [Star R] (x : R) :
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 IsStarNormal.star_comm_self {R : Type u_1} [Mul R] [Star R] {x : R} [self : ] :

A normal element of a star monoid commutes with its adjoint.

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 : ) :
theorem IsSelfAdjoint.neg {R : Type u_1} [] [] {x : R} (hx : ) :
theorem IsSelfAdjoint.sub {R : Type u_1} [] [] {x : R} {y : R} (hx : ) (hy : ) :
@[simp]
theorem IsSelfAdjoint.add_star_self {R : Type u_1} [] [] (x : R) :
@[simp]
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 : ) :
@[simp]
theorem IsSelfAdjoint.natCast {R : Type u_1} [] [] (n : ) :
@[simp]
theorem IsSelfAdjoint.ofNat {R : Type u_1} [] [] (n : ) [n.AtLeastTwo] :
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 : ) :
@[simp]
theorem IsSelfAdjoint.nnratCast {R : Type u_1} [] [] (q : ℚ≥0) :
@[simp]
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
• = { carrier := {x : R | }, add_mem' := , zero_mem' := , neg_mem' := }
Instances For
def skewAdjoint (R : Type u_1) [] [] :

Equations
• = { 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
• =
One ()
Equations
@[simp]
theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [] :
1 = 1
Equations
• =
Equations
• selfAdjoint.instNatCastSubtypeMemAddSubgroup = { natCast := fun (n : ) => n, }
Equations
• selfAdjoint.instIntCastSubtypeMemAddSubgroup = { intCast := fun (n : ) => n, }
Equations
• selfAdjoint.instPowSubtypeMemAddSubgroupNat = { pow := fun (x : ()) (n : ) => x ^ n, }
@[simp]
theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [] (x : ()) (n : ) :
(x ^ n) = x ^ n
Equations
• selfAdjoint.instMulSubtypeMemAddSubgroup = { mul := fun (x y : ()) => x * y, }
@[simp]
theorem selfAdjoint.val_mul {R : Type u_1} [] (x : ()) (y : ()) :
(x * y) = x * y
Equations
Inv ()
Equations
• selfAdjoint.instInvSubtypeMemAddSubgroup = { inv := fun (x : ()) => (x)⁻¹, }
@[simp]
theorem selfAdjoint.val_inv {R : Type u_1} [] [] (x : ()) :
x⁻¹ = (x)⁻¹
Div ()
Equations
• selfAdjoint.instDivSubtypeMemAddSubgroup = { div := fun (x y : ()) => x / y, }
@[simp]
theorem selfAdjoint.val_div {R : Type u_1} [] [] (x : ()) (y : ()) :
(x / y) = x / y
Equations
• selfAdjoint.instPowSubtypeMemAddSubgroupInt = { pow := fun (x : ()) (z : ) => x ^ z, }
@[simp]
theorem selfAdjoint.val_zpow {R : Type u_1} [] [] (x : ()) (z : ) :
(x ^ z) = x ^ z
instance selfAdjoint.instNNRatCast {R : Type u_1} [] [] :
NNRatCast ()
Equations
• selfAdjoint.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q, }
instance selfAdjoint.instRatCast {R : Type u_1} [] [] :
RatCast ()
Equations
• selfAdjoint.instRatCast = { ratCast := fun (q : ) => q, }
@[simp]
theorem selfAdjoint.val_nnratCast {R : Type u_1} [] [] (q : ℚ≥0) :
q = q
@[simp]
theorem selfAdjoint.val_ratCast {R : Type u_1} [] [] (q : ) :
q = q
instance selfAdjoint.instSMulNNRat {R : Type u_1} [] [] :
Equations
• selfAdjoint.instSMulNNRat = { smul := fun (a : ℚ≥0) (x : ()) => a x, }
instance selfAdjoint.instSMulRat {R : Type u_1} [] [] :
SMul ()
Equations
• selfAdjoint.instSMulRat = { smul := fun (a : ) (x : ()) => a x, }
@[simp]
theorem selfAdjoint.val_nnqsmul {R : Type u_1} [] [] (q : ℚ≥0) (x : ()) :
(q x) = q x
@[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)
instance selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [SMul R A] [] :
SMul R ()
Equations
• selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : ()) => r x, }
@[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
instance selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] :
MulAction R ()
Equations
instance selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] :
Equations
instance selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [Module R A] [] :
Module R ()
Equations
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
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 ) :
instance skewAdjoint.instIsStarNormalValMemSetCoeAddSubgroup {R : Type u_1} [Ring R] [] (x : ()) :
Equations
• =
theorem skewAdjoint.smul_mem {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] (r : R) {x : A} (h : x ) :
r x
instance skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] :
SMul R ()
Equations
• skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule = { smul := fun (r : R) (x : ()) => r x, }
@[simp]
theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] (r : R) (x : ()) :
(r x) = r x
instance skewAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [] [] :
Equations
instance skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [] [] [] [] [Module R A] [] :
Module R ()
Equations
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 100]
instance TrivialStar.isStarNormal {R : Type u_1} [Mul R] [] [] {x : R} :
Equations
• =
@[instance 100]
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.