Self-adjoint, skew-adjoint and normal elements of a star additive group #
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 astar_module R₂ R
, thenself_adjoint R
has a naturalmodule (self_adjoint R₂) (self_adjoint R)
structure. However, doing this literally would be undesirable since in the main case of interest (R₂ = ℂ
) we wantmodule ℝ (self_adjoint R)
and notmodule (self_adjoint ℂ) (self_adjoint R)
. We solve this issue by adding the typeclass[has_trivial_star R₃]
, of whichℝ
is an instance (registered indata/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 thatstar (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 byz
) as a monoid action ofR
onR
(similar to the existingconj_act
for groups), and then state the fact thatself_adjoint R
is invariant under it.
An element is self-adjoint if it is equal to its star.
Equations
- is_self_adjoint x = (has_star.star x = x)
@[class]
- star_comm_self : commute (has_star.star x) x
An element of a star monoid is normal if it commutes with its adjoint.
theorem
star_comm_self'
{R : Type u_1}
[has_mul R]
[has_star R]
(x : R)
[is_star_normal x] :
has_star.star x * x = x * has_star.star x
theorem
is_self_adjoint.star_eq
{R : Type u_1}
[has_star R]
{x : R}
(hx : is_self_adjoint x) :
has_star.star x = x
theorem
is_self_adjoint_iff
{R : Type u_1}
[has_star R]
{x : R} :
is_self_adjoint x ↔ has_star.star x = x
@[simp]
theorem
is_self_adjoint.star_mul_self
{R : Type u_1}
[semigroup R]
[star_semigroup R]
(x : R) :
is_self_adjoint (has_star.star x * x)
@[simp]
theorem
is_self_adjoint.mul_star_self
{R : Type u_1}
[semigroup R]
[star_semigroup R]
(x : R) :
is_self_adjoint (x * has_star.star x)
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]
[star_hom_class F R S]
{x : R}
(hx : is_self_adjoint x)
(f : F) :
is_self_adjoint (⇑f x)
Functions in a star_hom_class
preserve self-adjoint elements.
theorem
is_self_adjoint.add
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x y : R}
(hx : is_self_adjoint x)
(hy : is_self_adjoint y) :
is_self_adjoint (x + y)
theorem
is_self_adjoint.neg
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x : R}
(hx : is_self_adjoint x) :
is_self_adjoint (-x)
theorem
is_self_adjoint.sub
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x y : R}
(hx : is_self_adjoint x)
(hy : is_self_adjoint y) :
is_self_adjoint (x - y)
theorem
is_self_adjoint.bit0
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x : R}
(hx : is_self_adjoint x) :
is_self_adjoint (bit0 x)
theorem
is_self_adjoint.conjugate
{R : Type u_1}
[non_unital_semiring R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x)
(z : R) :
is_self_adjoint (z * x * has_star.star z)
theorem
is_self_adjoint.conjugate'
{R : Type u_1}
[non_unital_semiring R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x)
(z : R) :
is_self_adjoint (has_star.star z * x * z)
theorem
is_self_adjoint.is_star_normal
{R : Type u_1}
[non_unital_semiring R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x) :
theorem
is_self_adjoint.bit1
{R : Type u_1}
[ring R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x) :
is_self_adjoint (bit1 x)
theorem
is_self_adjoint.pow
{R : Type u_1}
[ring R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x)
(n : ℕ) :
is_self_adjoint (x ^ n)
theorem
is_self_adjoint.mul
{R : Type u_1}
[non_unital_comm_ring R]
[star_ring R]
{x y : R}
(hx : is_self_adjoint x)
(hy : is_self_adjoint y) :
is_self_adjoint (x * 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) :
is_self_adjoint (x / y)
theorem
is_self_adjoint.zpow
{R : Type u_1}
[field R]
[star_ring R]
{x : R}
(hx : is_self_adjoint x)
(n : ℤ) :
is_self_adjoint (x ^ n)
theorem
is_self_adjoint.smul
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_group A]
[star_add_monoid A]
[has_smul R A]
[star_module R A]
(r : R)
{x : A}
(hx : is_self_adjoint x) :
is_self_adjoint (r • x)
The self-adjoint elements of a star additive group, as an additive subgroup.
Equations
- self_adjoint R = {carrier := {x : R | is_self_adjoint x}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥self_adjoint
- self_adjoint.inhabited
- self_adjoint.has_one
- self_adjoint.nontrivial
- self_adjoint.has_nat_cast
- self_adjoint.has_int_cast
- self_adjoint.nat.has_pow
- self_adjoint.has_mul
- self_adjoint.comm_ring
- self_adjoint.has_inv
- self_adjoint.has_div
- self_adjoint.int.has_pow
- self_adjoint.has_rat_cast
- self_adjoint.has_qsmul
- self_adjoint.field
- self_adjoint.has_smul
- self_adjoint.mul_action
- self_adjoint.distrib_mul_action
- self_adjoint.module
The skew-adjoint elements of a star additive group, as an additive subgroup.
Equations
- skew_adjoint R = {carrier := {x : R | has_star.star x = -x}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥skew_adjoint
theorem
self_adjoint.mem_iff
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x : R} :
x ∈ self_adjoint R ↔ has_star.star x = x
@[simp, norm_cast]
theorem
self_adjoint.star_coe_eq
{R : Type u_1}
[add_group R]
[star_add_monoid R]
{x : ↥(self_adjoint R)} :
has_star.star ↑x = ↑x
@[protected, instance]
Equations
- self_adjoint.inhabited = {default := 0}
@[protected, instance]
Equations
- self_adjoint.has_one = {one := ⟨1, _⟩}
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- self_adjoint.nat.has_pow = {pow := λ (x : ↥(self_adjoint R)) (n : ℕ), ⟨↑x ^ n, _⟩}
@[protected, instance]
def
self_adjoint.has_mul
{R : Type u_1}
[non_unital_comm_ring R]
[star_ring R] :
has_mul ↥(self_adjoint R)
Equations
- self_adjoint.has_mul = {mul := λ (x y : ↥(self_adjoint R)), ⟨↑x * ↑y, _⟩}
@[simp, norm_cast]
theorem
self_adjoint.coe_mul
{R : Type u_1}
[non_unital_comm_ring R]
[star_ring R]
(x y : ↥(self_adjoint R)) :
@[protected, instance]
Equations
- self_adjoint.comm_ring = function.injective.comm_ring coe 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]
Equations
- self_adjoint.has_inv = {inv := λ (x : ↥(self_adjoint R)), ⟨(x.val)⁻¹, _⟩}
@[protected, instance]
Equations
- self_adjoint.has_div = {div := λ (x y : ↥(self_adjoint R)), ⟨↑x / ↑y, _⟩}
@[protected, instance]
Equations
- self_adjoint.int.has_pow = {pow := λ (x : ↥(self_adjoint R)) (z : ℤ), ⟨↑x ^ z, _⟩}
@[protected, instance]
@[protected, instance]
Equations
- self_adjoint.has_qsmul = {smul := λ (a : ℚ) (x : ↥(self_adjoint R)), ⟨a • ↑x, _⟩}
@[protected, instance]
Equations
- self_adjoint.field = function.injective.field coe self_adjoint.field._proof_1 self_adjoint.field._proof_2 self_adjoint.field._proof_3 self_adjoint.field._proof_4 self_adjoint.field._proof_5 self_adjoint.field._proof_6 self_adjoint.field._proof_7 self_adjoint.coe_inv self_adjoint.coe_div self_adjoint.field._proof_8 self_adjoint.field._proof_9 self_adjoint.coe_rat_smul self_adjoint.field._proof_10 self_adjoint.coe_zpow self_adjoint.field._proof_11 self_adjoint.field._proof_12 self_adjoint.coe_rat_cast
@[protected, instance]
def
self_adjoint.has_smul
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_group A]
[star_add_monoid A]
[has_smul R A]
[star_module R A] :
has_smul R ↥(self_adjoint A)
Equations
- self_adjoint.has_smul = {smul := λ (r : R) (x : ↥(self_adjoint A)), ⟨r • ↑x, _⟩}
@[simp, norm_cast]
theorem
self_adjoint.coe_smul
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_group A]
[star_add_monoid A]
[has_smul R A]
[star_module R A]
(r : R)
(x : ↥(self_adjoint A)) :
@[protected, instance]
def
self_adjoint.mul_action
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_group A]
[star_add_monoid A]
[monoid R]
[mul_action R A]
[star_module R A] :
mul_action R ↥(self_adjoint A)
Equations
- self_adjoint.mul_action = function.injective.mul_action coe self_adjoint.mul_action._proof_1 self_adjoint.mul_action._proof_2
@[protected, instance]
def
self_adjoint.distrib_mul_action
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_group A]
[star_add_monoid A]
[monoid R]
[distrib_mul_action R A]
[star_module R A] :
Equations
- self_adjoint.distrib_mul_action = function.injective.distrib_mul_action (self_adjoint A).subtype self_adjoint.distrib_mul_action._proof_1 self_adjoint.distrib_mul_action._proof_2
@[protected, instance]
def
self_adjoint.module
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[semiring R]
[module R A]
[star_module R A] :
module R ↥(self_adjoint A)
Equations
- self_adjoint.module = function.injective.module R (self_adjoint A).subtype self_adjoint.module._proof_1 self_adjoint.module._proof_2
theorem
skew_adjoint.mem_iff
{R : Type u_1}
[add_comm_group R]
[star_add_monoid R]
{x : R} :
x ∈ skew_adjoint R ↔ has_star.star x = -x
@[simp, norm_cast]
theorem
skew_adjoint.star_coe_eq
{R : Type u_1}
[add_comm_group R]
[star_add_monoid R]
{x : ↥(skew_adjoint R)} :
has_star.star ↑x = -↑x
@[protected, instance]
Equations
- skew_adjoint.inhabited = {default := 0}
theorem
skew_adjoint.bit0_mem
{R : Type u_1}
[add_comm_group R]
[star_add_monoid R]
{x : R}
(hx : x ∈ skew_adjoint R) :
bit0 x ∈ skew_adjoint R
theorem
skew_adjoint.conjugate
{R : Type u_1}
[ring R]
[star_ring R]
{x : R}
(hx : x ∈ skew_adjoint R)
(z : R) :
z * x * has_star.star z ∈ skew_adjoint R
theorem
skew_adjoint.conjugate'
{R : Type u_1}
[ring R]
[star_ring R]
{x : R}
(hx : x ∈ skew_adjoint R)
(z : R) :
has_star.star z * x * z ∈ skew_adjoint R
theorem
skew_adjoint.is_star_normal_of_mem
{R : Type u_1}
[ring R]
[star_ring R]
{x : R}
(hx : x ∈ skew_adjoint R) :
@[protected, instance]
theorem
skew_adjoint.smul_mem
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[monoid R]
[distrib_mul_action R A]
[star_module R A]
(r : R)
{x : A}
(h : x ∈ skew_adjoint A) :
r • x ∈ skew_adjoint A
@[protected, instance]
def
skew_adjoint.has_smul
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[monoid R]
[distrib_mul_action R A]
[star_module R A] :
has_smul R ↥(skew_adjoint A)
Equations
- skew_adjoint.has_smul = {smul := λ (r : R) (x : ↥(skew_adjoint A)), ⟨r • ↑x, _⟩}
@[simp, norm_cast]
theorem
skew_adjoint.coe_smul
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[monoid R]
[distrib_mul_action R A]
[star_module R A]
(r : R)
(x : ↥(skew_adjoint A)) :
@[protected, instance]
def
skew_adjoint.distrib_mul_action
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[monoid R]
[distrib_mul_action R A]
[star_module R A] :
Equations
- skew_adjoint.distrib_mul_action = function.injective.distrib_mul_action (skew_adjoint A).subtype skew_adjoint.distrib_mul_action._proof_1 skew_adjoint.coe_smul
@[protected, instance]
def
skew_adjoint.module
{R : Type u_1}
{A : Type u_2}
[has_star R]
[has_trivial_star R]
[add_comm_group A]
[star_add_monoid A]
[semiring R]
[module R A]
[star_module R A] :
module R ↥(skew_adjoint A)
Equations
- skew_adjoint.module = function.injective.module R (skew_adjoint A).subtype skew_adjoint.module._proof_1 skew_adjoint.module._proof_2
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
is_star_normal_star_self
{R : Type u_1}
[monoid R]
[star_semigroup R]
{x : R}
[is_star_normal x] :
@[protected, instance]
def
has_trivial_star.is_star_normal
{R : Type u_1}
[monoid R]
[star_semigroup R]
[has_trivial_star R]
{x : R} :
@[protected, instance]