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(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446

wants to merge 27 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Sep 9, 2022 •
edited by github-actions bot
Loading

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.

Open in Gitpod

@j-loreaux
initial proof of completeness
9f5730b
@j-loreaux
remove commutativity requirement
a63714d
@j-loreaux
remove filter.has_basis.mul
0645ab7
@j-loreaux
clean up until completeness
a537cdf
@j-loreaux
clean up and add docstrings
2556c14
@j-loreaux
closed not necessary
0d55d8f
@j-loreaux
More cleaning
3f458b1
@j-loreaux
simplify proof of cauchy
eaefdb4
@j-loreaux
remove inverse bits, no longer necessary
f239bc2
@j-loreaux
use filter.has_basis.cauchy_seq_iff
be35831
@j-loreaux
un-capitalize
4d7fd1e
@j-loreaux
fix variables
8ae8dbd
@j-loreaux
fix to_additive docstrings
e7f1e16
@j-loreaux
rename file
f333290
@j-loreaux
add module docstring and copyright
374adee
@j-loreaux
generalize to arbitrary topological groups
f81ba8f
@j-loreaux
fix broken norm instance
4325272
@j-loreaux
remove uniformity countably generated
363c7fa
@j-loreaux
distribute to appropriate files
e46cf83
@j-loreaux
add references
337a9b0
@j-loreaux
fix Misc to Book
6aa9936
@j-loreaux
use filter.has_antitone_basis.subbasis_with_rel
556c93f
@j-loreaux
add maximal ideal closed
a873e3b
@j-loreaux
add normed structures on quotients
9fe2092
@j-loreaux
Revert "add maximal ideal closed"
71e3203 
This reverts commit a873e3b.
@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-analysis Analysis (normed *, calculus) labels Sep 9, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 9, 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 9, 2022
This was referenced Sep 12, 2022
Closed
Closed
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 13, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@dupuisf
Copy link
Collaborator

dupuisf commented Sep 15, 2022

Could you add a little bit of documentation about this in the file-level docstring as well? Looks good otherwise.

bors d+

@bors
Copy link

bors bot commented Sep 15, 2022

✌️ 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 delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 15, 2022
@j-loreaux
Copy link
Collaborator Author

bors r+

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
Copy link

bors bot commented Sep 15, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals [Merged by Bors] - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals Sep 15, 2022
@bors bors bot closed this Sep 15, 2022
@bors bors bot deleted the j-loreaux/normed-ring-quotient branch September 15, 2022 16:26
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(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
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@j-loreaux @mathlib-dependent-issues-bot @dupuisf