Zulip Chat Archive

Stream: Is there code for X?

Topic: Monoid hom preserves identity


view this post on Zulip Oliver Nash (Nov 09 2020 at 15:10):

Surely I'm being dumb but I can't find the following:

@[to_additive]
lemma monoid_map_mul_one {G H : Type*} [monoid G] [left_cancel_monoid H]
  (f : G  H) (h :  x y, f (x * y) = (f x) * (f y)) :
  f 1 = 1 :=
suffices (f 1) * (f 1) = (f 1) * 1, by exact mul_left_cancel this,
by rw [ h, mul_one, mul_one]

Is it possible it doesn't exist?

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:11):

docs#monoid_hom.map_one

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:11):

Thank you but note that my f is just a raw function, and not a monoid hom.

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:11):

Oh oops

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:12):

Oh I see... The group theory folder might have something along these lines

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:13):

Yeah, it must be there. I poked around unsuccessfully there for a while and then got lazy and decided to ask here :wink: I'll look again.

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:14):

I put map_one_of_ into the API doc search, and the little :octopus: didn't find anything that looks reasonable

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:16):

Good thinking, I guess perhaps it could be missing. Thanks.

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:16):

(I should get back to my day job now.)

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:22):

docs#monoid_hom.mk'

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:23):

So here, (monoid_hom.mk' f h).map_one I think is your proof

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:27):

This assumes you have a group...

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:27):

And Oliver wants to work with a cancellative monoid

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:31):

Oh, I missed that. Am I right in thinking that given a group you can always obtain a left_cancel_monoid? Perhaps the solution is to weaken the assumptions on mk' and use that proof instead.

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:33):

groups are always cancellative since you have multiplicative inverses

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:33):

Looks like docs#group.to_left_cancel_monoid is also missing, and only the weaker docs#group.to_left_cancel_semigroup exists

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:33):

If you look at the proof of this thing, it uses mul_self_iff_eq_one which needs a group

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:33):

I actually only need it for a group I was just being ridiculous and stating the weaker form.

view this post on Zulip Oliver Nash (Nov 09 2020 at 15:33):

Thanks.

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:34):

It might still be worth replacing the definition of mk' to use your weaker and more ridiculous proof

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:36):

Regarding my above comment - groups turn into left_cancel_monoids with group.to_cancel_monoid.to_left_cancel_monoid, which typeclass inference ought to be able to follow

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:44):

I guess there's still the question of whether to use right or left in mk'...

view this post on Zulip Adam Topaz (Nov 09 2020 at 15:44):

left is usually the default

view this post on Zulip Eric Wieser (Nov 09 2020 at 15:45):

I suppose mk'' is always an option for right


Last updated: May 16 2021 at 05:21 UTC