From 57b0e68f4e056185851ef9d980f2283538c3a561 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 15 May 2021 21:20:50 +0000 Subject: [PATCH] chore(*/pi): rename *_hom.apply to pi.eval_*_hom (#5851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 9 +++++---- src/algebra/big_operators/pi.lean | 6 +++--- src/algebra/category/Group/biproducts.lean | 2 +- src/algebra/char_p/pi.lean | 4 ++-- src/algebra/group/pi.lean | 18 ++++++++---------- src/algebra/ring/pi.lean | 20 ++++++++------------ src/data/dfinsupp.lean | 4 ++-- src/data/polynomial/algebra_map.lean | 2 +- src/linear_algebra/quadratic_form.lean | 2 +- src/ring_theory/witt_vector/basic.lean | 2 +- 10 files changed, 32 insertions(+), 37 deletions(-) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index 71255b1dac62c..293f32bde90c7 100644 --- a/src/algebra/algebra/basic.lean +++ b/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 diff --git a/src/algebra/big_operators/pi.lean b/src/algebra/big_operators/pi.lean index ffb4874072e04..fa32e9ff5a7c1 100644 --- a/src/algebra/big_operators/pi.lean +++ b/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`."] diff --git a/src/algebra/category/Group/biproducts.lean b/src/algebra/category/Group/biproducts.lean index ef00e2626a7ca..10730e722a3dc 100644 --- a/src/algebra/category/Group/biproducts.lean +++ b/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, }, diff --git a/src/algebra/char_p/pi.lean b/src/algebra/char_p/pi.lean index 61bbe3ee9cfa5..b87b8a93d4f30 100644 --- a/src/algebra/char_p/pi.lean +++ b/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] : diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean index 6dab665c91e74..67837111d6230 100644 --- a/src/algebra/group/pi.lean +++ b/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`. diff --git a/src/algebra/ring/pi.lean b/src/algebra/ring/pi.lean index 1198dc4287617..6f44f77929b46 100644 --- a/src/algebra/ring/pi.lean +++ b/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 diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 0ff0c69a695c7..4e30af3272b30 100644 --- a/src/data/dfinsupp.lean +++ b/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) := diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean index e80c4b3bb5aad..58a367498c46d 100644 --- a/src/data/polynomial/algebra_map.lean +++ b/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) : diff --git a/src/linear_algebra/quadratic_form.lean b/src/linear_algebra/quadratic_form.lean index 75fa479fb331f..b893fdd0461bd 100644 --- a/src/linear_algebra/quadratic_form.lean +++ b/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 diff --git a/src/ring_theory/witt_vector/basic.lean b/src/ring_theory/witt_vector/basic.lean index c65dece4aa911..8165b12e66ce4 100644 --- a/src/ring_theory/witt_vector/basic.lean +++ b/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