chore(*/pi): rename *_hom.apply to pi.eval_*_hom (#5851)

These definitions state the fact that fixing an `i` and applying a function `(Π i, f i)` maintains the algebraic structure of the function. We already have a name for this operation, `function.eval`.

These isn't a statement about `monoid_hom` or `ring_hom` at all - that just happens to be their type.
For this reason, this commit moves all the definitions of this type into the `pi` namespace:

* `add_monoid_hom.apply` → `pi.eval_add_monoid_hom`
* `monoid_hom.apply` → `pi.eval_monoid_hom`
* `ring_hom.apply` → `pi.eval_ring_hom`
* `pi.alg_hom.apply` [sic] → `pi.eval_alg_hom`

This scales better, because we might want to say that applying a `linear_map` over a non-commutative ring is an `add_monoid_hom`. Using the naming convention established by this commit, that's easy; it's `linear_map.eval_add_monoid_hom` to mirror `pi.apply_add_monoid_hom`.

This partially addresses [this zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Naming.3A.20eval.20vs.20apply/near/223813950)

src/algebra/algebra/basic.lean

@@ -1340,13 +1340,14 @@ instance algebra {r : comm_semiring R}
 -- 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)
+variables {I} (R) (f)
 
-/-- `function.eval` as an `alg_hom`. The name matches `ring_hom.apply`, `monoid_hom.apply`, etc. -/
+/-- `function.eval` as an `alg_hom`. The name matches `pi.eval_ring_hom`, `pi.eval_monoid_hom`,
+etc. -/
 @[simps]
-def alg_hom.apply {r : comm_semiring R} [Π i, semiring (f i)] [Π i, algebra R (f i)] (i : I) :
+def eval_alg_hom {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}
+{ to_fun := λ f, f i, commutes' := λ r, rfl, .. pi.eval_ring_hom f i}
 
 end pi
 

src/algebra/big_operators/pi.lean

@@ -21,19 +21,19 @@ namespace pi
 @[to_additive]
 lemma list_prod_apply {α : Type*} {β : α → Type*} [Πa, monoid (β a)] (a : α) (l : list (Πa, β a)) :
   l.prod a = (l.map (λf:Πa, β a, f a)).prod :=
-(monoid_hom.apply β a).map_list_prod _
+(eval_monoid_hom β a).map_list_prod _
 
 @[to_additive]
 lemma multiset_prod_apply {α : Type*} {β : α → Type*} [∀a, comm_monoid (β a)] (a : α)
   (s : multiset (Πa, β a)) : s.prod a = (s.map (λf:Πa, β a, f a)).prod :=
-(monoid_hom.apply β a).map_multiset_prod _
+(eval_monoid_hom β a).map_multiset_prod _
 
 end pi
 
 @[simp, to_additive]
 lemma finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀a, comm_monoid (β a)] (a : α)
   (s : finset γ) (g : γ → Πa, β a) : (∏ c in s, g c) a = ∏ c in s, g c a :=
-(monoid_hom.apply β a).map_prod _ _
+(pi.eval_monoid_hom β a).map_prod _ _
 
 /-- An 'unapplied' analogue of `finset.prod_apply`. -/
 @[to_additive "An 'unapplied' analogue of `finset.sum_apply`."]

src/algebra/category/Group/biproducts.lean

@@ -79,7 +79,7 @@ Construct limit data for a product in `AddCommGroup`, using `AddCommGroup.of (Π
 def product_limit_cone : limits.limit_cone F :=
 { cone :=
   { X := AddCommGroup.of (Π j, F.obj j),
-    π := discrete.nat_trans (λ j, add_monoid_hom.apply (λ j, F.obj j) j), },
+    π := discrete.nat_trans (λ j, pi.eval_add_monoid_hom (λ j, F.obj j) j), },
   is_limit :=
   { lift := lift F,
     fac' := λ s j, by { ext, simp, },

src/algebra/char_p/pi.lean

@@ -18,9 +18,9 @@ namespace char_p
 instance pi (ι : Type u) [hi : nonempty ι] (R : Type v) [semiring R] (p : ℕ) [char_p R p] :
   char_p (ι → R) p :=
 ⟨λ x, let ⟨i⟩ := hi in iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
-⟨λ h, funext $ λ j, show ring_hom.apply (λ _, R) j (↑x : ι → R) = 0,
+⟨λ h, funext $ λ j, show pi.eval_ring_hom (λ _, R) j (↑x : ι → R) = 0,
     by rw [ring_hom.map_nat_cast, h],
-  λ h, (ring_hom.apply (λ _, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+  λ h, (pi.eval_ring_hom (λ _, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
 
 -- diamonds
 instance pi' (ι : Type u) [hi : nonempty ι] (R : Type v) [comm_ring R] (p : ℕ) [char_p R p] :

src/algebra/group/pi.lean

@@ -144,17 +144,15 @@ section monoid_hom
 variables (f) [Π i, mul_one_class (f i)]
 
 /-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
-homomorphism. -/
-@[to_additive "Evaluation of functions into an indexed collection of additive monoids at a point
-is an additive monoid homomorphism."]
-def monoid_hom.apply (i : I) : (Π i, f i) →* f i :=
+homomorphism.
+This is `function.eval i` as a `monoid_hom`. -/
+@[to_additive "Evaluation of functions into an indexed collection of additive monoids at a
+point is an additive monoid homomorphism.
+This is `function.eval i` as an `add_monoid_hom`.", simps]
+def pi.eval_monoid_hom (i : I) : (Π i, f i) →* f i :=
 { to_fun := λ g, g i,
-  map_one' := rfl,
-  map_mul' := λ x y, rfl, }
-
-@[simp, to_additive]
-lemma monoid_hom.apply_apply (i : I) (g : Π i, f i) :
-  (monoid_hom.apply f i) g = g i := rfl
+  map_one' := pi.one_apply i,
+  map_mul' := λ x y, pi.mul_apply _ _ i, }
 
 /-- Coercion of a `monoid_hom` into a function is itself a `monoid_hom`.
 

src/algebra/ring/pi.lean

@@ -60,21 +60,17 @@ protected def ring_hom
   pi.ring_hom f g a = f a g :=
 rfl
 
-end pi
-
 section ring_hom
 
-variable {I : Type*}     -- The indexing type
-variable (f : I → Type*) -- The family of types already equipped with instances
-variables [Π i, semiring (f i)]
+variables [Π i, semiring (f i)] (f)
 
 /-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
-homomorphism. -/
-def ring_hom.apply (i : I) : (Π i, f i) →+* f i :=
-{ ..(monoid_hom.apply f i),
-  ..(add_monoid_hom.apply f i) }
-
-@[simp]
-lemma ring_hom.apply_apply (i : I) (g : Π i, f i) : (ring_hom.apply f i) g = g i := rfl
+homomorphism. This is `function.eval` as a `ring_hom`. -/
+@[simps]
+def eval_ring_hom (i : I) : (Π i, f i) →+* f i :=
+{ ..(eval_monoid_hom f i),
+  ..(eval_add_monoid_hom f i) }
 
 end ring_hom
+
+end pi

src/data/dfinsupp.lean

@@ -157,9 +157,9 @@ def coe_fn_add_monoid_hom [Π i, add_zero_class (β i)] : (Π₀ i, β i) →+ (
 { to_fun := coe_fn, map_zero' := coe_zero, map_add' := coe_add }
 
 /-- Evaluation at a point is an `add_monoid_hom`. This is the finitely-supported version of
-`add_monoid_hom.apply`. -/
+`pi.eval_add_monoid_hom`. -/
 def eval_add_monoid_hom [Π i, add_zero_class (β i)] (i : ι) : (Π₀ i, β i) →+ β i :=
-(add_monoid_hom.apply β i).comp coe_fn_add_monoid_hom
+(pi.eval_add_monoid_hom β i).comp coe_fn_add_monoid_hom
 
 instance is_add_monoid_hom [Π i, add_zero_class (β i)] {i : ι} :
   is_add_monoid_hom (λ g : Π₀ i : ι, β i, g i) :=

src/data/polynomial/algebra_map.lean

@@ -197,7 +197,7 @@ aeval_alg_hom_apply (algebra.of_id R A) x p
 
 @[simp] lemma aeval_fn_apply {X : Type*} (g : polynomial R) (f : X → R) (x : X) :
   ((aeval f) g) x = aeval (f x) g :=
-(aeval_alg_hom_apply (pi.alg_hom.apply _ _ _ x) f g).symm
+(aeval_alg_hom_apply (pi.eval_alg_hom _ _ x) f g).symm
 
 @[norm_cast] lemma aeval_subalgebra_coe
   (g : polynomial R) {A : Type*} [semiring A] [algebra R A] (s : subalgebra R A) (f : s) :

src/linear_algebra/quadratic_form.lean

@@ -271,7 +271,7 @@ def coe_fn_add_monoid_hom : quadratic_form R M →+ (M → R) :=
 /-- Evaluation on a particular element of the module `M` is an additive map over quadratic forms. -/
 @[simps apply]
 def eval_add_monoid_hom (m : M) : quadratic_form R M →+ R :=
-(add_monoid_hom.apply _ m).comp coe_fn_add_monoid_hom
+(pi.eval_add_monoid_hom _ m).comp coe_fn_add_monoid_hom
 
 section sum
 

src/ring_theory/witt_vector/basic.lean

@@ -240,7 +240,7 @@ def ghost_map : 𝕎 R →+* ℕ → R :=
 
 /-- Evaluates the `n`th Witt polynomial on the first `n` coefficients of `x`,
 producing a value in `R`. -/
-def ghost_component (n : ℕ) : 𝕎 R →+* R := (ring_hom.apply _ n).comp ghost_map
+def ghost_component (n : ℕ) : 𝕎 R →+* R := (pi.eval_ring_hom _ n).comp ghost_map
 
 lemma ghost_component_apply (n : ℕ) (x : 𝕎 R) : ghost_component n x = aeval x.coeff (W_ ℤ n) := rfl