feat: define Submodule.IsTopCompl#38547
feat: define Submodule.IsTopCompl#38547ADedecker wants to merge 24 commits intoleanprover-community:masterfrom
Conversation
PR summary 452dba9608Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
ping me when this is ready; I'd like to review this :) |
ADedecker
added
t-topology
ADedecker
added
the
awaiting-CI
|
@themathqueen CI will probably fail a few times because of import stuff, but otherwise this is ready for review! |
| protected noncomputable def IsTopCompl.projectionOnto (h : IsTopCompl p q) : M →L[R] p := | ||
| ⟨p.linearProjOfIsCompl q h.isCompl, by | ||
| rw [IsInducing.subtypeVal.continuous_iff] | ||
| exact h.continuous_projection⟩ |
There was a problem hiding this comment.
This is not the standard name, but I claim that it should be. I think the Onto is the best way to distinguish between the two forms of a projection.
So I claim we shoud have:
IsCompl.projection/IsCompl.projectionOntoSubmodule.orthogonalProjectionOnto/Submodule.orthogonalProjection
There was a problem hiding this comment.
So you're proposing these changes, right?
Submodule.linearProjOfIsCompl->Submodule.IsCompl.projectionOnto,Submodule.orthogonalProjection->Submodule.orthogonalProjectionOnto,Submodule.starProjection->Submodule.orthogonalProjection
I agree that these are better names (especially the first one).
Only problem with the latter two is that orthogonalProjection -> orthogonalProjectionOnto won't have a deprecation or anything (I guess we can add a note?).
But, how about we start with the first one? Then later we can change the orthogonal projections?
Start a Zulip thread about this, just in case anyone objects to this?
There was a problem hiding this comment.
Yes, these are my suggestions. I won't really have time to do this renaming though, but I'll start the discussion on Zulip in case you (or someone else) wants to proceed.
github-actions
Bot
removed
the
awaiting-CI
|
I believe that @themathqueen is right that some renaming might be desirable but I'm happy to merge these changes as they stand. With that in mind: |
|
✌️ themathqueen can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-triage
Bot
added
the
delegated
|
@ocfnash I think there is a misunderstanding : the names in this PR are not the standard one given to similar objects, but I think that they are better (and IIUC Monica agrees). Thus the renaming discussion is about the existing objects in Mathlib, rather than the ones introduced in this PR. |
| IsClosed (p : Set M) := | ||
| h.symm.isClosed' | ||
|
|
||
| /-- If `p` and `q` are topological complements and `q` is closed, then `p` is Hausdorff. -/ |
There was a problem hiding this comment.
Shouldn't we say:
| /-- If `p` and `q` are topological complements and `q` is closed, then `p` is Hausdorff. -/ | |
| /-- If `p` and `q` are topological complements and `q` is closed, then `p` is regular. -/ |
or else move this comment down to the instance below.
There was a problem hiding this comment.
(I wrote this hours ago but accidentally left the review pending)
There was a problem hiding this comment.
I'll move it to the theorem below, all of these axioms are equivalent anyways in this setting.
Indeed this was already my understanding. The only reason I haven't sent this straight to bors was that I wanted to be sure Monica felt the conversation here was resolved. |
mathlib-triage
Bot
added
delegated
themathqueen
left a comment
themathqueen
left a comment
There was a problem hiding this comment.
Here's a first round of comments. I'll do another round first thing tomorrow.
Before I forget, we'll want the IsTopCompl versions of Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl and Submodule.toLinearMap_starProjection_eq_isComplProjection.
I think it's fine if you do it in this PR, but also fine to keep it as a follow up, up to you.
There was a problem hiding this comment.
Why not call this file Projection?
There was a problem hiding this comment.
I'm not a huge fan. I know a significant portion of the file is dedicated to projections, but I really view it as being about topological complements.
|
I'm a bit short on time, so I'll leave the link with orthogonal projections for later. |
|
Do you want to add the continuous analogues for LinearMap.IsIdempotentElem.eq_isCompl_projection and LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker in this PR? |
|
I'm tempted to say that this is large enough already. There are a bunch other things which I left out, my main goal was to have a working definition and API. |
themathqueen
left a comment
themathqueen
left a comment
There was a problem hiding this comment.
Here's another batch of comments. I'll have one final look in a few hours (please bear with me 🙏)
|
There's no rush! |
|
Ah, I remembered why I didn't put |
themathqueen
left a comment
themathqueen
left a comment
There was a problem hiding this comment.
Okay, I think I'm happy with this. Thanks! Just some minor comments.
For the analogues I mentioned in the previous comments, I can do them after this PR if you want.
|
|
||
| end IsTopCompl | ||
|
|
||
| section ClosedComplemented |
There was a problem hiding this comment.
how about namespaceing this instead of doing ClosedComplemented. throughout the section?
There was a problem hiding this comment.
I tend to prefer adding more ClosedComplemented to adding more _root_.Submodule., but if you feel strongly about it I'm fine with doing this change.
| /-- If `h : IsTopCompl p q`, `h.projectionOnto` is the continuous linear projection `M →L[R] p` | ||
| along `q`. This is the continuous version of `Submodule.linearProjOfIsCompl`. | ||
|
|
||
| See also `Submodule.IsTopCompl.projection` for the same projection as an element of `M →L[R] M`. -/ | ||
| protected noncomputable def IsTopCompl.projectionOnto (h : IsTopCompl p q) : M →L[R] p := |
There was a problem hiding this comment.
As annoying as this would look like in the code, I think this and IsTopCompl.projection should have p and q explicit so that it doesn't pretty print IsTopCompl.projectionOnto ⋯ in some cases (it would look confusing to someone who didn't write it without opening the code). At least you'd still be able to use dot notation though, just needs to also have h.projectionOnto _ _ :(.
Same goes for IsCompl.projection (I'll fix this in a PR later tomorrow, or you could do it if you want). See for example, Submodule.toLinearMap_starProjection_eq_isComplProjection.
| /-- If `h : IsTopCompl p q`, `h.projectionOnto` is the continuous linear projection `M →L[R] p` | |
| along `q`. This is the continuous version of `Submodule.linearProjOfIsCompl`. | |
| See also `Submodule.IsTopCompl.projection` for the same projection as an element of `M →L[R] M`. -/ | |
| protected noncomputable def IsTopCompl.projectionOnto (h : IsTopCompl p q) : M →L[R] p := | |
| variable (p q) in | |
| /-- If `h : IsTopCompl p q`, `h.projectionOnto` is the continuous linear projection `M →L[R] p` | |
| along `q`. This is the continuous version of `Submodule.linearProjOfIsCompl`. | |
| See also `Submodule.IsTopCompl.projection` for the same projection as an element of `M →L[R] M`. -/ | |
| protected noncomputable def IsTopCompl.projectionOnto (h : IsTopCompl p q) : M →L[R] p := |
Oh yeah! My bad, I totally forgot that we fixed |
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
| algebraic isomorphism `M ≃ p × q` is an homeomorphism. | ||
|
|
||
| Not all submodules of `M` admit such a topological complements (even if they admit algebraic | ||
| complements). In the litterature, such a submodule is called *topologically complemented* |
There was a problem hiding this comment.
Thanks, will fix!
Tip: for this kind of changes, you can write suggestions (see https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/commenting-on-a-pull-request) so that I can just click "accept" to implement it.
4 participants
Right now, Mathlib defines Submodule.ClosedComplemented.
Submodule.IsTopComplis the more precise version saying that two subspaces are topological complements to each other.