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.

Meanwhile, Claude also found a proof that $\aleph_1$-cofiltered limits do not exist (≈ 20 minutes). I have checked it thoroughly. It uses a non-trivial finitely generated group that is isomorphic to its own square.

---

TODO. decide the remaining properties for finitely generated groups:

• ℵ₁-filtered colimits (no; proof has already been generated, needs to be checked)
• ℵ₁-accessible (follows)