From daf8adf14245800e936d0b7f3c9890d259eac81e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Wed, 14 Dec 2022 21:31:23 +0000
Subject: [PATCH] feat(algebra/star/basic): add ring_hom.has_involutive_star
 (#17904)

Define an instance `has_involutive_star` for ring homorphisms into a `star_ring`.
---
 src/algebra/star/basic.lean        | 12 ++++++++++++
 src/algebra/star/self_adjoint.lean |  4 ++++
 2 files changed, 16 insertions(+)

diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
index 9e4be9cab8f6b..2229212f9d368 100644
--- a/src/algebra/star/basic.lean
+++ b/src/algebra/star/basic.lean
@@ -291,6 +291,18 @@ lemma star_ring_end_apply [comm_semiring R] [star_ring R] {x : R} :
 @[simp] lemma star_ring_end_self_apply [comm_semiring R] [star_ring R] (x : R) :
   star_ring_end R (star_ring_end R x) = x := star_star x
 
+instance ring_hom.has_involutive_star {S : Type u} [non_assoc_semiring S] [comm_semiring R]
+  [star_ring R] : has_involutive_star (S →+* R) :=
+{ to_has_star := { star := λ f, ring_hom.comp (star_ring_end R) f },
+  star_involutive :=
+    by { intro _, ext, simp only [ring_hom.coe_comp, function.comp_app, star_ring_end_self_apply] }}
+
+lemma ring_hom.star_def {S : Type u} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
+  (f : S →+* R) : has_star.star f = ring_hom.comp (star_ring_end R) f := rfl
+
+lemma ring_hom.star_apply {S : Type u} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
+  (f : S →+* R) (s : S) : star f s = star (f s) := rfl
+
 -- A more convenient name for complex conjugation
 alias star_ring_end_self_apply ← complex.conj_conj
 alias star_ring_end_self_apply ← is_R_or_C.conj_conj
diff --git a/src/algebra/star/self_adjoint.lean b/src/algebra/star/self_adjoint.lean
index d33bddca15b18..81aa4b3834f10 100644
--- a/src/algebra/star/self_adjoint.lean
+++ b/src/algebra/star/self_adjoint.lean
@@ -58,6 +58,10 @@ lemma star_eq [has_star R] {x : R} (hx : is_self_adjoint x) : star x = x := hx
 
 lemma _root_.is_self_adjoint_iff [has_star R] {x : R} : is_self_adjoint x ↔ star x = x := iff.rfl
 
+@[simp]
+lemma star_iff [has_involutive_star R] {x : R} : is_self_adjoint (star x) ↔ is_self_adjoint x :=
+by simpa only [is_self_adjoint, star_star] using eq_comm
+
 @[simp]
 lemma star_mul_self [semigroup R] [star_semigroup R] (x : R) : is_self_adjoint (star x * x) :=
 by simp only [is_self_adjoint, star_mul, star_star]