feat(algebra/algebra/basic): add alg_hom.apply (#7278)

This also renames some variables from α to R for readability

src/algebra/algebra/basic.lean

@@ -1286,24 +1286,33 @@ We couldn't set this up back in `algebra.pi_instances` because this file imports
 namespace pi
 
 variable {I : Type u}     -- The indexing type
+variable {R : Type*}      -- The scalar type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
 variables (I f)
 
-instance algebra (α) {r : comm_semiring α}
-  [s : ∀ i, semiring (f i)] [∀ i, algebra α (f i)] :
-  algebra α (Π i : I, f i) :=
+instance algebra {r : comm_semiring R}
+  [s : ∀ i, semiring (f i)] [∀ i, algebra R (f i)] :
+  algebra R (Π i : I, f i) :=
 { commutes' := λ a f, begin ext, simp [algebra.commutes], end,
   smul_def' := λ a f, begin ext, simp [algebra.smul_def''], end,
-  ..pi.ring_hom (λ i, algebra_map α (f i)) }
+  ..pi.ring_hom (λ i, algebra_map R (f i)) }
 
-@[simp] lemma algebra_map_apply (α) {r : comm_semiring α}
-  [s : ∀ i, semiring (f i)] [∀ i, algebra α (f i)] (a : α) (i : I) :
-  algebra_map α (Π i, f i) a i = algebra_map α (f i) a := rfl
+@[simp] lemma algebra_map_apply {r : comm_semiring R}
+  [s : ∀ i, semiring (f i)] [∀ i, algebra R (f i)] (a : R) (i : I) :
+  algebra_map R (Π i, f i) a i = algebra_map R (f i) a := rfl
 
 -- One could also build a `Π i, R i`-algebra structure on `Π i, A i`,
 -- when each `A i` is an `R i`-algebra, although I'm not sure that it's useful.
 
+variables (R) (f)
+
+/-- `function.eval` as an `alg_hom`. The name matches `ring_hom.apply`, `monoid_hom.apply`, etc. -/
+@[simps]
+def alg_hom.apply {r : comm_semiring R} [Π i, semiring (f i)] [Π i, algebra R (f i)] (i : I) :
+  (Π i, f i) →ₐ[R] f i :=
+{ commutes' := λ r, rfl, .. ring_hom.apply f i}
+
 end pi
 
 section is_scalar_tower