Zulip Chat Archive

Stream: general

Topic: coe as monoid_hom


view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 28 2020 at 17:00):

:= coe_N_Z.map_prod _?

view this post on Zulip Eric Wieser (Nov 28 2020 at 17:01):

Possibly more underscores

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 17:06):

To go from to we have nat.cast_ring_hom ℤ.

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 17:06):

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

view this post on Zulip Adam Topaz (Nov 28 2020 at 17:07):

I think he wants the multiplicative monoid hom

view this post on Zulip Adam Topaz (Nov 28 2020 at 17:07):

So docs#nat.cast_monoid_hom ?

view this post on Zulip Adam Topaz (Nov 28 2020 at 17:09):

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

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 17:10):

(nat.cast_ring_hom ℤ).to_monoid_hom should work

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 17:10):

Ops, I didn't see you answer

view this post on Zulip 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 ...

view this post on Zulip Eric Wieser (Nov 28 2020 at 17:47):

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

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 17:59):

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

view this post on Zulip 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)

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 18:06):

Ah sorry, it was at beginning of the conversation

view this post on Zulip 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...

view this post on Zulip 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:

view this post on Zulip Paul van Wamelen (Nov 28 2020 at 18:14):

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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 18:18):

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

view this post on Zulip 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 : β →* γ).

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 18:51):

Presumably one is deprecated, that's another difference

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 28 2020 at 19:07):

what are the types?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 28 2020 at 20:52):

(I think)

view this post on Zulip 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