## 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:09):

You can use nat.cast_ring_hom.to_monoid_hom I guess... see the message below

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

(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