feat(algebra/star/star_alg_hom): define unital and non-unital `star_a…

…lg_hom`s (#16089)

This defines three new hom classes `star_hom_class`, `star_alg_hom_class` and `non_unital_star_alg_hom_class`, and associated hom types for the latter two.  `star_hom_class` is used essentially as a mixin.

The types `star_alg_hom` and `non_unital_star_alg_hom` constitute the morphisms in the categories of unital C⋆-algebras and C⋆-algebras, respectively.

Per this [recent discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/has_coe_t.20for.20semilinear_map_class), there are no coercions implemented for these new morphisms aside from the usual `has_coe_to_fun` arising from the `fun_like` instance. In particular, there is no coercion from `star_alg_hom` to `alg_hom`, nor for the non-unital variants, but of course there is the "manual coercion" `star_alg_hom.to_alg_hom`. Likewise, there is no coercion from `F` to `star_alg_hom R A B` given an instance `star_alg_hom_class F R A B`. Such coercions as we deem useful and prudent can be added later.

src/algebra/star/basic.lean

@@ -389,6 +389,18 @@ instance [comm_semiring R] [star_ring R] :
 
 end ring_hom_inv_pair
 
+section
+set_option old_structure_cmd true
+
+/-- `star_hom_class F R S` states that `F` is a type of `star`-preserving maps from `R` to `S`. -/
+class star_hom_class (F : Type*) (R S : out_param Type*) [has_star R] [has_star S]
+  extends fun_like F R (λ _, S) :=
+(map_star : ∀ (f : F) (r : R), f (star r) = star (f r))
+
+export star_hom_class (map_star)
+
+end
+
 /-! ### Instances -/
 
 namespace units

src/algebra/star/module.lean

@@ -117,3 +117,9 @@ linear_equiv.of_linear
   ((self_adjoint.submodule R A).subtype.coprod (skew_adjoint.submodule R A).subtype)
   (by ext; simp)
   (linear_map.ext $ star_module.self_adjoint_part_add_skew_adjoint_part R)
+
+@[simp]
+lemma algebra_map_star_comm {R A : Type*} [comm_semiring R] [star_ring R] [semiring A]
+  [star_semigroup A] [algebra R A] [star_module R A] (r : R) :
+  algebra_map R A (star r) = star (algebra_map R A r) :=
+by simp only [algebra.algebra_map_eq_smul_one, star_smul, star_one]