[Merged by Bors] - feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials #5520
Conversation
…polynomial ring proofs
dtumad
changed the title
bryangingechen
added
the
awaiting-review
There was a problem hiding this comment.
The code looks good!
I'm wondering how easy it would be to "generalize" your results from "for all maximal ideals, the quotient map ..." to "for all ring homs that are surjective onto a field, ...". (Even though they should be equivalent, the latter contains more free variables in its conclusion: it might be easier to use in practice.) Have you considered the surjective map case already?
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
I think this is possible to do, but the trouble I had is that the proof needs to derive that certain other rings are actually fields by pulling across the homomorphisms, and the interface for |
There was a problem hiding this comment.
I'm hqppy with merging this as it currently stands, and deriving the "surjective to a field" conclusion later, since it needs more work in other parts.
@jcommelin, what do you think?
|
@Vierkantor I realized there are much simpler proofs to the field surjection versions of the lemmas than the proofs I was picturing. I've just added them to this PR since they don't actually require many other changes elsewhere. |
|
Fantastic 😄 |
github-actions
bot
added
ready-to-merge
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
|
Build failed (retrying...): |
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
|
Build failed (retrying...): |
…d polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. `is_integral_localization_map_polynomial_quotient` already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. `polynomial.quotient_mk_comp_C_is_integral_of_jacobson` and `mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson` are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems. Co-authored-by: Devon Tuma <dtumad@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct.
is_integral_localization_map_polynomial_quotientalready exists in the proof of a previous theorem, and this just pulls it out into an independent lemma.polynomial.quotient_mk_comp_C_is_integral_of_jacobsonandmv_polynomial.quotient_mk_comp_C_is_integral_of_jacobsonare the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems.