Documentation

Mathlib.Algebra.Star.SelfAdjoint

Self-adjoint, skew-adjoint and normal elements of a star additive group #

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 isStarNormal_iff {R : Type u_1} [Mul R] [Star R] (x : R) :

IsStarNormal x ↔ Commute (star x) x

theorem star_comm_self' {R : Type u_1} [Mul R] [Star R] (x : R) [IsStarNormal x] :

star x * x = x * star x

theorem IsSelfAdjoint.all {R : Type u_1} [Star R] [TrivialStar R] (r : R) :

IsSelfAdjoint r

All elements are self-adjoint when star is trivial.

theorem IsSelfAdjoint.star_eq {R : Type u_1} [Star R] {x : R} (hx : IsSelfAdjoint x) :

star x = x

theorem isSelfAdjoint_iff {R : Type u_1} [Star R] {x : R} :

IsSelfAdjoint x ↔ star x = x

@[simp]

theorem IsSelfAdjoint.star_iff {R : Type u_1} [InvolutiveStar R] {x : R} :

IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

@[simp]

theorem IsSelfAdjoint.star_mul_self {R : Type u_1} [Mul R] [StarMul R] (x : R) :

IsSelfAdjoint (star x * x)

@[simp]

theorem IsSelfAdjoint.mul_star_self {R : Type u_1} [Mul R] [StarMul R] (x : R) :

IsSelfAdjoint (x * star x)

theorem IsSelfAdjoint.commute_iff {R : Type u_3} [Mul R] [StarMul R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

Commute x y ↔ IsSelfAdjoint (x * y)

Self-adjoint elements commute if and only if their product is self-adjoint.

theorem IsSelfAdjoint.map {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 : IsSelfAdjoint x) (f : F) :

IsSelfAdjoint (f x)

Functions in a StarHomClass preserve self-adjoint elements.

theorem isSelfAdjoint_map {F : Type u_3} {R : Type u_4} {S : Type u_5} [Star R] [Star S] [FunLike F R S] [StarHomClass F R S] [TrivialStar R] (f : F) (x : R) :

IsSelfAdjoint (f x)

@[simp]

theorem IsSelfAdjoint.zero (R : Type u_1) [AddMonoid R] [StarAddMonoid R] :

IsSelfAdjoint 0

theorem IsSelfAdjoint.add {R : Type u_1} [AddMonoid R] [StarAddMonoid R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

IsSelfAdjoint (x + y)

theorem IsSelfAdjoint.neg {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} (hx : IsSelfAdjoint x) :

IsSelfAdjoint (-x)

theorem IsSelfAdjoint.sub {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

IsSelfAdjoint (x - y)

@[simp]

theorem IsSelfAdjoint.add_star_self {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] (x : R) :

IsSelfAdjoint (x + star x)

@[simp]

theorem IsSelfAdjoint.star_add_self {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] (x : R) :

IsSelfAdjoint (star x + x)

theorem IsSelfAdjoint.conjugate {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) :

IsSelfAdjoint (z * x * star z)

theorem IsSelfAdjoint.conjugate' {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (z : R) :

IsSelfAdjoint (star z * x * z)

theorem IsSelfAdjoint.conjugate_self {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) {z : R} (hz : IsSelfAdjoint z) :

IsSelfAdjoint (z * x * z)

theorem IsSelfAdjoint.isStarNormal {R : Type u_1} [Semigroup R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) :

@[simp]

theorem IsSelfAdjoint.one (R : Type u_1) [MulOneClass R] [StarMul R] :

IsSelfAdjoint 1

theorem IsSelfAdjoint.pow {R : Type u_1} [Monoid R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℕ) :

IsSelfAdjoint (x ^ n)

@[simp]

theorem IsSelfAdjoint.natCast {R : Type u_1} [Semiring R] [StarRing R] (n : ℕ) :

IsSelfAdjoint ↑n

@[simp]

theorem IsSelfAdjoint.ofNat {R : Type u_1} [Semiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :

IsSelfAdjoint (OfNat.ofNat n)

theorem IsSelfAdjoint.mul {R : Type u_1} [CommSemigroup R] [StarMul R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

IsSelfAdjoint (x * y)

theorem IsSelfAdjoint.conj_eq {α : Type u_3} [CommSemiring α] [StarRing α] {a : α} (ha : IsSelfAdjoint a) :

(starRingEnd α) a = a

@[simp]

theorem IsSelfAdjoint.intCast {R : Type u_1} [Ring R] [StarRing R] (z : ℤ) :

IsSelfAdjoint ↑z

theorem IsSelfAdjoint.inv {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) :

IsSelfAdjoint x⁻¹

theorem IsSelfAdjoint.zpow {R : Type u_1} [Group R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℤ) :

IsSelfAdjoint (x ^ n)

theorem IsSelfAdjoint.inv₀ {R : Type u_1} [GroupWithZero R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) :

IsSelfAdjoint x⁻¹

theorem IsSelfAdjoint.zpow₀ {R : Type u_1} [GroupWithZero R] [StarMul R] {x : R} (hx : IsSelfAdjoint x) (n : ℤ) :

IsSelfAdjoint (x ^ n)

@[simp]

theorem IsSelfAdjoint.nnratCast {R : Type u_1} [DivisionSemiring R] [StarRing R] (q : ℚ≥0) :

IsSelfAdjoint ↑q

@[simp]

theorem IsSelfAdjoint.ratCast {R : Type u_1} [DivisionRing R] [StarRing R] (x : ℚ) :

IsSelfAdjoint ↑x

theorem IsSelfAdjoint.div {R : Type u_1} [Semifield R] [StarRing R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :

IsSelfAdjoint (x / y)

theorem IsSelfAdjoint.smul {R : Type u_1} {A : Type u_2} [Star R] [Star A] [SMul R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) {x : A} (hx : IsSelfAdjoint x) :

IsSelfAdjoint (r • x)

theorem IsSelfAdjoint.smul_iff {R : Type u_1} {A : Type u_2} [Monoid R] [StarMul R] [Star A] [MulAction R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) (hu : IsUnit r) {x : A} :

IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

def selfAdjoint (R : Type u_1) [AddGroup R] [StarAddMonoid R] :

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

Equations

Instances For

def skewAdjoint (R : Type u_1) [AddCommGroup R] [StarAddMonoid R] :

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

Equations

Instances For

theorem selfAdjoint.mem_iff {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : R} :

x ∈ selfAdjoint R ↔ star x = x

@[simp]

theorem selfAdjoint.star_val_eq {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : ↥(selfAdjoint R)} :

star ↑x = ↑x

instance selfAdjoint.instInhabitedSubtypeMemAddSubgroup {R : Type u_1} [AddGroup R] [StarAddMonoid R] :

Inhabited ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.isSelfAdjoint {R : Type u_1} [AddGroup R] [StarAddMonoid R] {x : ↥(selfAdjoint R)} :

IsSelfAdjoint ↑x

instance selfAdjoint.isStarNormal {R : Type u_1} [NonUnitalRing R] [StarRing R] (x : ↥(selfAdjoint R)) :

IsStarNormal ↑x

instance selfAdjoint.instOneSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] :

One ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_one {R : Type u_1} [Ring R] [StarRing R] :

↑1 = 1

instance selfAdjoint.instNontrivialSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] [Nontrivial R] :

Nontrivial ↥(selfAdjoint R)

instance selfAdjoint.instNatCastSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] :

NatCast ↥(selfAdjoint R)

Equations

instance selfAdjoint.instIntCastSubtypeMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] :

IntCast ↥(selfAdjoint R)

Equations

instance selfAdjoint.instPowSubtypeMemAddSubgroupNat {R : Type u_1} [Ring R] [StarRing R] :

Pow ↥(selfAdjoint R) ℕ

Equations

@[simp]

theorem selfAdjoint.val_pow {R : Type u_1} [Ring R] [StarRing R] (x : ↥(selfAdjoint R)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

instance selfAdjoint.instMulSubtypeMemAddSubgroup {R : Type u_1} [NonUnitalCommRing R] [StarRing R] :

Mul ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_mul {R : Type u_1} [NonUnitalCommRing R] [StarRing R] (x y : ↥(selfAdjoint R)) :

↑(x * y) = ↑x * ↑y

instance selfAdjoint.instCommRingSubtypeMemAddSubgroup {R : Type u_1} [CommRing R] [StarRing R] :

CommRing ↥(selfAdjoint R)

Equations

instance selfAdjoint.instInvSubtypeMemAddSubgroup {R : Type u_1} [Field R] [StarRing R] :

Inv ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_inv {R : Type u_1} [Field R] [StarRing R] (x : ↥(selfAdjoint R)) :

↑x⁻¹ = (↑x)⁻¹

instance selfAdjoint.instDivSubtypeMemAddSubgroup {R : Type u_1} [Field R] [StarRing R] :

Div ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_div {R : Type u_1} [Field R] [StarRing R] (x y : ↥(selfAdjoint R)) :

↑(x / y) = ↑x / ↑y

instance selfAdjoint.instPowSubtypeMemAddSubgroupInt {R : Type u_1} [Field R] [StarRing R] :

Pow ↥(selfAdjoint R) ℤ

Equations

@[simp]

theorem selfAdjoint.val_zpow {R : Type u_1} [Field R] [StarRing R] (x : ↥(selfAdjoint R)) (z : ℤ) :

↑(x ^ z) = ↑x ^ z

instance selfAdjoint.instNNRatCast {R : Type u_1} [Field R] [StarRing R] :

NNRatCast ↥(selfAdjoint R)

Equations

instance selfAdjoint.instRatCast {R : Type u_1} [Field R] [StarRing R] :

RatCast ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_nnratCast {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) :

↑↑q = ↑q

@[simp]

theorem selfAdjoint.val_ratCast {R : Type u_1} [Field R] [StarRing R] (q : ℚ) :

↑↑q = ↑q

instance selfAdjoint.instSMulNNRat {R : Type u_1} [Field R] [StarRing R] :

SMul ℚ≥0 ↥(selfAdjoint R)

Equations

instance selfAdjoint.instSMulRat {R : Type u_1} [Field R] [StarRing R] :

SMul ℚ ↥(selfAdjoint R)

Equations

@[simp]

theorem selfAdjoint.val_nnqsmul {R : Type u_1} [Field R] [StarRing R] (q : ℚ≥0) (x : ↥(selfAdjoint R)) :

↑(q • x) = q • ↑x

@[simp]

theorem selfAdjoint.val_qsmul {R : Type u_1} [Field R] [StarRing R] (q : ℚ) (x : ↥(selfAdjoint R)) :

↑(q • x) = q • ↑x

instance selfAdjoint.instField {R : Type u_1} [Field R] [StarRing R] :

Field ↥(selfAdjoint R)

Equations

instance selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [SMul R A] [StarModule R A] :

SMul R ↥(selfAdjoint A)

Equations

@[simp]

theorem selfAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [SMul R A] [StarModule R A] (r : R) (x : ↥(selfAdjoint A)) :

↑(r • x) = r • ↑x

instance selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [Monoid R] [MulAction R A] [StarModule R A] :

MulAction R ↥(selfAdjoint A)

Equations

instance selfAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] :

DistribMulAction R ↥(selfAdjoint A)

Equations

instance selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Semiring R] [Module R A] [StarModule R A] :

Module R ↥(selfAdjoint A)

Equations

theorem skewAdjoint.mem_iff {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : R} :

x ∈ skewAdjoint R ↔ star x = -x

@[simp]

theorem skewAdjoint.star_val_eq {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] {x : ↥(skewAdjoint R)} :

star ↑x = -↑x

instance skewAdjoint.instInhabitedSubtypeMemAddSubgroup {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] :

Inhabited ↥(skewAdjoint R)

Equations

theorem skewAdjoint.conjugate {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) (z : R) :

z * x * star z ∈ skewAdjoint R

theorem skewAdjoint.conjugate' {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) (z : R) :

star z * x * z ∈ skewAdjoint R

theorem skewAdjoint.isStarNormal_of_mem {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : x ∈ skewAdjoint R) :

instance skewAdjoint.instIsStarNormalValMemAddSubgroup {R : Type u_1} [Ring R] [StarRing R] (x : ↥(skewAdjoint R)) :

IsStarNormal ↑x

theorem skewAdjoint.smul_mem {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A} (h : x ∈ skewAdjoint A) :

r • x ∈ skewAdjoint A

instance skewAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] :

SMul R ↥(skewAdjoint A)

Equations

@[simp]

theorem skewAdjoint.val_smul {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) (x : ↥(skewAdjoint A)) :

↑(r • x) = r • ↑x

instance skewAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Monoid R] [DistribMulAction R A] [StarModule R A] :

DistribMulAction R ↥(skewAdjoint A)

Equations

instance skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule {R : Type u_1} {A : Type u_2} [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A] [Semiring R] [Module R A] [StarModule R A] :

Module R ↥(skewAdjoint A)

Equations

theorem IsSelfAdjoint.smul_mem_skewAdjoint {R : Type u_1} {A : Type u_2} [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A] [StarModule R A] {r : R} (hr : r ∈ skewAdjoint R) {a : A} (ha : IsSelfAdjoint a) :

r • a ∈ skewAdjoint A

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

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

IsSelfAdjoint (r • a)

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

instance IsStarNormal.zero {R : Type u_1} [Semiring R] [StarRing R] :

instance IsStarNormal.one {R : Type u_1} [MulOneClass R] [StarMul R] :

instance IsStarNormal.star {R : Type u_1} [Mul R] [StarMul R] {x : R} [IsStarNormal x] :

IsStarNormal (star x)

instance IsStarNormal.neg {R : Type u_1} [Ring R] [StarAddMonoid R] {x : R} [IsStarNormal x] :

IsStarNormal (-x)

instance IsStarNormal.val_inv {R : Type u_1} [Monoid R] [StarMul R] {x : Rˣ} [IsStarNormal ↑x] :

IsStarNormal ↑x⁻¹

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 : IsStarNormal r] :

IsStarNormal (f r)

instance IsStarNormal.smul {R : Type u_3} {A : Type u_4} [SMul R A] [Star R] [Star A] [Mul A] [StarModule R A] [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (a : A) [ha : IsStarNormal a] :

IsStarNormal (r • a)

@[instance 100]

instance TrivialStar.isStarNormal {R : Type u_1} [Mul R] [StarMul R] [TrivialStar R] {x : R} :

@[instance 100]

instance CommMonoid.isStarNormal {R : Type u_1} [CommMonoid R] [StarMul R] {x : R} :

theorem Pi.isSelfAdjoint {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :

IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)

theorem IsSelfAdjoint.apply {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Star (α i)] {f : (i : ι) → α i} :

IsSelfAdjoint f → ∀ (i : ι), IsSelfAdjoint (f i)

Alias of the forward direction of Pi.isSelfAdjoint.