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: zeroLocus_span and some simp attributes #6650
Conversation
ChrisHughes24
commented
Aug 18, 2023
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.
While you're at it, could you change the proof of zeroLocus_vanishingIdeal_galoisConnection
to:
theorem zeroLocus_vanishingIdeal_galoisConnection :
@GaloisConnection (Ideal (MvPolynomial σ k)) (Set (σ → k))ᵒᵈ _ _ zeroLocus vanishingIdeal :=
GaloisConnection.monotone_intro (fun _ _ ↦ vanishingIdeal_anti_mono)
(fun _ _ ↦ zeroLocus_anti_mono) le_vanishingIdeal_zeroLocus zeroLocus_vanishingIdeal_le
I also feel like it would be nice to state the Galois connection lemma without mentioning GaloisConnection
for rewriting (it would allow to simplify again the proof that I suggest below by using rw
), would you mind doing that?
Thanks!
bors d+
Set.Subset.antisymm | ||
(fun _ hx _ hp => hx _ (Ideal.subset_span hp)) | ||
(zeroLocus_vanishingIdeal_galoisConnection.l_le <| | ||
Ideal.span_le.2 <| fun _ hp _ hx => hx _ hp) |
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.
Set.Subset.antisymm | |
(fun _ hx _ hp => hx _ (Ideal.subset_span hp)) | |
(zeroLocus_vanishingIdeal_galoisConnection.l_le <| | |
Ideal.span_le.2 <| fun _ hp _ hx => hx _ hp) | |
eq_of_forall_le_iff fun _ ↦ (zeroLocus_vanishingIdeal_galoisConnection _ _).trans <| | |
Ideal.span_le.trans forall₂_swap |
✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |