feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups

[smorel394]

If F : J ⥤ AddCommGrp.{w} is a functor, we show that F admits a colimit if and only
if Colimits.Quot F (the quotient of the direct sum of the commutative groups F.obj j
by the relations given by the morphisms in the diagram) is w-small.

• depends on: [Merged by Bors] - chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version #20416
• depends on: feat(Algebra/Module/CharacterModule): a morphism of abelian groups is bijective if and only if its dual is bijective #20512

---

[github-actions]

PR summary 7e8c8b27d9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.Grp.LargeColimits (new file)	1486

---

Declarations diff

+ dual_bijective_iff_bijective
+ dual_comp
+ dual_injective_iff_surjective
+ dual_injective_of_surjective
+ dual_zero
+ hasColimit_iff_small_quot
+ isColimit_iff_bijective_desc
+ surjective_of_dual_injective

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1457	1	erw

Current commit 7e8c8b27d9
Reference commit 57f8888c4b

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version #20416
• feat(Algebra/Module/CharacterModule): a morphism of abelian groups is bijective if and only if its dual is bijective #20512
  By Dependent Issues (🤖). Happy coding!

[joelriou]

Instead of "Big", I would suggest "Large", because it matches more the notions of "SmallCategory" and "LargeCategory" that we have.