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/seminorm): Group seminorms #15594

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(analysis/seminorm): Group seminorms #15594

wants to merge 5 commits into from

Conversation

YaelDillies
Copy link
Collaborator

Multiplicativize the existing add_group_seminorm material.

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jul 21, 2022
@urkud urkud added t-algebra Algebra (groups, rings, fields etc) t-analysis Analysis (normed *, calculus) labels Jul 24, 2022
b-mehta
b-mehta reviewed Aug 13, 2022
View reviewed changes
Copy link
Collaborator

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

Are group_seminorms needed for anything?

src/analysis/seminorm.lean

namespace add_group_seminorm
attribute [nolint doc_blame] add_group_seminorm.to_zero_hom
Copy link
Collaborator

Choose a reason for hiding this comment

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

Seems like a good opportunity to add this doc!

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

See #2409

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I am particularly unwilling to add this docstring because:

  • It won't show up in the docs.
  • zero_hom is mathematically irrelevant.

Copy link
Member

Choose a reason for hiding this comment

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

I'm pretty sure this does show up in the docs?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Hmm, yeah you're right, it does show up.

src/analysis/seminorm.lean Outdated Show resolved Hide resolved
@YaelDillies
Copy link
Collaborator Author

Currently, we have two ways to talk about (additive group) seminorms:

  • add_group_seminorm
  • seminormed_add_comm_group.core

I want to get rid of the second way and make seminormed groups depend on seminorms (rather than the other way around, as it is today). Now, I am adding multiplicative normed groups in #15705 so I need multiplicative seminorms to make the above plan work, and multiplicativising the API isn't much more work.

You will notice that the above doesn't get us rid of normed_add_comm_group.core. This will get solved once we introduce norms, which I'm planning to do in a separate PR and which I think is desirable anyway to be able to state results such as Asplund's averaging technique.

jcommelin
jcommelin approved these changes Aug 15, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

bors bot pushed a commit that referenced this pull request Aug 15, 2022
@YaelDillies
feat(analysis/seminorm): Group seminorms (#15594)
6eb146e 
Multiplicativize the existing `add_group_seminorm` material.
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Aug 15, 2022
@bors
Copy link

bors bot commented Aug 15, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 15, 2022
@YaelDillies
feat(analysis/seminorm): Group seminorms (#15594)
c4df52c 
Multiplicativize the existing `add_group_seminorm` material.
@bors
Copy link

bors bot commented Aug 15, 2022

Build failed (retrying...):

@bors
Copy link

bors bot commented Aug 15, 2022

Canceled.

@eric-wieser
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Aug 15, 2022

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

@eric-wieser eric-wieser added delegated The PR author may merge after reviewing final suggestions. awaiting-CI The author would like to see what CI has to say before doing more work. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Aug 15, 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 Aug 15, 2022
@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Aug 16, 2022
@YaelDillies
feat(analysis/seminorm): Group seminorms (#15594)
fb1787b 
Multiplicativize the existing `add_group_seminorm` material.
@bors
Copy link

bors bot commented Aug 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/seminorm): Group seminorms [Merged by Bors] - feat(analysis/seminorm): Group seminorms Aug 16, 2022
@bors bors bot closed this Aug 16, 2022
@bors bors bot deleted the group_seminorm branch August 16, 2022 06:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@b-mehta b-mehta b-mehta left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-algebra Algebra (groups, rings, fields etc) t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@YaelDillies @eric-wieser @jcommelin @b-mehta @urkud @leanprover-community-bot-assistant