# 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.

- 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*. - 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 *un*bundled 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: May 16 2021 at 05:21 UTC