feat(algebra/star/self_adjoint): define normal elements of a star monoid (#11991)

In this PR, we define the normal elements of a star monoid, i.e. those elements `x`
that commute with `star x`. This is defined as the prop type class `is_star_normal`.

This was formalized as part of the semilinear maps paper.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author: dupuisf

src/algebra/star/self_adjoint.lean

@@ -8,12 +8,15 @@ import algebra.star.basic
 import group_theory.subgroup.basic
 
 /-!
-# Self-adjoint and skew-adjoint elements of a star additive group
+# 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 a `star_module R₂ R`, then `self_adjoint R` has a natural
@@ -54,6 +57,16 @@ def skew_adjoint [add_comm_group R] [star_add_monoid R] : add_subgroup R :=
 
 variables {R}
 
+/-- An element of a star monoid is normal if it commutes with its adjoint. -/
+class is_star_normal [has_mul R] [has_star R] (x : R) : Prop :=
+(star_comm_self : commute (star x) x)
+
+export is_star_normal (star_comm_self)
+
+lemma star_comm_self' [has_mul R] [has_star R] (x : R) [is_star_normal x] :
+  (star x) * x = x * star x :=
+is_star_normal.star_comm_self
+
 namespace self_adjoint
 
 section add_group
@@ -91,6 +104,12 @@ by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
 lemma conjugate' {x : R} (hx : x ∈ self_adjoint R) (z : R) : star z * x * z ∈ self_adjoint R :=
 by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
 
+lemma is_star_normal_of_mem {x : R} (hx : x ∈ self_adjoint R) : is_star_normal x :=
+⟨by { simp only [mem_iff] at hx, simp only [hx] }⟩
+
+instance (x : self_adjoint R) : is_star_normal (x : R) :=
+is_star_normal_of_mem (set_like.coe_mem _)
+
 instance : has_pow (self_adjoint R) ℕ :=
 ⟨λ x n, ⟨(x : R) ^ n, by simp only [mem_iff, star_pow, star_coe_eq]⟩⟩
 
@@ -212,6 +231,12 @@ by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul
 lemma conjugate' {x : R} (hx : x ∈ skew_adjoint R) (z : R) : star z * x * z ∈ skew_adjoint R :=
 by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, neg_mul, mul_neg, mul_assoc]
 
+lemma is_star_normal_of_mem {x : R} (hx : x ∈ skew_adjoint R) : is_star_normal x :=
+⟨by { simp only [mem_iff] at hx, simp only [hx, commute.neg_left] }⟩
+
+instance (x : skew_adjoint R) : is_star_normal (x : R) :=
+is_star_normal_of_mem (set_like.coe_mem _)
+
 end ring
 
 section has_scalar
@@ -237,3 +262,23 @@ function.injective.module R (skew_adjoint A).subtype subtype.coe_injective coe_s
 end has_scalar
 
 end skew_adjoint
+
+instance is_star_normal_zero [semiring R] [star_ring R] : is_star_normal (0 : R) :=
+⟨by simp only [star_comm_self, star_zero]⟩
+
+instance is_star_normal_one [monoid R] [star_semigroup R] : is_star_normal (1 : R) :=
+⟨by simp only [star_comm_self, star_one]⟩
+
+instance is_star_normal_star_self [monoid R] [star_semigroup R] {x : R} [is_star_normal x] :
+  is_star_normal (star x) :=
+⟨show star (star x) * (star x) = (star x) * star (star x), by rw [star_star, star_comm_self']⟩
+
+@[priority 100] -- see Note [lower instance priority]
+instance has_trivial_star.is_star_normal [monoid R] [star_semigroup R]
+  [has_trivial_star R] {x : R} : is_star_normal x :=
+⟨by rw [star_trivial]⟩
+
+@[priority 100] -- see Note [lower instance priority]
+instance comm_monoid.is_star_normal [comm_monoid R] [star_semigroup R] {x : R} :
+  is_star_normal x :=
+⟨mul_comm _ _⟩