Skip to content

[Merged by Bors] - chore: don't use TopologicalGroup.toUniformSpace in tendstoUniformly_iff#19098

Closed
j-loreaux wants to merge 2 commits intomasterfrom
j-loreaux/UniformGroup.tendstoUniformly_iff
Closed

[Merged by Bors] - chore: don't use TopologicalGroup.toUniformSpace in tendstoUniformly_iff#19098
j-loreaux wants to merge 2 commits intomasterfrom
j-loreaux/UniformGroup.tendstoUniformly_iff

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Nov 15, 2024 •
edited
Loading

This changes TopologicalGroup.tendstoUniformly_iff so that it takes a UniformSpace instance instead of only a TopologicalGroup instance, along with a proof that the uniform space is the one induced by the topological group structure. The previous version would have been hard to use in case you had, for example, a normed commutative group, as the uniform space structure inferred would not match (defeq) the one given in this theorem, which was previously TopologicalSpace.toUniformSpace.

Open in Gitpod

@j-loreaux j-loreaux added t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields, etc) easy < 20s of review time. See the lifecycle page for guidelines. labels Nov 15, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 15, 2024 •
edited
Loading

PR summary 12438efb1a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ tendstoLocallyUniformlyOn_iff
+ tendstoLocallyUniformly_iff
+ tendstoUniformlyOn_iff
+ tendstoUniformly_iff
- TopologicalGroup.tendstoLocallyUniformlyOn_iff
- TopologicalGroup.tendstoLocallyUniformly_iff
- TopologicalGroup.tendstoUniformlyOn_iff
- TopologicalGroup.tendstoUniformly_iff

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).

@j-loreaux j-loreaux removed the easy < 20s of review time. See the lifecycle page for guidelines. label Nov 15, 2024
@j-loreaux j-loreaux mentioned this pull request Nov 15, 2024
Closed
1 task
@j-loreaux j-loreaux added the easy < 20s of review time. See the lifecycle page for guidelines. label Nov 15, 2024
@ADedecker
Copy link
Copy Markdown
Member

ADedecker commented Nov 15, 2024

Let me just note (maybe it would be nice to add this to the commit message) that this is strictly speaking removing some mathematical content, because TopologicalSpace.toUniformSpace does make sense for any topological group while UniformGroup is a weird thing that has basically no chance to be true outside of the compact or abelian case.

The reason I won't ask to keep the current version though is that we already have to redo a lot of more crucial things once we do this properly (by having LeftUniformity and RightUniformity typeclasses), so this will be refactored anyways.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 15, 2024

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 15, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Nov 16, 2024

@ADedecker I've opted for a middle ground where we don't lose any mathematical content, but instead the fact that the uniform space is equal to the one induced by the topological group structure is passed as an argument. This allows the caller to supply UniformGroup.toUniformSpace_eq in case that they need to.

@j-loreaux
Copy link
Copy Markdown
Contributor Author

j-loreaux commented Nov 16, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 16, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 16, 2024
@j-loreaux
chore: don't use TopologicalGroup.toUniformSpace in `tendstoUniform…
b4ef117 
…ly_iff` (#19098)

This changes `TopologicalGroup.tendstoUniformly_iff` so that it takes a `UniformSpace` instance instead of only a `TopologicalGroup` instance, along with a proof that the uniform space is the one induced by the topological group structure. The previous version would have been hard to use in case you had, for example, a normed commutative group, as the uniform space structure inferred would not match (defeq) the one given in this theorem, which was previously `TopologicalSpace.toUniformSpace`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 16, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: don't use TopologicalGroup.toUniformSpace in tendstoUniformly_iff [Merged by Bors] - chore: don't use TopologicalGroup.toUniformSpace in tendstoUniformly_iff Nov 16, 2024
@mathlib-bors mathlib-bors bot closed this Nov 16, 2024
@mathlib-bors mathlib-bors bot deleted the j-loreaux/UniformGroup.tendstoUniformly_iff branch November 16, 2024 16:02
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@j-loreaux @TobiasLeichtfried
chore: don't use TopologicalGroup.toUniformSpace in `tendstoUniform…
125b8cf 
…ly_iff` (#19098)

This changes `TopologicalGroup.tendstoUniformly_iff` so that it takes a `UniformSpace` instance instead of only a `TopologicalGroup` instance, along with a proof that the uniform space is the one induced by the topological group structure. The previous version would have been hard to use in case you had, for example, a normed commutative group, as the uniform space structure inferred would not match (defeq) the one given in this theorem, which was previously `TopologicalSpace.toUniformSpace`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@j-loreaux @ADedecker