eval_zero is a bundled semiring hom

Stream: Is there code for X?

[Damiano Testa]

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!

[Anne Baanen]

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.

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Eric Wieser]

Is docs#polynomial.aeval_C close?

[Johan Commelin]

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

[Eric Wieser]

(deleted)

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

Is the lemma you want docs#polynomial.eval_C?

[Damiano Testa]

Eric Wieser said:

Is the lemma you want docs#eval_C?

I believe so! Thanks!

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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?

[Eric Wieser]

funext $ λ _, eval_C gives the proof you need

[Damiano Testa]

@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!

[Eric Wieser]

by {ext, simp} would also close the goal

[Kevin Buzzard]

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"

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Devon Tuma]

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?

[Johan Commelin]

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

[Johan Commelin]

But it's an alg_hom

[Kevin Buzzard]

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"]

[Johan Commelin]

You mean: unbundled homs?

[Johan Commelin]

I severely hope the answer will be yes

[Kevin Buzzard]

oh yeah that's exactly what I mean!

[Eric Wieser]

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