Lean4
/-- The categorical cokernel of a morphism in `AddCommGrpCat`
agrees with the usual group-theoretical quotient.
-/
noncomputable def cokernelIsoQuotient {G H : AddCommGrpCat.{u}} (f : G ⟶ H) :
cokernel f ≅ AddCommGrpCat.of (H ⧸ AddMonoidHom.range f.hom)
where
hom :=
cokernel.desc f (ofHom (mk' _)) <| by
ext x
simp
inv :=
ofHom <|
QuotientAddGroup.lift _ (cokernel.π f).hom <| by
rintro _ ⟨x, rfl⟩
exact cokernel.condition_apply f x
hom_inv_id := by
refine coequalizer.hom_ext ?_
simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]
rfl
inv_hom_id := by
ext x
dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk', Function.comp_apply,
AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id]
exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _
