refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces

[dagurtomas]

trafficstars

This PR unifies the definitions of the categories CompHaus, Profinite, Stonean, and LightProfinite by defining a structure CompHausLike P depending on a predicate P on topological spaces. Many of the properties of these categories of compact Hausdorff spaces are shared between them and this approach reduces duplication of boilerplate code, in particular the explicit constructions of certain limits and colimits.

---

The benefit of this refactor is demonstrated by its big negative diff, and the fact that it can be used to prove that the functors of discrete objects into light condensed sets and condensed sets are given by the sheaf of locally constant maps, at the same time (see #14027).

• [x] depends on: #13904
• [x] depends on: #13905
• [x] depends on: #13907
• [ ] depends on: #13908
• [ ] depends on: #13909
• [ ] depends on: #13911
• [ ] depends on: #13912

[github-actions[bot]]

PR summary 54d8152f7a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Category.CompHaus.EffectiveEpi	1379	1381	+2 (+0.15%)
Mathlib.Topology.Category.CompHaus.Limits	1355	1356	+1 (+0.07%)
Mathlib.Topology.Category.Profinite.EffectiveEpi	1403	1404	+1 (+0.07%)
Mathlib.Topology.Category.Stonean.EffectiveEpi	1403	1404	+1 (+0.07%)

Import changes for all files

Files	Import difference
8 files Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Condensed.TopComparison Mathlib.Condensed.Explicit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.CompHaus.Limits Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence	1
7 files Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Basic Mathlib.Condensed.Solid Mathlib.Condensed.Discrete Mathlib.Condensed.Functors	2

---

Declarations diff

+ instance : HasExplicitFiniteCoproducts.{w, u} (fun _ ↦ True) + instance : HasExplicitPullbacks (fun _ ↦ True) - Sigma.ι_comp_toFiniteCoproduct - coproductHomeoCoproduct - coproductIsoCoproduct - finiteCoproduct - finiteCoproduct.desc - finiteCoproduct.hom_ext - finiteCoproduct.isColimit - finiteCoproduct.ι - finiteCoproduct.ι_desc - finiteCoproduct.ι_desc_apply - finiteCoproduct.ι_injective - finiteCoproduct.ι_jointly_surjective - instance : FinitaryExtensive CompHaus - instance : Precoherent CompHaus.{u} := inferInstance - instance : PreservesFiniteCoproducts compHausToTop := by - isTerminalPUnit - pullback - pullback.condition - pullback.cone - pullback.fst - pullback.hom_ext - pullback.isLimit - pullback.lift - pullback.lift_fst - pullback.lift_snd - pullback.snd - pullbackHomeoPullback - pullbackIsoPullback - pullback_fst_eq - pullback_snd_eq --- struct

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.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13904~~
• ~~leanprover-community/mathlib4#13905~~
• ~~leanprover-community/mathlib4#13907~~
• ~~leanprover-community/mathlib4#13908~~
• ~~leanprover-community/mathlib4#13909~~
• ~~leanprover-community/mathlib4#13911~~
• ~~leanprover-community/mathlib4#13912~~
• ~~leanprover-community/mathlib4#15359~~
• ~~leanprover-community/mathlib4#15362~~
• ~~leanprover-community/mathlib4#15363~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style