homs vs. functions

Stream: new members

[Joachim Breitner]

More beginner questions, hope that’s ok. My goal is

⇑h2 ∘ ⇑h1 = id

but what I really want (to apply suitable lemmas) is what I can’t express better than

monoid_hom.comp h2 h1 = monoid_hom.id G

How do I go about this? Is there a way to apply this lemma (is_free_group.hom_ext) to the above goal and have lean somehow figure out that both sides are indeed homs?

[Yakov Pechersky]

mathlib has the style tendency to not use pointfree (comp) lemmas, but use fully applied lemmas. so often such goals are solved by using an extensionality lemma (or tactic) first

[Yakov Pechersky]

So in this case, you might have a proof of that lemma, let's say named H, and use congr_fun H _

[Yakov Pechersky]

A #mwe always helps to give concrete examples

[Anne Baanen]

I hope we already have docs#monoid_hom.coe_comp and docs#monoid_hom.coe_id (EDIT: no coe_id unfortunately), then you could do it as follows:

[Anne Baanen]

import algebra.group.hom

variables {M N : Type*} [monoid M] [monoid N]

@[simp] lemma monoid_hom.coe_id : ((monoid_hom.id M) : M → M) = id := rfl

example (h1 : M →* N) (h2 : N →* M) (h : monoid_hom.comp h2 h1 = monoid_hom.id M) :
  (h2 ∘ h1 : M → M) = id :=
by rw [← monoid_hom.coe_comp, ← monoid_hom.coe_id, h]

[Anne Baanen]

Now in fact coe_comp and coe_id are true by definition, so you can actually cheat a bit and say:

example (h1 : M →* N) (h2 : N →* M) (h : monoid_hom.comp h2 h1 = monoid_hom.id M) :
  (h2 ∘ h1 : M → M) = id :=
congr_arg (coe_fn : (M →* M) → (M → M)) h

where coe_fn is the name of the double uparrow ⇑ implicitly converting a hom to a function.

[Joachim Breitner]

That proof term works, thanks. At least the sorry is gone, and maybe I’ll learn how to do it more pretty later :)