From 8481bf46ebeee670a674512b6318a08729a1021e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 21 Apr 2021 00:48:48 +0000
Subject: [PATCH] feat(algebra/algebra/basic): add alg_hom.apply (#7278)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This also renames some variables from α to R for readability
---
 src/algebra/algebra/basic.lean | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
index b01f8bda218b9..ac4ca350dfe39 100644
--- a/src/algebra/algebra/basic.lean
+++ b/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