Add the category of finitely generated groups

[ScriptRaccoon]

This PR adds the category of finitely generated groups Grp_fg. We already have several variants (finite groups, finitely generated abelian groups, countable groups, finitely generated free abelian groups), but this one was missing.

The first draft of the proofs has been generated automatically with Claude Code from an empty Grp_fg.yaml file using the skill structure-proofs added in #394. After working for 12 minutes, almost all properties have been decided; only 3 have remained, which appear more difficult ($\aleph_1$-cofiltered limits, $\aleph_1$-filtered colimits, $\aleph_1$-accessible).

The generated proofs had a style very similar to the other proofs in the project. In any case, according to the AI guidelines, these proofs need to be checked by a human reviewer, which I did. In the process, the proofs and the skill have been improved. They were already good before my review, but now they are close to being perfect.

Later, Claude also found proofs that $\aleph_1$-cofiltered limits and $\aleph_1$-filtered colimits do not exist (≈ 20 minutes each). I have checked them thoroughly, and they have been revised multiple times. Hence, all properties are decided now.

Moreover, a content page content/fg-groups-aleph1-filtered-colimits.md has been added that proves the widely used result that a regular epimorphism that has a kernel pair is the coequalizer of that kernel pair.