compatibility of maps and presented groups

Stream: mathlib4

[Noah G. Singer]

Hi, does anyone happen to know an idiomatic proof of the following theorem or similar:

example (α β : Type) (S : Set (FreeGroup α)) (T : Set (FreeGroup β)) (f : α → β) (r : FreeGroup α):
  (PresentedGroup.mk T (FreeGroup.map f r)) = (FreeGroup.lift (PresentedGroup.of ∘ f)) r

I am trying to use this together with PresentedGroup.toGroup to show that you can get a homomorphism between two presented groups mapping generators to generators as long as the image of every relation is trivial.

[Notification Bot]

Julian Berman has marked this topic as resolved.

[Notification Bot]

Noah G. Singer has marked this topic as unresolved.

[Noah G. Singer]

(deleted)

[Noah G. Singer]

Actually, I have a proof. I will pr it eventually. But, I’ll refer back to check that it’s not already present somewhere else

[Patrick Massot]

@Noah G. Singer This issue is that Lean has trouble recognizing the group morphism composition on the left-hand side, so it needs help. For instance

example (α β : Type) (T : Set (FreeGroup β)) (f : α → β) (r : FreeGroup α):
    PresentedGroup.mk T (FreeGroup.map f r) = FreeGroup.lift (PresentedGroup.of ∘ f) r :=
  FreeGroup.lift.unique (PresentedGroup.mk T |>.comp <| FreeGroup.map f) fun _ ↦ rfl

[Patrick Massot]

I agree this lemma should be somewhere. If it isn’t then adding it would be nice.

[Patrick Massot]

To be clear, the method I used was:

• try apply?. See nothing where I was expecting something like uniqueness in the universal property of free groups.
• recognize the issue is that Lean doesn’t see a group morphism on LHS.
• type change (PresentedGroup.mk T).comp (FreeGroup.map f) r = _ and retry apply?