mathlibdocumentation

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 λ 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.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_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.conjugate {R : Type u_1} [star_ring R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.conjugate' {R : Type u_1} [star_ring R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.is_star_normal {R : Type u_1} [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint_one (R : Type u_1) [ring R] [star_ring R] :
theorem is_self_adjoint.bit1 {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.pow {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.mul {R : Type u_1} [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.inv {R : Type u_1} [field R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.div {R : Type u_1} [field R] [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.zpow {R : Type u_1} [field R] [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.smul {R : Type u_1} {A : Type u_2} [has_star R] [add_group A] [ A] [ A] (r : R) {x : A} (hx : is_self_adjoint x) :

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

Equations
Instances for ↥skew_adjoint
theorem self_adjoint.mem_iff {R : Type u_1} [add_group R] {x : R} :
@[simp, norm_cast]
@[protected, instance]
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
@[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
theorem self_adjoint.rat_cast_mem {R : Type u_1} [field R] [star_ring R] (x : ) :
@[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]
@[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
@[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} :