[Merged by Bors] - feat(topology/algebra/module/strong_topology): golf arrow_congrSL introduced in #19107
#19128
Conversation
github-actions
bot
added
the
modifies-synchronized-file
ADedecker
added
WIP
github-actions
bot
added
the
modifies-synchronized-file
|
Does it make sense to have compL instead of 2 maps? |
|
IIRC |
| begin | ||
| letI : uniform_space G := topological_add_group.to_uniform_space G, | ||
| haveI : uniform_add_group G := topological_add_comm_group_is_uniform, | ||
| rw (strong_topology.embedding_coe_fn _ _ _).continuous_iff, | ||
| refine (uniform_on_fun.precomp_uniform_continuous _).continuous.comp | ||
| (strong_topology.embedding_coe_fn _ _ _).continuous, | ||
| exact λ S hS, hS.image L, | ||
| end } |
There was a problem hiding this comment.
This should be a standalone lemma I think
There was a problem hiding this comment.
I would guess (precomp G L).continuous is enough ? In Lean 3 this usually works quite well, and usually we don't add this lemma (see e.g continuous_linear_map.compSL)
That said maybe we'll want to add it if Lean4 is a bit more rigid on unification.
|
|
||
| include σ₁₄ σ₂₄ σ₁₃ σ₃₄ σ₂₁ σ₂₃ | ||
|
|
||
| /-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the | ||
| spaces of continuous (semi)linear maps. -/ | ||
| @[simps] def arrow_congrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : |
There was a problem hiding this comment.
Are you sure we want to drop arrow_congrₛₗ? Why not both?
There was a problem hiding this comment.
Well the extra hypothesis are not actually adding any constraint IIRC (in the sense that they follow from the previous assumptions, but the typeclass system can't know that), so just using arrow_congrSL looks fine to me.
|
|
ADedecker
added
awaiting-review
|
Thanks! 🎉 |
github-actions
bot
added
ready-to-merge
…ntroduced in #19107 (#19128) I added more general definitions `precomp` and `postcomp` for expressing that (pre/post)-composing by a *fixed* continuous linear maps is continuous. These were planned about a year ago when I defined the strong topology and follow from [uniform_on_fun.precomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.precomp_uniform_continuous) and [uniform_on_fun.postcomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.postcomp_uniform_continuous). The proof of continuity of `arrow_congrSL` is a direct consequence of these, so we don't have to do it by hand. This is not really a "golf" since I added more lines than I removed, but these more general constructions will be needed at some point anyway (my use case was distribution theory) so I'm doing some proactive golfing 😄.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
arrow_congrSL introduced in #19107arrow_congrSL introduced in #19107
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
The changed proof was rewritten completely.
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
I added more general definitions
precompandpostcompfor expressing that (pre/post)-composing by a fixed continuous linear maps is continuous. These were planned about a year ago when I defined the strong topology and follow from uniform_on_fun.precomp_uniform_continuous and uniform_on_fun.postcomp_uniform_continuous.The proof of continuity of
arrow_congrSLis a direct consequence of these, so we don't have to do it by hand.This is not really a "golf" since I added more lines than I removed, but these more general constructions will be needed at some point anyway (my use case was distribution theory) so I'm doing some proactive golfing 😄.