Localization algebra #1007
Merged
Localization algebra #1007
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
felixwellen
requested changes
Jun 9, 2023
|
Checking the library took 47min in the CI, we should investigate. |
|
Both master and this branch take 27min on my machine, so it should be fine. |
jpoiret
force-pushed
the
localization-algebra
branch
from
4aa8a22 to
fc4fcab
Compare
felixwellen
requested changes
Jul 5, 2023
jpoiret
force-pushed
the
localization-algebra
branch
from
fc4fcab to
54050ab
Compare
jpoiret
force-pushed
the
localization-algebra
branch
from
54050ab to
29b7fb5
Compare
|
Great - thanks! |
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.
Hi,
This is an attempt to define the localization of an algebra at an arbitrary multiplicatively closed subset of it, compared with the current localization at a multiplicatively closed subset of the base ring. I've had many attempts, trying to use CT and the fact that algebras over a base ring are equivalent to rings under a base ring, but the definitional behavior was really hard to predict and things just didn't compute well. I chose instead to just extend the existing construction in the most straightforward way. I'm still trying to formulate a recursion principle using the universal property, so that we're able to prove things about the localization without resorting to its actual construction.
This depends on a rebased version of #931.
LMKWYT