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
[Merged by Bors] - feat(ring_theory/henselian): Henselian local rings #8986
Conversation
jcommelin
commented
Sep 3, 2021
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - feat(ring_theory/ideal/operations): ring_hom.ker_is_maximal_of_surjective #8990
- depends on: [Merged by Bors] - feat(ring_theory/ideal/local_ring): residue field is an algebra #8991
- depends on: [Merged by Bors] - feat(linear_algebra/smodeq): sub_mem, eval #8993
- depends on: [Merged by Bors] - feat(ring_theory/ideal/operations): ideal.pow_mem_pow #8996
- depends on: [Merged by Bors] - feat(data/polynomial/taylor): Taylor expansion of polynomials #9000
- depends on: [Merged by Bors] - feat(linear_algebra/adic_completion): le_jacobson_bot #9125
Also, the kernel of a surjective map to a field is equal to the unique maximal ideal.
…l coefficients I place this identity in a new file because the current proof depends on `polynomial`.
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
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.
LGTM!
I'll let @eric-wieser see if he's happy with the unit
stuff before merging.
|
||
open local_ring polynomial function | ||
|
||
lemma is_local_ring_hom_of_le_jacobson_bot {R : Type*} [comm_ring R] |
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.
An argument can be made that this should go in ring_theory.jacobson_ideal
, but is_local_ring_hom
isn't imported there. I don't mind either way, to be honest.
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 agree. At some point it will move to a proper home.
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.
The names for the new lemmas aren't what I'd expect
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.
Well done for getting through this proof!
bors r+ |
Pull request successfully merged into master. Build succeeded: |