## Stream: Is there code for X?

### Topic: poly (a)eval and algebra maps

#### Moritz Firsching (Mar 11 2021 at 14:42):

I wonder if there are simpler ways of doing the following two lemmas of if there is some code for it which I overlooked:

import tactic
import ring_theory.power_series.basic
import number_theory.bernoulli

open power_series
open nat
open ring_hom

open polynomial (aeval)

variables {A : Type*} [comm_ring A] [algebra ℚ A]

lemma aux_eval (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
begin
dsimp [polynomial.aeval_def],
unfold polynomial.eval,
delta eval₂,
simp only [← ring_hom.map_sum, ring_hom.id_apply],
rw [finsupp.sum, finsupp.sum],
simp only [ring_hom.map_sum, ring_hom.map_pow, ring_hom.map_mul],
end

lemma aux_smul (q r : ℚ):
q • (algebra_map ℚ A) r = (algebra_map ℚ A) (q * r) :=
begin
simp only [ring_hom.map_mul],
rw [←algebra.smul_def, algebra.smul_def, algebra.commutes],
end


(see #6641 for context)

#### Eric Wieser (Mar 11 2021 at 14:50):

Can you make that a #mwe with imports?

sure, done

#### Eric Wieser (Mar 11 2021 at 14:56):

lemma aux_eval {A : Type*} [semiring A] [algebra ℚ A] (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
begin
change aeval (algebra.of_id ℚ A t) p = _,
rw aeval_alg_hom,
refl,
end


#### Moritz Firsching (Mar 11 2021 at 14:59):

That's already much nicer!

#### Eric Wieser (Mar 11 2021 at 14:59):

Or as a one-line proof with some noise

section

-- this instance causes conflicts in the proof
local attribute [-instance] rat.algebra_rat

lemma aux_eval {A : Type*} [semiring A] [algebra ℚ A] (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
aeval_alg_hom_apply (algebra.of_id ℚ A) t p

end


The key observation here is that algebra_map has a corresponding alg_hom, which you can then use docs#polynomial.aeval_alg_hom_apply on

#### Moritz Firsching (Mar 11 2021 at 15:04):

Would it be useful to have that lemma somewhere as aeval_map_eq_map_eval or should I use it in my proof only (I would probably not give it a name then, now that it is so short)?

(deleted)

#### Eric Wieser (Mar 11 2021 at 15:08):

I think aeval_algebra_map_apply would be a reasonable lemma with that definition

#### Eric Wieser (Mar 11 2021 at 15:08):

Except obviously generalizing over  ℚ

#### Eric Wieser (Mar 11 2021 at 15:09):

Which also removes the need for hiding the annoying instanec

#### Eric Wieser (Mar 11 2021 at 15:12):

second lemma is slightly shorter as:

lemma smul_algebra_map (q r : R) :
q • algebra_map R A r = algebra_map R A (q * r) :=
by rw [algebra.smul_def, ring_hom.map_mul]


#### Moritz Firsching (Mar 11 2021 at 19:32):

Thanks for the help, @Eric Wieser ! I have inlined aux_eval, not sure if this would be worthwhile to add to mathlib.
Made a separate pr for the first lemma 6649

Last updated: May 07 2021 at 22:14 UTC