Zulip Chat Archive

Stream: Is there code for X?

Topic: eval_zero is a bundled semiring hom


view this post on Zulip Damiano Testa (Nov 27 2020 at 11:09):

Dear All,

I would like to use the following two facts.

  1. If R is a commutative (semi-)ring, then, for each r : R, the evaluation map eval r : R →+* polynomial R exists as a bundled homomorphism.
  2. The composition eval r ∘ C : R →+* R is id again, as a bundled homomorphism.

Are they in Lean? I can find many of these in their unbundled versions, but not the bundled ones.

I am really only interested in evaluating at 0, so this would be enough.

Thanks!

view this post on Zulip Anne Baanen (Nov 27 2020 at 11:13):

You can use aeval x, which is an alg_hom from the R-algebra polynomial R to R, i.e. a ring homomorphism which preserves the image of C : R -> polynomial R.

view this post on Zulip Johan Commelin (Nov 27 2020 at 11:13):

Evaluation at 0 is constant_coeff, right? It exists for mv_polynomial, but maybe not for polynomial.

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:14):

In case you want something like a #mwe, I have started as follows:

import data.polynomial.eval

open polynomial

noncomputable def eval0 {R : Type*} [comm_semiring R] : polynomial R →+* R :=
λ p, eval 0 p, eval_one, (λ _ _, eval_mul), eval_zero, (λ _ _, eval_add)⟩

view this post on Zulip Johan Commelin (Nov 27 2020 at 11:14):

It would be good to add it. Should be a not so big PR

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:14):

Is docs#polynomial.aeval_C close?

view this post on Zulip Johan Commelin (Nov 27 2020 at 11:15):

I would prefer calling it constant_coeff, and defining it in terms of coeff, but then have a lemma that relates it to (a)eval 0

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:15):

(deleted)

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:15):

Thanks! I will take a look at aeval, aeval_C and constant_coeff!

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:17):

So, is the consensus then that eval 0 should be singled out and be called constant_coeff?

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:18):

Is the lemma you want docs#polynomial.eval_C?

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:20):

Eric Wieser said:

Is the lemma you want docs#eval_C?

I believe so! Thanks!

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:20):

(Thanks for correcting the link, I was going to mention it!)

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:20):

I think @Yury G. Kudryashov was looking into bundling polynomial.eval

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:25):

Is there a standard way to go from the statement docs#polynomial.eval_C
(@[simp] lemma eval_C : (C a).eval x = a := eval₂_C _ _)
to the assertion that the composition eval r ∘ C equals id?

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:26):

funext $ λ _, eval_C gives the proof you need

view this post on Zulip Damiano Testa (Nov 27 2020 at 11:31):

@Eric Wieser Thank you very much! I did not know what funext was!

This might also bypass the issue that I had with bundled things: I had some trouble communicating with Lean, but I may now try more extensively with funext!

view this post on Zulip Eric Wieser (Nov 27 2020 at 11:32):

by {ext, simp} would also close the goal

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 11:43):

Computer scientists make a lot of fuss about functional extensionality, but this fuss has nothing to do with what we're doing. Extensionality is the general principle that two objects are equal if they're made of the same stuff. For example the axiom of extensionality in ZFC says that two sets are equal if and only if they have the same elements. In Lean this idea is taken much further; if you have two structures (for example subgroups, each defined as a subset plus some proofs) then the ext tactic should reduce a goal of H = K to "for all x, x in H <-> x in K"

view this post on Zulip Yury G. Kudryashov (Nov 27 2020 at 18:10):

I have a branch with bundled polynomial.eval but it doesn't compile at the moment.

view this post on Zulip Yury G. Kudryashov (Nov 27 2020 at 18:13):

I'm going to split it into smaller pieces and PR during the next week.

view this post on Zulip Devon Tuma (Nov 27 2020 at 18:52):

I've been using eval₂_ring_hom (ring_hom.id R) r for evaluation at r as a ring_hom, is there some reason to avoid this that I'm not aware of?

view this post on Zulip Johan Commelin (Nov 27 2020 at 18:59):

It's somewhat long, but otherwise should be fine. I think aeval is a lot shorter (-;

view this post on Zulip Johan Commelin (Nov 27 2020 at 19:00):

But it's an alg_hom

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 19:04):

In Lean 4 will be able to work like mathematicians, and not care if it's a function or a ring hom or a monoid hom or an algebra hom? [he asked, fully expecting the answer "no"]

view this post on Zulip Johan Commelin (Nov 27 2020 at 19:05):

You mean: unbundled homs?

view this post on Zulip Johan Commelin (Nov 27 2020 at 19:05):

I severely hope the answer will be yes

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 19:10):

oh yeah that's exactly what I mean!

view this post on Zulip Eric Wieser (Nov 27 2020 at 19:10):

Doesn't docs#polynomial.eval₂_ring_hom have a sdifferent signature to docs#polynomial.aeval?


Last updated: May 16 2021 at 05:21 UTC