[Merged by Bors] - refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in AddCommGrp

[smorel394]

The old version of this file has a remark saying "TODO: In fact, in AddCommGrp there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead)."

This PR does precisely this (choosing the "instead" option). In fact, given a functor F : J ⥤ AddCommGrp.{w}, it constructs a candidate for the colimit of F as a quotient of DFinsupp (fun j ↦ F.obj j), without any smallness assumptions on J. It then proves that this quotient is a colimit of F if it is w-small, then deduces that AddCommGrp.{w} has all small colimits.

---

[github-actions]

PR summary 551492e1a7

Import changes exceeding 2%

%	File
+18.09%	Mathlib.Algebra.Category.Grp.Colimits

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.Grp.Colimits	691	816	+125 (+18.09%)

Import changes for all files

Files	Import difference
76 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.Algebra.Category.Grp.AB Mathlib.Condensed.Limits Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Condensed.Light.Explicit Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Algebra.Category.Grp.Abelian Mathlib.Condensed.AB Mathlib.Condensed.Explicit Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Condensed.Module Mathlib.Condensed.Discrete.Characterization Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.RepresentationTheory.Rep Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Condensed.Solid Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Condensed.Discrete.Module Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.NumberTheory.MulChar.Duality Mathlib.Condensed.Light.Epi Mathlib.RepresentationTheory.Character Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Module.PID Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.Grp.Images Mathlib.Condensed.Light.AB Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Condensed.Light.Limits Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.FDRep Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.Condensed.Light.Module Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Condensed.Epi Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Category.ModuleCat.Free Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	1
Mathlib.Algebra.Category.ModuleCat.FilteredColimits	35
Mathlib.Algebra.Category.ModuleCat.Colimits	98
Mathlib.Algebra.Category.Grp.Colimits	125
Mathlib.Data.DFinsupp.Small (new file)	458

---

Declarations diff

+ DFinsupp.small
+ Quot
+ Quot.addMonoidHom_ext
+ Quot.desc
+ Quot.desc_colimitCocone
+ Quot.desc_toCocone_desc
+ Quot.desc_toCocone_desc_app
+ Quot.map_ι
+ Quot.ι
+ Quot.ι_desc
+ Relations
+ hasColimit_of_small_quot
+ instance (priority := 1300) hasColimitsOfSize [UnivLE.{u, w}] :
+ instance [DecidableEq J] : AddCommGroup (Quot F)
+ instance [DecidableEq J] [Small.{w} J] : Small.{w} (Quot F)
+ isColimit_of_bijective_desc
+ on
+ toCocone
- ColimitType
- ColimitTypeInhabited
- Prequotient
- Relation
- coconeFun
- coconeMorphism
- cocone_naturality
- cocone_naturality_components
- colimit
- colimitSetoid
- descFun
- descFunLift
- descMorphism
- hasColimits
- hasColimitsOfSize
- instance : Add (ColimitType.{w} F)
- instance : AddCommGroup (ColimitType.{w} F)
- instance : HasColimitsOfSize.{0, 0} (AddCommGrp.{u}) := hasColimitsOfSize.{u, 0, 0}
- instance : HasColimitsOfSize.{u, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{v}
- instance : HasColimitsOfSize.{u, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
- instance : Inhabited (Prequotient.{w} F)
- instance : Neg (ColimitType.{w} F)
- instance : Zero (ColimitType.{w} F)
- quot_add
- quot_neg
- quot_zero

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) = (2.56, 0.00)

Current number	Change	Type
4824	-2	porting notes
1518	4	erw

Current commit 551492e1a7
Reference commit 0f18102487

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).

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit 75fa8cf.
There were significant changes against commit e6514e0:

  Benchmark                                              Metric         Change
  ============================================================================
- ~Mathlib.Algebra.Category.Grp.Colimits                 instructions   126.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian   instructions   -80.1%
+ ~Mathlib.Condensed.Discrete.Module                     instructions   -16.7%

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style