feat(Condensed): characterisation of discrete (light) condensed sets and modules

[dagurtomas]

This PR provides a characterisation of discrete condensed sets and modules, both in the light setting and the classical one.

• A condensed module is discrete if and only if its underlying condensed set is
• Six equivalent conditions on a condensed set X to be discrete
  1. The counit of the discrete-underlying adjunction applied to X is an isomorphism
  2. X is in the essential image of the constant sheaf functor Type (u+1) ⥤ CondensedSet.{u}
  3. X is in the essential image of the functor Type (u+1) ⥤ CondensedSet.{u} which takes a set to the sheaf of locally constant maps into it.
  4. The counit of the locally-constant-underlying adjunction applied to X is an isomorphism.
  5. X restricted to the coherent site of profinite sets is discrete as a sheaf
  6. For every profinite set S written as a limit of finite sets, X maps S to the corresponding colimit.
• The analogues for the above for light condensed sets and modules

---

• [ ] depends on: #12930
• [ ] depends on: #13333
• [ ] depends on: #13486
• [ ] depends on: #13947
• [x] depends on: #14017
• [x] depends on: #14406

[github-actions[bot]]

PR summary 8f7896ed23

Import changes exceeding 2%

%	File
+4.47%	Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.ModuleCat.FilteredColimits	805	841	+36 (+4.47%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.ModuleCat.FilteredColimits	36
Mathlib.Condensed.Discrete.Characterization	1696

---

Declarations diff

+ forgetReflectsFilteredColimits + instance : HasLimitsOfSize.{u, u+1} (ModuleCat.{u+1} R) ++ IsDiscrete ++ LocallyConstant.adjunction ++ isDiscrete_iff_isDiscrete_forget ++ mem_locallyContant_essImage_of_isColimit_mapCocone ++++ isDiscrete_tfae

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.

[dagurtomas]

PR summary 92528ad914

Import changes exceeding 2%

% File +4.37% Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Import changes for modified files

Declarations diff

I think it's completely reasonable that the file ModuleCat.FilteredColimits knows that ModuleCat has colimits

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12930~~
• ~~leanprover-community/mathlib4#13333~~
• ~~leanprover-community/mathlib4#13486~~
• ~~leanprover-community/mathlib4#13947~~
• ~~leanprover-community/mathlib4#14017~~
• ~~leanprover-community/mathlib4#14382~~
• ~~leanprover-community/mathlib4#14406~~
• ~~leanprover-community/mathlib4#15321~~
• ~~leanprover-community/mathlib4#15566~~
• ~~leanprover-community/mathlib4#15569~~
• ~~leanprover-community/mathlib4#17537~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

:v: dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dagurtomas]

Thanks for all the reviews 🎉

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style