feat(Topology/Category): category of delta-generated spaces

[peabrainiac]

Introduces the category of delta-generated spaces and shows that it is complete, cocomplete and coreflective in the category of topological spaces.

---

• depends on: [Merged by Bors] - feat(Topology/Compactness): delta-generated spaces #19431

[github-actions]

PR summary f15b416599

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Category.DeltaGenerated (new file)	1484

---

Declarations diff

+ DeltaGenerated
+ coreflectorAdjunction
+ deltaGeneratedToTop
+ deltaGeneratedToTop.coreflective
+ deltaGeneratedToTop.createsColimits
+ fullyFaithfulDeltaGeneratedToTop
+ hasColimits
+ hasLimits
+ instance : CoeSort DeltaGenerated Type*
+ instance : ConcreteCategory.{u} DeltaGenerated.{u}
+ instance : LargeCategory.{u} DeltaGenerated.{u}
+ instance : deltaGeneratedToTop.{u}.Faithful := fullyFaithfulDeltaGeneratedToTop.faithful
+ instance : deltaGeneratedToTop.{u}.Full := fullyFaithfulDeltaGeneratedToTop.full
+ instance : topToDeltaGenerated.{u}.Faithful
+ of
+ topToDeltaGenerated

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:

• [Merged by Bors] - feat(Topology/Compactness): delta-generated spaces #19431
  By Dependent Issues (🤖). Happy coding!

[grunweg]

Checking in from PR triage: this PR has a merge conflict. Can you merge master, please? Then this PR can be reviewed much more easily. Thanks!

[peabrainiac]

The merge conflict is fixed now. Thanks for pointing it out, I didn't notice - really unfortunate that github apparently doesn't give PR authors the option to get notified when merge confllicts occur.

[grunweg]

Thanks. I agree this is unfortunate. I can only think of two strategies:

• in this specific case, a dependent PR was merged: that's usually an occasion for merge conflicts. Github's email notifications cover this.
• for the general case, the on the queue page contains data about all open PRs: filtering by your github handle will give you an overview about all your PRs. (This might be the most useful if you have many PRs. I use this sometimes.)

[grunweg]

I just took a look at your PR. I just pushed a few nits myself (to save you the extra round of suggesting them and you accepting them); feel free to revert any changes you disagree with.

[grunweg]

Two follow-up questions:

• how difficult is it to show that delta-generated spaces are compactly generated? DeltaGeneratedSpace mentions this, but doesn't prove it (as far as I can see)
• given this PR, how far is mathlib from knowing that a diffeological space/an orbifold is? :-)

[grunweg]

@kim-em This PR looks good to me: the proofs are reasonable, its structure matches CompactlyGenerated.lean. I'm not an expert on the best spelling of things in category theory. Can you give this a final look, please? Thanks!

[peabrainiac]

Two follow-up questions:

• how difficult is it to show that delta-generated spaces are compactly generated? DeltaGeneratedSpace mentions this, but doesn't prove it (as far as I can see)

• given this PR, how far is mathlib from knowing that a diffeological space/an orbifold is? :-)

Showing that they are compactly generated requires showing that they are generated not just by euclidean spaces like how I've defined them there, but also by something like the unit interval or the standard simplices. That is unfortunately tricky, because the only proof I know requires a concatenation of countably many paths - I've already written the proof up, but the details of this concatenation are unfortunately hairy, so in it I have a few sorries left.

Diffeological spaces on the other hand have honestly been in reach the entire time - I just somewhat procrastinated them, both because PRing their definition feels a lot like locking in design choices that I am not yet 100% sure about, and because there are some things about them that I not not super happy with. For example, that the d-topology and quotient topology on a diffeological quotient space agree is currently only a theorem and not true by rfl, which is quite inconvenient - but changing that would require defining coinduced diffeologies only after the subspace diffeology has already been developed, which would require some restructuring across files.

[peabrainiac]

Showing that they are compactly generated requires showing that they are generated not just by euclidean spaces like how I've defined them there, but also by something like the unit interval or the standard simplices.

Actually thinking about it, this of course isn't true: every delta-generated space is a quotient of a disjoint union of compactly generated spaces, and so itself compactly generated. I do need the path stuff anyway to show that first-countable locally path-connected spaces are delta-generated, but at least here it isn't necessary.