every monomorphism of Grps is a equalizer

Stream: new members

[Noah Anderson]

Hi there! How can I prove "every monomorphism of Grps is the equalizer of two homomorphisms" in Lean? This post introduced multiple solutions to the problem.

I've tried to follow the "distinguished element + permutation group" proof (illustrated in the "added" part of the problem description), but don't know how to implement the idea of this "distinguished element".

Also, I looked into the solution via free products with amalgamation in Paul Taylor's answer, but I find the idea of "length" hard to formalize?

[Edward van de Meent]

I feel like the "distinguished element" approach may be talking about something like docs#WithZero ?

[Noah Anderson]

forgive me, I am not familiar with WithZero
1.png
Like, here I need a group action acting differently on elements of cosets and the zero, how to define such thing?

[Eric Paul]

This may not be the right way to do it for your problem, but here is a basic example of adding a new element to something and then defining a map on it.

import Mathlib

variable [Group H] {K : Subgroup H}
-- The left cosets of K
#check H ⧸ K
-- A new type where every element is either a left coset of K or a new element `()`
def X := H ⧸ K ⊕ Unit
-- the new element of `X`
#check (.inr () : X)
-- the old elements:
-- maps each element of `H` to its coset as an element of `X`
#check fun (h : H) => (.inl ⟦h⟧ : X)

open Classical in
-- This swaps the coset of `1` with the new element and fixes everything else
noncomputable def map : X (H := H) (K := K) → X (H := H) (K := K)
  | .inl x =>
    if x = ⟦1⟧ then
      .inr ()
    else
      .inl x
  | .inr () => .inl ⟦1⟧

[Noah Anderson]

Ah yes! It works, thanks