poly (a)eval and algebra maps

Stream: Is there code for X?

[Moritz Firsching]

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]

Can you make that a #mwe with imports?

[Moritz Firsching]

sure, done

[Eric Wieser]

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]

That's already much nicer!

[Eric Wieser]

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]

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)?

[Moritz Firsching]

(deleted)

[Eric Wieser]

I think aeval_algebra_map_apply would be a reasonable lemma with that definition

[Eric Wieser]

Except obviously generalizing over ℚ

[Eric Wieser]

Which also removes the need for hiding the annoying instanec

[Eric Wieser]

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]

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