feat(CategoryTheory): AB5 and AB4* for condensed modules

[dagurtomas]

---

• depends on: feat(Algebra/Category): the category of abelian groups satisfies AB4* #19912
• depends on: feat(CategoryTheory/Sites): colimits in categories of extensive sheaves are computed objectwise #19913
• depends on: feat(CategoryTheory/Abelian): AB axioms carry over to functor categories #19914

[github-actions]

PR summary 0b55b3c9e7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.Grp.AB5	1326	0	-1326 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.Grp.AB5	-1326
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms	-910
Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits (new file)	875
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic	910
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory (new file)	911
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf (new file)	923
Mathlib.Algebra.Category.Grp.AB (new file)	1328
Mathlib.Algebra.Category.ModuleCat.AB (new file)	1330
Mathlib.Condensed.AB (new file)	1812

---

Declarations diff

+ createsColimitOfIsSheaf
+ hasExactColimitsOfShape
+ hasExactColimitsOfShape_transport
+ hasExactLimitsOfShape
+ hasExactLimitsOfShape_transport
+ instance : AB4 (CondensedMod.{u} R) := AB4.of_AB5 _
+ instance : AB4 (ModuleCat.{u} R) := AB4.of_AB5 _
+ instance : AB4 AddCommGrp.{u} := AB4.of_AB5 _
+ instance : AB4Star (CondensedMod.{u} R)
+ instance : AB4Star (ModuleCat.{u} R)
+ instance : AB4Star AddCommGrp.{u}
+ instance : AB5 (CondensedMod.{u} R)
+ instance : AB5 (ModuleCat.{u} R)
+ instance : HasColimits (CondensedMod.{u} R)
+ instance : HasExactColimitsOfShape J (C ⥤ A)
+ instance : HasExactLimitsOfShape (Discrete J) (AddCommGrp.{u}) := by
+ instance : HasExactLimitsOfShape J (C ⥤ A)
+ instance : HasLimits (CondensedMod.{u} R)
+ instance [HasFiniteColimits A] [HasLimitsOfShape J A] [HasExactLimitsOfShape J A]
+ instance [HasFiniteLimits A] [HasColimitsOfShape J A] [HasExactColimitsOfShape J A]
+ instance [Preadditive A] : PreservesFiniteProducts (colim (J := J) (C := A))
+ instance [Preadditive A] [HasFiniteColimits A] :
+ instance [PreservesFiniteProducts (colim (J := J) (C := A))] :
+ instance {A : Type*} [Category A] [HasFiniteColimits A]
+ instance {A : Type*} [Category A] [HasFiniteLimits A] : HasFiniteLimits (Condensed.{u} A)
+ instance {A J : Type*} [Category A] [Category J] [HasColimitsOfShape J A]
+ instance {A J : Type*} [Category A] [Category J] [HasLimitsOfShape J A] :
+ isSheaf_pointwiseColimit
+ pointwiseCocone
+ pointwiseIsColimit
++-- instance :
- instance : HasLimits (CondensedMod.{u} R) := by

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.

---

No changes to technical debt.

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:

• feat(Algebra/Category): the category of abelian groups satisfies AB4* #19912
• feat(CategoryTheory/Sites): colimits in categories of extensive sheaves are computed objectwise #19913
• feat(CategoryTheory/Abelian): AB axioms carry over to functor categories #19914
  By Dependent Issues (🤖). Happy coding!