Zulip Chat Archive

Stream: Is there code for X?

Topic: poly (a)eval and algebra maps


view this post on Zulip 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)

view this post on Zulip Eric Wieser (Mar 11 2021 at 14:50):

Can you make that a #mwe with imports?

view this post on Zulip Moritz Firsching (Mar 11 2021 at 14:55):

sure, done

view this post on Zulip 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

view this post on Zulip Moritz Firsching (Mar 11 2021 at 14:59):

That's already much nicer!

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip Moritz Firsching (Mar 11 2021 at 15:06):

(deleted)

view this post on Zulip Eric Wieser (Mar 11 2021 at 15:08):

I think aeval_algebra_map_apply would be a reasonable lemma with that definition

view this post on Zulip Eric Wieser (Mar 11 2021 at 15:08):

Except obviously generalizing over

view this post on Zulip Eric Wieser (Mar 11 2021 at 15:09):

Which also removes the need for hiding the annoying instanec

view this post on Zulip 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]

view this post on Zulip 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