feat: Ultrastrong topology - #84
Open
themathqueen wants to merge 45 commits into
Open
Conversation
themathqueen
commented
Jun 1, 2026
…ets the new computer.)
themathqueen
commented
Jun 4, 2026
Collaborator
|
Oh shoot! Thanks for removing that instance. I put it in while messing around with things earlier and intended to cut it but forgot. |
themathqueen
commented
Jun 5, 2026
…m...but I need to finish and rearrange...
…hese as variants of B.flip rather than B, since this was what we did for `PolarTopology.bilin`, but this leads to the `IsCompatibleDual` instances requiring an extra flip...so I'm not sure we shouldn't go back and change these all to be about B and not B.flip.
…trongStar.bilin` into `Ultrastrong.pairing` and `UltrastrongStar.pairing`...perhaps we have that `bilin` is the flip of `pairing` throughout these files? Maybe that needs more clarity?
…transparency level (or the correct def, for that matter, since Jireh was uneasy about the uniformities.)
themathqueen
commented
Jun 17, 2026
| @@ -128,7 +128,7 @@ lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily := | |||
| { topology_eq_withSeminorms := rfl } | |||
|
|
|||
| @[expose] | |||
Collaborator
Author
There was a problem hiding this comment.
Aren't instances already exposed? Is there any need for @[expose]?
Collaborator
There was a problem hiding this comment.
I actually don't know this...although it makes sense that they should be! Let me remove this and then check if I can see an instance in another file with this one as an import...
Collaborator
There was a problem hiding this comment.
No I guess I don't have to do that...all of our other instances here don't have the @[expose] tag, so it must be what you are saying is true. Please let me know if I'm wrong!
…se from the individual seminorms, and added the needed IsUniformAddGroup instances needed to support this.
…so sure it's the right way to go...got to get back on the horse, here.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
wip