From 0dd146c23431d3352d5c576cd8c19f0fcff29cc8 Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Sat, 19 Aug 2023 08:16:42 +0000
Subject: [PATCH] feat: zeroLocus_span and some simp attributes (#6650)

---
 Mathlib/RingTheory/Nullstellensatz.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/Nullstellensatz.lean b/Mathlib/RingTheory/Nullstellensatz.lean
index f40a29de81986..85abdfdb660a7 100644
--- a/Mathlib/RingTheory/Nullstellensatz.lean
+++ b/Mathlib/RingTheory/Nullstellensatz.lean
@@ -52,10 +52,12 @@ theorem zeroLocus_anti_mono {I J : Ideal (MvPolynomial σ k)} (h : I ≤ J) :
     zeroLocus J ≤ zeroLocus I := fun _ hx p hp => hx p <| h hp
 #align mv_polynomial.zero_locus_anti_mono MvPolynomial.zeroLocus_anti_mono
 
+@[simp]
 theorem zeroLocus_bot : zeroLocus (⊥ : Ideal (MvPolynomial σ k)) = ⊤ :=
   eq_top_iff.2 fun x _ _ hp => Trans.trans (congr_arg (eval x) (mem_bot.1 hp)) (eval x).map_zero
 #align mv_polynomial.zero_locus_bot MvPolynomial.zeroLocus_bot
 
+@[simp]
 theorem zeroLocus_top : zeroLocus (⊤ : Ideal (MvPolynomial σ k)) = ⊥ :=
   eq_bot_iff.2 fun x hx => one_ne_zero ((eval x).map_one ▸ hx 1 Submodule.mem_top : (1 : k) = 0)
 #align mv_polynomial.zero_locus_top MvPolynomial.zeroLocus_top
@@ -93,11 +95,19 @@ theorem zeroLocus_vanishingIdeal_le (V : Set (σ → k)) : V ≤ zeroLocus (vani
 
 theorem zeroLocus_vanishingIdeal_galoisConnection :
     @GaloisConnection (Ideal (MvPolynomial σ k)) (Set (σ → k))ᵒᵈ _ _ zeroLocus vanishingIdeal :=
-  fun I V =>
-  ⟨fun h => le_trans (le_vanishingIdeal_zeroLocus I) (vanishingIdeal_anti_mono h), fun h =>
-    le_trans (zeroLocus_anti_mono h) (zeroLocus_vanishingIdeal_le V)⟩
+  GaloisConnection.monotone_intro (fun _ _ ↦ vanishingIdeal_anti_mono)
+    (fun _ _ ↦ zeroLocus_anti_mono) le_vanishingIdeal_zeroLocus zeroLocus_vanishingIdeal_le
 #align mv_polynomial.zero_locus_vanishing_ideal_galois_connection MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection
 
+theorem le_zeroLocus_iff_le_vanishingIdeal {V : Set (σ → k)} {I : Ideal (MvPolynomial σ k)} :
+    V ≤ zeroLocus I ↔ I ≤ vanishingIdeal V :=
+  zeroLocus_vanishingIdeal_galoisConnection.le_iff_le
+
+theorem zeroLocus_span (S : Set (MvPolynomial σ k)) :
+    zeroLocus (Ideal.span S) = { x | ∀ p ∈ S, eval x p = 0 } :=
+  eq_of_forall_le_iff fun _ => le_zeroLocus_iff_le_vanishingIdeal.trans <|
+    Ideal.span_le.trans forall₂_swap
+
 theorem mem_vanishingIdeal_singleton_iff (x : σ → k) (p : MvPolynomial σ k) :
     p ∈ (vanishingIdeal {x} : Ideal (MvPolynomial σ k)) ↔ eval x p = 0 :=
   ⟨fun h => h x rfl, fun hpx _ hy => hy.symm ▸ hpx⟩