-
Notifications
You must be signed in to change notification settings - Fork 138
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The Structure Sheaf #941
The Structure Sheaf #941
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great stuff! Some minor suggestions, discussed IRL
open CommRingStr | ||
private | ||
A = fst Aφ | ||
froToCommRingPath : CommAlgebra→CommRing (toCommAlg Aφ) ≡ fst Aφ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not a great name and also in another PR?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
fst Aφ
is just A
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah something similar is done in #931
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Did you decide what to do about this? Maybe just a better name is sufficient?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I went with CommAlgebra→CommRing≡
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe @MatthiasHu can fix his PR once this is merged and figure out what broke in his proposal
OK, hope the checks pass and the PR is ready to merge now. |
In this PR we construct the structure sheaf on the Zariski lattice of a commutative ring and prove the sheaf property.
This builds on #929 but diverges a bit, so it might be best to close that PR.
The older and weaker "pullback" version can probably be removed now.