[Merged by Bors] - feat(Topology/Category): category of delta-generated spaces by peabrainiac · Pull Request #19499 · leanprover-community/mathlib4

peabrainiac · 2024-11-26T03:49:18Z

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

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

github-actions · 2024-11-26T03:50:28Z

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 · 2024-11-26T23:21:25Z

This PR/issue depends on:

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

grunweg · 2024-12-11T22:44:36Z

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 · 2024-12-11T23:30:26Z

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 · 2024-12-12T12:24:02Z

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 · 2024-12-12T12:24:44Z

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 · 2024-12-12T12:26:01Z

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 · 2024-12-12T12:26:55Z

@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 · 2024-12-12T13:52:40Z

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 · 2024-12-12T14:10:46Z

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.

kim-em · 2025-01-11T03:24:02Z

bors merge

Introduces the category of delta-generated spaces and shows that it is complete, cocomplete and coreflective in the category of topological spaces. Co-authored-by: peabrainiac <43812953+peabrainiac@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-01-11T03:34:43Z

Build failed (retrying...):

Build

Introduces the category of delta-generated spaces and shows that it is complete, cocomplete and coreflective in the category of topological spaces. Co-authored-by: peabrainiac <43812953+peabrainiac@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-01-11T04:09:42Z

Build failed (retrying...):

Build

Introduces the category of delta-generated spaces and shows that it is complete, cocomplete and coreflective in the category of topological spaces. Co-authored-by: peabrainiac <43812953+peabrainiac@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-01-11T04:29:08Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

peabrainiac and others added 13 commits November 21, 2024 03:43

adapt DeltaGeneratedSpace.lean from the orbifolds repo

59f905a

delta-generated spaces are compactly generated

8d6ad77

formatting

5cc96d0

delta-generated spaces are sequential

505f85a

quotients and disjoint unions of delta-generated spaces

29ca05b

cleaned up code a bit

f641d39

update Mathlib.lean

ee2b0b6

remove redundant import

f7e97c6

remove unused argument

b5e3810

fix formatting

9d47778

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

fix copyright header typo

f467536

adapt DeltaGenerated.lean from the orbifolds repo

cd8b8ac

DeltaGenerated is complete, cocomplete and coreflective in TopCat

38d9c9c

peabrainiac added t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Nov 26, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Nov 26, 2024

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 26, 2024

add missing docstrings

98068bb

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 26, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 9, 2024

Merge branch 'master' into DeltaGenerated

2b496b4

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 11, 2024

Tweaks

f15b416

grunweg requested a review from kim-em December 12, 2024 12:27

ghost added the ready-to-merge This PR has been sent to bors. label Jan 11, 2025

mathlib-bors bot changed the title ~~feat(Topology/Category): category of delta-generated spaces~~ [Merged by Bors] - feat(Topology/Category): category of delta-generated spaces Jan 11, 2025

mathlib-bors bot closed this Jan 11, 2025

mathlib-bors bot deleted the DeltaGenerated branch January 11, 2025 04:29

Conversation

peabrainiac commented Nov 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary f15b416599

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Nov 26, 2024

Uh oh!

grunweg commented Dec 11, 2024

Uh oh!

peabrainiac commented Dec 11, 2024

Uh oh!

grunweg commented Dec 12, 2024

Uh oh!

grunweg commented Dec 12, 2024

Uh oh!

grunweg commented Dec 12, 2024

Uh oh!

grunweg commented Dec 12, 2024

Uh oh!

peabrainiac commented Dec 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

peabrainiac commented Dec 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

peabrainiac commented Nov 26, 2024 •

edited

Loading

github-actions bot commented Nov 26, 2024 •

edited

Loading

peabrainiac commented Dec 12, 2024 •

edited

Loading

peabrainiac commented Dec 12, 2024 •

edited

Loading