Monoid hom preserves identity

Stream: Is there code for X?

[Oliver Nash]

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?

[Adam Topaz]

docs#monoid_hom.map_one

[Oliver Nash]

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

[Adam Topaz]

Oh oops

[Adam Topaz]

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

[Oliver Nash]

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.

[Adam Topaz]

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

[Oliver Nash]

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

[Oliver Nash]

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

[Eric Wieser]

docs#monoid_hom.mk'

[Eric Wieser]

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

[Adam Topaz]

This assumes you have a group...

[Adam Topaz]

And Oliver wants to work with a cancellative monoid

[Eric Wieser]

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.

[Adam Topaz]

groups are always cancellative since you have multiplicative inverses

[Eric Wieser]

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

[Adam Topaz]

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

[Oliver Nash]

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

[Oliver Nash]

Thanks.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

left is usually the default

[Eric Wieser]

I suppose mk'' is always an option for right