feat(algebra/star/self_adjoint): module instance on self-adjoint elem…

…ents of a star algebra (#11322)

We put a module instance on `self_adjoint A`, where `A` is a `[star_module R A]` and `R` has a trivial star operation. A new typeclass `[has_trivial_star R]` is created for this purpose with an instance on `ℝ`. This allows us to express the fact that e.g. the space of complex Hermitian matrices is a real vector space.

src/algebra/star/basic.lean

@@ -75,6 +75,15 @@ star_involutive _
 lemma star_injective [has_involutive_star R] : function.injective (star : R → R) :=
 star_involutive.injective
 
+/--
+Typeclass for a trivial star operation. This is mostly meant for `ℝ`.
+-/
+class has_trivial_star (R : Type u) [has_star R] :=
+(star_trivial : ∀ (r : R), star r = r)
+
+export has_trivial_star (star_trivial)
+attribute [simp] star_trivial
+
 /--
 A `*`-monoid is a monoid `R` with an involutive operations `star`
 so `star (r * s) = star s * star r`.

src/algebra/star/self_adjoint.lean

@@ -14,16 +14,19 @@ This file defines `self_adjoint R`, where `R` is a star additive monoid, as the
 containing the elements that satisfy `star x = x`. This includes, for instance, Hermitian
 operators on Hilbert spaces.
 
-## TODO
+## 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.)
 
-* If `R` is a `star_module R₂ R`, put a module structure on `self_adjoint R`. This would naturally
-  be a `module (self_adjoint R₂) (self_adjoint R)`, but 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)`. One way of doing this would be to add the typeclass
-  `[has_trivial_star R]`, of which `ℝ` would be an instance, and then add a
-  `[module R (self_adjoint E)]` instance whenever we have `[module R E] [has_trivial_star E]`.
-  Another one would be to define a `[star_invariant_scalars R E]` to express the fact that
-  `star (x • v) = x • star v`.
+## 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
@@ -119,4 +122,29 @@ instance : field (self_adjoint R) :=
 
 end field
 
+section module
+
+variables {A : Type*} [semiring R] [has_star R] [has_trivial_star R] [add_comm_group A]
+  [star_add_monoid A] [module R A] [star_module R A]
+
+instance : has_scalar R (self_adjoint A) :=
+⟨λ r x, ⟨r • x, by rw [mem_iff, star_smul, star_trivial, star_coe_eq]⟩⟩
+
+@[simp, norm_cast] lemma coe_smul (r : R) (x : self_adjoint A) :
+  (coe : self_adjoint A → A) (r • x) = r • x := rfl
+
+instance : mul_action R (self_adjoint A) :=
+{ one_smul := λ x, by { ext, rw [coe_smul, one_smul] },
+  mul_smul := λ r s x, by { ext, simp only [mul_smul, coe_smul] } }
+
+instance : distrib_mul_action R (self_adjoint A) :=
+{ smul_add := λ r x y, by { ext, simp only [smul_add, add_subgroup.coe_add, coe_smul] },
+  smul_zero := λ r, by { ext, simp only [smul_zero', coe_smul, add_subgroup.coe_zero] } }
+
+instance : module R (self_adjoint A) :=
+{ add_smul := λ r s x, by { ext, simp only [add_smul, add_subgroup.coe_add, coe_smul] },
+  zero_smul := λ x, by { ext, simp only [coe_smul, zero_smul, add_subgroup.coe_zero] } }
+
+end module
+
 end self_adjoint

src/data/real/basic.lean

@@ -108,6 +108,7 @@ instance : inhabited ℝ          := ⟨0⟩
 
 /-- The real numbers are a `*`-ring, with the trivial `*`-structure. -/
 instance : star_ring ℝ          := star_ring_of_comm
+instance : has_trivial_star ℝ   := ⟨λ _, rfl⟩
 
 /-- Coercion `ℚ` → `ℝ` as a `ring_hom`. Note that this
 is `cau_seq.completion.of_rat`, not `rat.cast`. -/