[Merged by Bors] - chore(analysis/locally_convex/strong_topology): generalize to semilinear maps #18679
Conversation
mcdoll
added
awaiting-review
|
|
||
| lemma strong_topology.locally_convex_space (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) | ||
| (h𝔖₂ : directed_on (⊆) 𝔖) : | ||
| @locally_convex_space ℝ (E →L[ℝ] F) _ _ _ (strong_topology (ring_hom.id ℝ) F 𝔖) := | ||
| @locally_convex_space ℝ (E →SL[σ] F) _ _ _ (strong_topology σ F 𝔖) := |
There was a problem hiding this comment.
I was able to generalize ℝ to an arbitrary ordered_semiring R too.
I've pushed a commit; feel free to revert it (and my change to the PR description) if you think it's a bad idea
bors d+
There was a problem hiding this comment.
Thanks, I was not thinking about that. I think there is no applications for locally convex spaces over ordered semirings that are not the reals, but if the definition of locally convex allows for more generality, then these theorems should as well.
There was a problem hiding this comment.
Presumably you could work with rational coordinates in R^3, which would make sense here?
There was a problem hiding this comment.
If you're happy with the change I pushed feel free to merge.
There was a problem hiding this comment.
I didn't get a mail that CI went through. Does
bors merge
work in a comment?
There was a problem hiding this comment.
I guess the CI mail went to me because I was the one who pushed.
|
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
eric-wieser
added
delegated
…ear maps (#18679) This is needed to show that the space of C-linear maps is locally convex. Also generalizes the ring from `real` to a general ordered semiring, since the proofs didn't need the `real`s. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This is needed to show that the space of C-linear maps is locally convex.
Also generalizes the ring from
realto a general ordered semiring, since the proofs didn't need thereals.