-
Notifications
You must be signed in to change notification settings - Fork 297
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.
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
[Merged by Bors] - feat(analysis/normed_space/SemiNormedGroup): has_cokernels #7628
Conversation
From LTE. Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Thanks Benjamin! Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
…NormedGroup_cokernel
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
lemma lift_bound_by {N : Type*} [semi_normed_group N] (S : add_subgroup M) | ||
(f : normed_group_hom M N) (hf : ∀ s ∈ S, f s = 0) | ||
{c : ℝ≥0} (fb : f.bound_by c) : | ||
(lift S f hf).bound_by c := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I realize that I was just being completely ignorant with this bound_by
definition. Would you mind phrasing this in terms of the operator norm?
Thanks 🎉 bors merge |
# Cokernels in SemiNormedGroup₁ and SemiNormedGroup We show that `SemiNormedGroup₁` has cokernels (for which of course the `cokernel.π f` maps are norm non-increasing), as well as the easier result that `SemiNormedGroup` has cokernels. So far, I don't see a way to state nicely what we really want: `SemiNormedGroup` has cokernels, and `cokernel.π f` is norm non-increasing. The problem is that the limits API doesn't promise you any particular model of the cokernel, and in `SemiNormedGroup` one can always take a cokernel and rescale its norm (and hence making `cokernel.π f` arbitrarily large in norm), obtaining another categorical cokernel. Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Cokernels in SemiNormedGroup₁ and SemiNormedGroup
We show that
SemiNormedGroup₁
has cokernels(for which of course the
cokernel.π f
maps are norm non-increasing),as well as the easier result that
SemiNormedGroup
has cokernels.So far, I don't see a way to state nicely what we really want:
SemiNormedGroup
has cokernels, andcokernel.π f
is norm non-increasing.The problem is that the limits API doesn't promise you any particular model of the cokernel,
and in
SemiNormedGroup
one can always take a cokernel and rescale its norm(and hence making
cokernel.π f
arbitrarily large in norm), obtaining another categorical cokernel.