adding zeroLocusACompl_mem lemma

Author: Danelnov

WeakNullstellensatz/Basic.lean

@@ -3,8 +3,9 @@ import Mathlib.RingTheory.Ideal.Span
 
 open MvPolynomial
 open Ideal
+open Classical
 
-section UPoly
+public section UPoly
 
 variable {R σ : Type*} [CommRing R]
 
@@ -25,7 +26,7 @@ lemma eval_u_poly {i : σ} {A : Finset R} (x : σ → R)
 
 /-- A polynomial f is in the ideal generated by the u_polys iff f vanishes on all points
     whose coordinates lie in the given finite set A. -/
-theorem mem_ideal_U_iff [Fintype σ] [IsDomain R] [DecidableEq σ]
+theorem mem_ideal_U_iff [Fintype σ] [IsDomain R]
     (A : Finset R) (f : MvPolynomial σ R) :
     f ∈ ideal_U A ↔ ∀ (x : σ → R), (∀ (i : σ), x i ∈ A) → f.eval x = 0 := by
   rw [ideal_U, mem_span_range_iff_exists_fun]
@@ -54,20 +55,52 @@ theorem mem_ideal_U_iff [Fintype σ] [IsDomain R] [DecidableEq σ]
       simp [Finsupp.linearCombination_apply, Finsupp.sum_fintype] at h2
       exact h2.symm
 
+
 end UPoly
 
-section Field
 
-variable {K σ : Type*} [Field K] [Fintype K]
+variable {K σ : Type*} [Field K] (A : Finset K) (I : Ideal (MvPolynomial σ K))
 
-def zeroLocusA (A : Finset K) (I : Ideal (MvPolynomial σ K)) : Set (σ → K) :=
-  zeroLocus K I ∩ {x | ∀ i , x i ∈ A}
 
+def zeroLocusA : Set (σ → K) :=
+  zeroLocus K I ∩ {x : σ → K | ∀ i , x i ∈ A}
 
-example (A : Finset K) (I : Ideal (MvPolynomial σ K)) :
-    vanishingIdeal K (zeroLocusA A I) = I + ideal_U A := by
-  sorry
+
+def zeroLocusACompl : Set (σ → K) :=
+  {x : σ → K | ∀ i, x i ∈ A} \ (zeroLocusA A I)
 
 
+lemma zeroLocusACompl_mem
+    (x : σ → K) (S : Finset (MvPolynomial σ K)) (hI : I = Ideal.span S) :
+    x ∈ zeroLocusACompl A I → ∃ p ∈ S, p.eval x ≠ 0 := by
+  intro hx
+  simp [zeroLocusACompl, zeroLocusA, hI] at hx ⊢
+  have ⟨hx, ⟨g, ⟨hg, hgx⟩⟩⟩ := hx
+  induction hg using Submodule.span_induction with
+  | mem p hp =>
+    use p; exact ⟨hp, hgx⟩
+  | zero => aesop
+  | add p₁ p₂ _ _ ih₁ ih₂ =>
+    simp at hgx
+    by_cases h : (p₁.eval x) = 0
+    . simp [h] at hgx
+      exact ih₂ hgx
+    . exact ih₁ h
+  | smul p₁ p₂ _ ih =>
+    by_cases h : (p₂.eval x) = 0
+    . simp [h] at hgx
+    . exact ih h
 
-end Field
+
+example [Fintype σ] [Fintype K] (A : Finset K) (I : Ideal (MvPolynomial σ K)) :
+    vanishingIdeal K (zeroLocusA A I) = I + ideal_U A := by
+  ext p
+  simp [zeroLocusA, Submodule.mem_sup]
+  constructor <;> intro hp
+  . sorry
+  . intro x hx
+    obtain ⟨f, hf, g, hg, hp⟩ := hp
+    rw [← hp, eval_add]
+    simp_all
+    apply (mem_ideal_U_iff A g).mp
+    exact hg