Nilpotent self-adjoint elements, anticommutation and star transposition

In a star monoid with zero whose star is proper (IsProperStar: star x * x = 0 forces x = 0), such as a matrix ring over a star-ordered ring like ℝ or ℂ, a self-adjoint element x with x * x = star x * x = 0 is zero. Since the powers of a self-adjoint element are self-adjoint, peeling off squares shows that a nilpotent self-adjoint element is zero. This is what rules out nonzero nilpotent ideals in an algebra of matrices closed under conjugate transposition.

In a star ring, taking adjoints shows that an element anticommuting with a self-adjoint γ has an adjoint anticommuting with γ, as needed for gradings. Similarly, taking stars transposes one-sided relations with a self-adjoint element: x * q = x becomes q * x = x for self-adjoint x, and q * u = 0 becomes star u * q = 0. For a self-adjoint p, the element 2 p - 1 is again self-adjoint.

Main results

• IsSelfAdjoint.eq_zero_of_isNilpotent: a nilpotent self-adjoint element is zero.
• IsSelfAdjoint.mul_star_eq_neg_star_mul: if γ * x = -(x * γ) for a self-adjoint γ, then γ * star x = -(star x * γ).
• IsSelfAdjoint.mul_eq_right_of_mul_eq_left: for self-adjoint x and q, x * q = x implies q * x = x.
• IsSelfAdjoint.star_mul_eq_zero_of_mul_eq_zero: for self-adjoint q, q * u = 0 implies star u * q = 0.
• IsSelfAdjoint.two_mul_sub_one: 2 p - 1 is self-adjoint for a self-adjoint p.

theorem IsSelfAdjoint.eq_zero_of_isNilpotent {R : Type u_1} [MonoidWithZero R] [StarMul R] [IsProperStar R] {x : R} (hx : IsSelfAdjoint x) (hnil : IsNilpotent x) : x = 0

A nilpotent self-adjoint element is zero when the star is proper. Some such hypothesis is needed: over ZMod 2 the symmetric matrix !![1, 1; 1, 1] squares to zero.

theorem IsSelfAdjoint.mul_star_eq_neg_star_mul {R : Type u_1} [NonUnitalNonAssocRing R] [StarRing R] {γ x : R} (hγ : IsSelfAdjoint γ) (h : γ * x = -(x * γ)) : γ * star x = -(star x * γ)

An element anticommuting with a self-adjoint γ has an adjoint anticommuting with γ.

theorem IsSelfAdjoint.mul_eq_right_of_mul_eq_left {R : Type u_1} [Mul R] [StarMul R] {x q : R} (hx : IsSelfAdjoint x) (hq : IsSelfAdjoint q) (h : x * q = x) : q * x = x

For self-adjoint x and q, taking stars turns x * q = x into q * x = x.

theorem IsSelfAdjoint.star_mul_eq_zero_of_mul_eq_zero {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarRing R] {q u : R} (hq : IsSelfAdjoint q) (h : q * u = 0) : star u * q = 0

For self-adjoint q, taking stars turns q * u = 0 into star u * q = 0.

theorem IsSelfAdjoint.two_mul_sub_one {R : Type u_1} [Ring R] [StarRing R] {p : R} (hp : IsSelfAdjoint p) : IsSelfAdjoint (2 * p - 1)

For a self-adjoint p, 2 p - 1 is self-adjoint.