Zulip Chat Archive

Stream: Is there code for X?

Topic: eval_zero is a bundled semiring hom


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!

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.

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.

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

Johan Commelin (Nov 27 2020 at 11:14):

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

Eric Wieser (Nov 27 2020 at 11:14):

Is docs#polynomial.aeval_C close?

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

Eric Wieser (Nov 27 2020 at 11:15):

(deleted)

Damiano Testa (Nov 27 2020 at 11:15):

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

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?

Eric Wieser (Nov 27 2020 at 11:18):

Is the lemma you want docs#polynomial.eval_C?

Damiano Testa (Nov 27 2020 at 11:20):

Eric Wieser said:

Is the lemma you want docs#eval_C?

I believe so! Thanks!

Damiano Testa (Nov 27 2020 at 11:20):

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

Eric Wieser (Nov 27 2020 at 11:20):

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

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?

Eric Wieser (Nov 27 2020 at 11:26):

funext $ λ _, eval_C gives the proof you need

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!

Eric Wieser (Nov 27 2020 at 11:32):

by {ext, simp} would also close the goal

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"

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.

Yury G. Kudryashov (Nov 27 2020 at 18:13):

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

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?

Johan Commelin (Nov 27 2020 at 18:59):

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

Johan Commelin (Nov 27 2020 at 19:00):

But it's an alg_hom

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

Johan Commelin (Nov 27 2020 at 19:05):

You mean: unbundled homs?

Johan Commelin (Nov 27 2020 at 19:05):

I severely hope the answer will be yes

Kevin Buzzard (Nov 27 2020 at 19:10):

oh yeah that's exactly what I mean!

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: Dec 20 2023 at 11:08 UTC