# Zulip Chat Archive

## Stream: general

### Topic: coe as monoid_hom

#### Paul van Wamelen (Nov 28 2020 at 16:55):

I needed `small_lemma`

below in a proof. I finally got it done, but it doesn't feel right. Is there a better way than:

```
import algebra.big_operators
import data.int.cast
universe u
variables {α : Type u} [fintype α]
open_locale big_operators
def coe_N_Z : ℕ →* ℤ :=
begin
refine {to_fun := _, map_one' := _, map_mul' := _},
exact (λ a, (a : ℤ)),
simp,
exact int.coe_nat_mul,
end
lemma small_lemma (t : α → ℕ) : (↑∏ i, t i : ℤ) = ∏ i, (↑(t i) : ℤ) :=
begin
apply monoid_hom.map_prod coe_N_Z,
end
```

#### Eric Wieser (Nov 28 2020 at 17:00):

:= coe_N_Z.map_prod _?

#### Eric Wieser (Nov 28 2020 at 17:01):

Possibly more underscores

#### Adam Topaz (Nov 28 2020 at 17:02):

One note: it's usually bad practice to make definitions in tactic mode. I usually put an underscore after := and use a hole command to generate a skeleton for the structure, and go from there

#### Adam Topaz (Nov 28 2020 at 17:03):

Also I'm sure the definition of coe_N_Z exists in mathlib, but we probably have a semiring hom which you can restrict to a monoid hom

#### Riccardo Brasca (Nov 28 2020 at 17:06):

To go from `ℕ`

to `ℤ`

we have `nat.cast_ring_hom ℤ`

.

#### Riccardo Brasca (Nov 28 2020 at 17:06):

If you want directly the monoid hom there is `nat.cast_add_monoid_hom`

.

#### Adam Topaz (Nov 28 2020 at 17:07):

I think he wants the multiplicative monoid hom

#### Adam Topaz (Nov 28 2020 at 17:07):

#### Adam Topaz (Nov 28 2020 at 17:09):

~~You can use ~~ see the message below`nat.cast_ring_hom.to_monoid_hom`

I guess...

#### Riccardo Brasca (Nov 28 2020 at 17:10):

`(nat.cast_ring_hom ℤ).to_monoid_hom`

should work

#### Riccardo Brasca (Nov 28 2020 at 17:10):

Ops, I didn't see you answer

#### Paul van Wamelen (Nov 28 2020 at 17:41):

Thanks, `nat.cast_ring_hom`

and `to_monoid_hom`

was what I was looking for!

So this

```
lemma small_lemma (t : α → ℕ) : (↑∏ i, t i : ℤ) = ∏ i, (↑(t i) : ℤ) :=
begin
exact monoid_hom.map_prod (nat.cast_ring_hom ℤ).to_monoid_hom t finset.univ,
end
```

should work, right? But it gives an error message involving `⇑`

...

#### Eric Wieser (Nov 28 2020 at 17:47):

Can you tell us more than one character of that error message?

#### Paul van Wamelen (Nov 28 2020 at 17:54):

```
invalid type ascription, term has type
⇑((nat.cast_ring_hom ℤ).to_monoid_hom) (∏ (x : α), t x) =
∏ (x : α), ⇑((nat.cast_ring_hom ℤ).to_monoid_hom) (t x)
but is expected to have type
↑∏ (i : α), t i = ∏ (i : α), ↑(t i)
```

#### Adam Topaz (Nov 28 2020 at 17:57):

I think lean can't unify the evaluation of this with coe. (I'm on mobile, so I can't check unfortunately.)

#### Paul van Wamelen (Nov 28 2020 at 17:57):

```
begin
convert monoid_hom.map_prod (nat.cast_ring_hom ℤ).to_monoid_hom t finset.univ,
swap, simp,
end
```

leaves me with `⊢ coe_base = nat.cast_coe`

#### Riccardo Brasca (Nov 28 2020 at 17:59):

You should give a minimal working example, as in https://leanprover-community.github.io/mwe.html

#### Riccardo Brasca (Nov 28 2020 at 18:00):

Meaning that people can just copy/paste your code (in what you wrote some imports are missing)

#### Riccardo Brasca (Nov 28 2020 at 18:06):

Ah sorry, it was at beginning of the conversation

#### Paul van Wamelen (Nov 28 2020 at 18:08):

This

```
lemma small_lemma3 (t : α → ℕ) : (↑∏ i, t i : ℤ) = ∏ i, (↑(t i) : ℤ) :=
begin
exact monoid_hom.map_prod
{to_fun := λ (a : ℕ), (a :ℤ), map_one' := int.coe_nat_one, map_mul' := int.coe_nat_mul}
t finset.univ
end
```

works...

#### Paul van Wamelen (Nov 28 2020 at 18:11):

Or

```
lemma small_lemma (t : α → ℕ) : (↑∏ i, t i : ℤ) = ∏ i, (↑(t i) : ℤ) := monoid_hom.map_prod {to_fun := λ (a : ℕ), (a :ℤ), map_one' := int.coe_nat_one, map_mul' := int.coe_nat_mul} t finset.univ
```

is (nearly) a one-liner :smile:

#### Paul van Wamelen (Nov 28 2020 at 18:14):

But surely somehow using `(nat.cast_ring_hom ℤ).to_monoid_hom`

would be nicer, right?

#### Riccardo Brasca (Nov 28 2020 at 18:18):

If what you want is that a monoids homomorphism commutes with finite products this is already in mathlib, `finset.prod_hom`

#### Riccardo Brasca (Nov 28 2020 at 18:18):

But if you just want t practice your proof works :)

#### Paul van Wamelen (Nov 28 2020 at 18:44):

Wow, `finset.prod`

and `monoid_hom.map_prod`

are almost identical. The difference seems to be `(g : β → γ) [is_monoid_hom g]`

vs. `(g : β →* γ)`

.

#### Eric Wieser (Nov 28 2020 at 18:47):

What happens if you drop the `to_monoid_hom`

? I think ring_hom.map_prod exists too

#### Kevin Buzzard (Nov 28 2020 at 18:51):

Presumably one is deprecated, that's another difference

#### Paul van Wamelen (Nov 28 2020 at 18:54):

`ring_hom.map_prod`

does indeed exist! Unfortunately it leads the exact same goal: `⊢ coe_base = nat.cast_coe`

#### Mario Carneiro (Nov 28 2020 at 19:07):

what are the types?

#### Adam Topaz (Nov 28 2020 at 20:08):

Looks like `nat.cast_ring_hom \Z n`

is not defeq to the coercion of `n`

from nat to the ring:

```
example {n : ℕ} : (nat.cast_ring_hom ℤ) n = n := rfl -- fails
```

#### Kevin Buzzard (Nov 28 2020 at 20:28):

The coercion from nat to int is "special" :-/ It's one of the constructors, for some sort of computer science reason.

#### Kevin Buzzard (Nov 28 2020 at 20:42):

Here's a nice way to do it: I'm a bit surprised I couldn't find this stuff in mathlib.

```
import tactic
theorem nat.add_monoid_hom_unique {R : Type} [semiring R] (f g : ℕ →+* R) : f = g :=
begin
suffices : (f : ℕ →+ R) = g,
simp [this],
ext,
show f 1 = g 1,
rw [f.map_one, g.map_one]
end
theorem nat.add_monoid_hom_unique' {R : Type} [semiring R] (f g : ℕ →+* R) (n : ℕ) :
f n = g n :=
begin
rw nat.add_monoid_hom_unique f g,
end
def int.of_nat' : ℕ →+* ℤ :=
by refine_struct { to_fun := int.of_nat}; simp
example {n : ℕ} : (nat.cast_ring_hom ℤ) n = n :=
begin
show _ = int.of_nat' n,
apply nat.add_monoid_hom_unique'
end
```

#### Kevin Buzzard (Nov 28 2020 at 20:44):

The `ext`

in the first theorem applies `add_monoid_hom.ext_nat : ∀ {A : Type} [_inst_1 : add_monoid A] {f g : ℕ →+ A}, ⇑f 1 = ⇑g 1 → f = g`

. It would be cool if `nat.add_monoid_hom_unique`

were tagged `ext`

:D

#### Adam Topaz (Nov 28 2020 at 20:51):

mathlib has a subsingleton instance for semiring morphisms out of nat, so `nat.add_monoid_hom_unique`

can be solved with `by simp`

.

#### Adam Topaz (Nov 28 2020 at 20:52):

(I think)

#### Adam Topaz (Nov 28 2020 at 20:53):

And it looks like the example itself can be solved with `by simp`

as well :)

Last updated: May 09 2021 at 18:17 UTC