[Merged by Bors] - chore(topology/algebra/group): generalise instances #15171
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
alexjbest
added
awaiting-review
alexjbest
removed
awaiting-review
alexjbest
added
the
awaiting-review
RemyDegenne
reviewed
Jul 8, 2022
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
eric-wieser
reviewed
Jul 8, 2022
…nprover-community/mathlib into alexjbest/gen/topology/algebra/group
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Merge conflict. |
|
bors d+ |
|
✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
|
bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Jul 14, 2022
Using the generalisation linter make the following generalisations in `topology/algebra/group`. Note that topological spaces that are groups with continuous multiplication but noncontinuous inverse do exist at least when the space is noncompact (they are known as paratopological spaces) I do not claim that they are used in mathlib though ;). In summary we generalise: - `tendsto_inv_nhds_within_Ioi` and all variants to only require continuous inverse rather that topological group - the continuous_inv operation on the multiplicative opposite to only require a has_inv, rather than a group - `topological_group.t1_space` from topological groups to only continuous mul - `topological_group.regular_space` (and t2_space) from assuming the base is t1 to only t0. - `compact_open_separated_mul_right/left`, from topological group to mul_one_class with a continuous mul - various `quotient_group.has_continuous_const_smul` type lemmas to continuous_mul and all `to_additive` versions. Also golf the proof of `subgroup.regular_quotient_of_is_closed`
|
bors r- |
…ogy/algebra/group
YaelDillies
added
awaiting-review
|
Just fixed the conflicts. I think it's ready to go again. maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
eric-wieser
reviewed
Apr 3, 2023
|
I think it's worth checking that the PR description is still up to date, in light of renames and merge conflicts. Do you mind doing that, @YaelDillies? |
YaelDillies
reviewed
Apr 3, 2023
|
bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Apr 4, 2023
Using the generalisation linter make the following generalisations in `topology.algebra.group.basic`. Note that topological spaces that are groups with continuous multiplication but noncontinuous inverse do exist at least when the space is noncompact (they are known as paratopological spaces) I do not claim that they are used in mathlib though ;). In summary we generalise: - `tendsto_inv_nhds_within_Ioi` and all variants to only require continuous inverse rather that topological group - the `continuous_inv` operation on the multiplicative opposite to only require a `has_inv`, rather than a group - `topological_group.t1_space` from topological groups to only continuous mul - `topological_group.regular_space` (and `t2_space`) from assuming the base is t1 to just topological group. - `compact_open_separated_mul_right/left`, from topological group to `mul_one_class` with a continuous mul - various `quotient_group.has_continuous_const_smul` type lemmas to continuous_mul - `tsum_sigma`/`tsum_prod` from t1 to t0 and their additivised versions. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 6, 2023
Match leanprover-community/mathlib#15171 * [`topology.algebra.group.basic`@`c10e724be91096453ee3db13862b9fb9a992fef2`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/group/basic?range=c10e724be91096453ee3db13862b9fb9a992fef2..3b1890e71632be9e3b2086ab512c3259a7e9a3ef) * [`topology.algebra.infinite_sum.basic`@`32253a1a1071173b33dc7d6a218cf722c6feb514`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/infinite_sum/basic?range=32253a1a1071173b33dc7d6a218cf722c6feb514..3b1890e71632be9e3b2086ab512c3259a7e9a3ef)
MonadMaverick
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 9, 2023
Match leanprover-community/mathlib#15171 * [`topology.algebra.group.basic`@`c10e724be91096453ee3db13862b9fb9a992fef2`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/group/basic?range=c10e724be91096453ee3db13862b9fb9a992fef2..3b1890e71632be9e3b2086ab512c3259a7e9a3ef) * [`topology.algebra.infinite_sum.basic`@`32253a1a1071173b33dc7d6a218cf722c6feb514`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/infinite_sum/basic?range=32253a1a1071173b33dc7d6a218cf722c6feb514..3b1890e71632be9e3b2086ab512c3259a7e9a3ef)
MonadMaverick
pushed a commit
to MonadMaverick/mathlib4
that referenced
this pull request
Apr 9, 2023
Match leanprover-community/mathlib#15171 * [`topology.algebra.group.basic`@`c10e724be91096453ee3db13862b9fb9a992fef2`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/group/basic?range=c10e724be91096453ee3db13862b9fb9a992fef2..3b1890e71632be9e3b2086ab512c3259a7e9a3ef) * [`topology.algebra.infinite_sum.basic`@`32253a1a1071173b33dc7d6a218cf722c6feb514`..`3b1890e71632be9e3b2086ab512c3259a7e9a3ef`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/infinite_sum/basic?range=32253a1a1071173b33dc7d6a218cf722c6feb514..3b1890e71632be9e3b2086ab512c3259a7e9a3ef)
xroblot
pushed a commit
that referenced
this pull request
Apr 23, 2023
Using the generalisation linter make the following generalisations in `topology.algebra.group.basic`. Note that topological spaces that are groups with continuous multiplication but noncontinuous inverse do exist at least when the space is noncompact (they are known as paratopological spaces) I do not claim that they are used in mathlib though ;). In summary we generalise: - `tendsto_inv_nhds_within_Ioi` and all variants to only require continuous inverse rather that topological group - the `continuous_inv` operation on the multiplicative opposite to only require a `has_inv`, rather than a group - `topological_group.t1_space` from topological groups to only continuous mul - `topological_group.regular_space` (and `t2_space`) from assuming the base is t1 to just topological group. - `compact_open_separated_mul_right/left`, from topological group to `mul_one_class` with a continuous mul - various `quotient_group.has_continuous_const_smul` type lemmas to continuous_mul - `tsum_sigma`/`tsum_prod` from t1 to t0 and their additivised versions. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Using the generalisation linter make the following generalisations in
topology.algebra.group.basic.Note that topological spaces that are groups with continuous multiplication but noncontinuous inverse do exist at least when the space is noncompact (they are known as paratopological spaces) I do not claim that they are used in mathlib though ;).
In summary we generalise:
tendsto_inv_nhds_within_Ioiand all variants to only require continuous inverse rather that topological groupcontinuous_invoperation on the multiplicative opposite to only require ahas_inv, rather than a grouptopological_group.t1_spacefrom topological groups to only continuous multopological_group.regular_space(andt2_space) from assuming the base is t1 to just topological group.compact_open_separated_mul_right/left, from topological group tomul_one_classwith a continuous mulquotient_group.has_continuous_const_smultype lemmas to continuous_multsum_sigma/tsum_prodfrom t1 to t0and their additivised versions.