Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete #16368

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete #16368

wants to merge 23 commits into from

Conversation

j-loreaux
Copy link
Collaborator

Open in Gitpod

@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Sep 4, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 4, 2022
This was referenced Sep 9, 2022
Closed
Closed
dupuisf
dupuisf reviewed Sep 13, 2022
View reviewed changes
src/topology/algebra/uniform_group.lean
Comment on lines +766 to +767
[@complete_space G (topological_group.to_uniform_space G)] :
@complete_space (G ⧸ N) (topological_group.to_uniform_space (G ⧸ N)) :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would make sense to add a note about why this topological_group.to_uniform_space stuff is needed here and in the next instance.

@dupuisf dupuisf added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 13, 2022
@j-loreaux
Copy link
Collaborator Author

Let me know if the changes I made were what you were looking for.

@dupuisf
Copy link
Collaborator

dupuisf commented Sep 13, 2022

Yes, this looks good. Out of curiosity, does the last instance actually kick in in these most common use cases where the uniform space structure is defeq with this one?

@j-loreaux
Copy link
Collaborator Author

j-loreaux commented Sep 13, 2022 •
edited
Loading

Yes, I checked that. Well, it does for seminormed_add_comm_group anyway. For quotients by submodules and ideals you need to transfer manually through the definitional equality of submodule.to_add_subgroup.

@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 13, 2022
@dupuisf
Copy link
Collaborator

dupuisf commented Sep 13, 2022

Yes, I checked that. Well, it does for seminormed_add_comm_group anyway. For quotients by submodules and ideals you need to transfer manually through the definitional equality of submodule.to_add_subgroup.

Would it make sense to add extra instances for submodules and ideals so we don't have to do this manually?

@j-loreaux
Copy link
Collaborator Author

It's in #16446. It needs to be there because we didn't have norm structures on other kinds of quotients yet.

@dupuisf
Copy link
Collaborator

dupuisf commented Sep 13, 2022

Ah I see! In that case LGTM.

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 13, 2022
bors bot pushed a commit that referenced this pull request Sep 13, 2022
@j-loreaux
feat(topology/algebra/uniform_group): the quotient of a first countab…
c0ad3bf 
…le complete topological group by a normal subgroup is itself complete (#16368)
@bors
Copy link

bors bot commented Sep 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete [Merged by Bors] - feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete Sep 13, 2022
@bors bors bot closed this Sep 13, 2022
@bors bors bot deleted the j-loreaux/uniform-group-quotient-complete branch September 13, 2022 16:05
bors bot pushed a commit that referenced this pull request Sep 15, 2022
@j-loreaux
feat(analysis/normed/group/quotient): transfer norm structures on quo…
3077b72 
…tients of groups to quotients of modules by submodules and of rings by ideals (#16446)

This takes the existing norm structures on quotients of additive groups and transfers it along the definitional equality to quotients of modules by submodules and quotients of rings by ideals. In addition, this puts the extra norm structures on these objects where appropriate including `complete_space`, `normed_space`, `semi_normed_comm_ring`, `normed_comm_ring` and `normed_algebra`.

- [x] depends on: #16368
bors bot pushed a commit that referenced this pull request Sep 16, 2022
@j-loreaux
feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand tr…
f1397dc 
…ansform is a bijective isometry for C⋆-algebras over ℂ (#16488)

- [x] depends on: #16451
- [x] depends on: #16438
- [x] depends on: #16368
- [x] depends on: #16303
- [x] depends on: #16446
- [x] depends on: #16448
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
@j-loreaux @b-mehta
feat(topology/algebra/uniform_group): the quotient of a first countab…
8cb7cf3 
…le complete topological group by a normal subgroup is itself complete (#16368)
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
@j-loreaux @b-mehta
feat(analysis/normed/group/quotient): transfer norm structures on quo…
9ee3050 
…tients of groups to quotients of modules by submodules and of rings by ideals (#16446)

This takes the existing norm structures on quotients of additive groups and transfers it along the definitional equality to quotients of modules by submodules and quotients of rings by ideals. In addition, this puts the extra norm structures on these objects where appropriate including `complete_space`, `normed_space`, `semi_normed_comm_ring`, `normed_comm_ring` and `normed_algebra`.

- [x] depends on: #16368
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
@j-loreaux @b-mehta
feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand tr…
efa2d4c 
…ansform is a bijective isometry for C⋆-algebras over ℂ (#16488)

- [x] depends on: #16451
- [x] depends on: #16438
- [x] depends on: #16368
- [x] depends on: #16303
- [x] depends on: #16446
- [x] depends on: #16448
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@dupuisf dupuisf dupuisf left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) 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.

None yet
3 participants
@j-loreaux @dupuisf @urkud