coe as monoid_hom

Stream: general

[Paul van Wamelen]

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]

:= coe_N_Z.map_prod _?

[Eric Wieser]

Possibly more underscores

[Adam Topaz]

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]

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]

To go from ℕ to ℤ we have nat.cast_ring_hom ℤ.

[Riccardo Brasca]

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

[Adam Topaz]

I think he wants the multiplicative monoid hom

[Adam Topaz]

So docs#nat.cast_monoid_hom ?

[Adam Topaz]

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

[Riccardo Brasca]

(nat.cast_ring_hom ℤ).to_monoid_hom should work

[Riccardo Brasca]

Ops, I didn't see you answer

[Paul van Wamelen]

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]

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

[Paul van Wamelen]

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]

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]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

Ah sorry, it was at beginning of the conversation

[Paul van Wamelen]

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]

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]

But surely somehow using (nat.cast_ring_hom ℤ).to_monoid_hom would be nicer, right?

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Paul van Wamelen]

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]

What happens if you drop the to_monoid_hom? I think ring_hom.map_prod exists too

[Kevin Buzzard]

Presumably one is deprecated, that's another difference

[Paul van Wamelen]

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

[Mario Carneiro]

what are the types?

[Adam Topaz]

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]

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

[Kevin Buzzard]

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]

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]

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]

(I think)

[Adam Topaz]

And it looks like the example itself can be solved with by simp as well :)