bump to nightly-2023-07-04-17

mathlib commit leanprover-community/mathlib@728ef9d

Mathbin/RingTheory/Nullstellensatz.lean

@@ -40,29 +40,40 @@ variable {k : Type _} [Field k]
 
 variable {σ : Type _}
 
+#print MvPolynomial.zeroLocus /-
 /-- Set of points that are zeroes of all polynomials in an ideal -/
 def zeroLocus (I : Ideal (MvPolynomial σ k)) : Set (σ → k) :=
   {x : σ → k | ∀ p ∈ I, eval x p = 0}
 #align mv_polynomial.zero_locus MvPolynomial.zeroLocus
+-/
 
+#print MvPolynomial.mem_zeroLocus_iff /-
 @[simp]
 theorem mem_zeroLocus_iff {I : Ideal (MvPolynomial σ k)} {x : σ → k} :
     x ∈ zeroLocus I ↔ ∀ p ∈ I, eval x p = 0 :=
   Iff.rfl
 #align mv_polynomial.mem_zero_locus_iff MvPolynomial.mem_zeroLocus_iff
+-/
 
+#print MvPolynomial.zeroLocus_anti_mono /-
 theorem zeroLocus_anti_mono {I J : Ideal (MvPolynomial σ k)} (h : I ≤ J) :
     zeroLocus J ≤ zeroLocus I := fun x hx p hp => hx p <| h hp
 #align mv_polynomial.zero_locus_anti_mono MvPolynomial.zeroLocus_anti_mono
+-/
 
+#print MvPolynomial.zeroLocus_bot /-
 theorem zeroLocus_bot : zeroLocus (⊥ : Ideal (MvPolynomial σ k)) = ⊤ :=
   eq_top_iff.2 fun x hx p hp => trans (congr_arg (eval x) (mem_bot.1 hp)) (eval x).map_zero
 #align mv_polynomial.zero_locus_bot MvPolynomial.zeroLocus_bot
+-/
 
+#print MvPolynomial.zeroLocus_top /-
 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
+-/
 
+#print MvPolynomial.vanishingIdeal /-
 /-- Ideal of polynomials with common zeroes at all elements of a set -/
 def vanishingIdeal (V : Set (σ → k)) : Ideal (MvPolynomial σ k)
     where
@@ -72,41 +83,57 @@ def vanishingIdeal (V : Set (σ → k)) : Ideal (MvPolynomial σ k)
   smul_mem' p q hq x hx := by
     simp only [hq x hx, Algebra.id.smul_eq_mul, MulZeroClass.mul_zero, RingHom.map_mul]
 #align mv_polynomial.vanishing_ideal MvPolynomial.vanishingIdeal
+-/
 
+#print MvPolynomial.mem_vanishingIdeal_iff /-
 @[simp]
 theorem mem_vanishingIdeal_iff {V : Set (σ → k)} {p : MvPolynomial σ k} :
     p ∈ vanishingIdeal V ↔ ∀ x ∈ V, eval x p = 0 :=
   Iff.rfl
 #align mv_polynomial.mem_vanishing_ideal_iff MvPolynomial.mem_vanishingIdeal_iff
+-/
 
+#print MvPolynomial.vanishingIdeal_anti_mono /-
 theorem vanishingIdeal_anti_mono {A B : Set (σ → k)} (h : A ≤ B) :
     vanishingIdeal B ≤ vanishingIdeal A := fun p hp x hx => hp x <| h hx
 #align mv_polynomial.vanishing_ideal_anti_mono MvPolynomial.vanishingIdeal_anti_mono
+-/
 
+#print MvPolynomial.vanishingIdeal_empty /-
 theorem vanishingIdeal_empty : vanishingIdeal (∅ : Set (σ → k)) = ⊤ :=
   le_antisymm le_top fun p hp x hx => absurd hx (Set.not_mem_empty x)
 #align mv_polynomial.vanishing_ideal_empty MvPolynomial.vanishingIdeal_empty
+-/
 
+#print MvPolynomial.le_vanishingIdeal_zeroLocus /-
 theorem le_vanishingIdeal_zeroLocus (I : Ideal (MvPolynomial σ k)) :
     I ≤ vanishingIdeal (zeroLocus I) := fun p hp x hx => hx p hp
 #align mv_polynomial.le_vanishing_ideal_zero_locus MvPolynomial.le_vanishingIdeal_zeroLocus
+-/
 
+#print MvPolynomial.zeroLocus_vanishingIdeal_le /-
 theorem zeroLocus_vanishingIdeal_le (V : Set (σ → k)) : V ≤ zeroLocus (vanishingIdeal V) :=
   fun V hV p hp => hp V hV
 #align mv_polynomial.zero_locus_vanishing_ideal_le MvPolynomial.zeroLocus_vanishingIdeal_le
+-/
 
+#print MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection /-
 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)⟩
 #align mv_polynomial.zero_locus_vanishing_ideal_galois_connection MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection
+-/
 
+#print MvPolynomial.mem_vanishingIdeal_singleton_iff /-
 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 y hy => hy.symm ▸ hpx⟩
 #align mv_polynomial.mem_vanishing_ideal_singleton_iff MvPolynomial.mem_vanishingIdeal_singleton_iff
+-/
 
+#print MvPolynomial.vanishingIdeal_singleton_isMaximal /-
 instance vanishingIdeal_singleton_isMaximal {x : σ → k} :
     (vanishingIdeal {x} : Ideal (MvPolynomial σ k)).IsMaximal :=
   by
@@ -123,7 +150,9 @@ instance vanishingIdeal_singleton_isMaximal {x : σ → k} :
   rw [← bot_quotient_is_maximal_iff, ring_equiv.bot_maximal_iff this]
   exact bot_is_maximal
 #align mv_polynomial.vanishing_ideal_singleton_is_maximal MvPolynomial.vanishingIdeal_singleton_isMaximal
+-/
 
+#print MvPolynomial.radical_le_vanishingIdeal_zeroLocus /-
 theorem radical_le_vanishingIdeal_zeroLocus (I : Ideal (MvPolynomial σ k)) :
     I.radical ≤ vanishingIdeal (zeroLocus I) :=
   by
@@ -136,12 +165,16 @@ theorem radical_le_vanishingIdeal_zeroLocus (I : Ideal (MvPolynomial σ k)) :
           (vanishing_ideal_anti_mono fun y hy => hy.symm ▸ hx),
         is_maximal.is_prime' _⟩
 #align mv_polynomial.radical_le_vanishing_ideal_zero_locus MvPolynomial.radical_le_vanishingIdeal_zeroLocus
+-/
 
+#print MvPolynomial.pointToPoint /-
 /-- The point in the prime spectrum assosiated to a given point -/
 def pointToPoint (x : σ → k) : PrimeSpectrum (MvPolynomial σ k) :=
   ⟨(vanishingIdeal {x} : Ideal (MvPolynomial σ k)), by infer_instance⟩
 #align mv_polynomial.point_to_point MvPolynomial.pointToPoint
+-/
 
+#print MvPolynomial.vanishingIdeal_pointToPoint /-
 @[simp]
 theorem vanishingIdeal_pointToPoint (V : Set (σ → k)) :
     PrimeSpectrum.vanishingIdeal (pointToPoint '' V) = MvPolynomial.vanishingIdeal V :=
@@ -155,17 +188,21 @@ theorem vanishingIdeal_pointToPoint (V : Set (σ → k)) :
       let ⟨x, hx⟩ := hI
       hx.2 ▸ fun x' hx' => (Set.mem_singleton_iff.1 hx').symm ▸ hp x hx.1
 #align mv_polynomial.vanishing_ideal_point_to_point MvPolynomial.vanishingIdeal_pointToPoint
+-/
 
+#print MvPolynomial.pointToPoint_zeroLocus_le /-
 theorem pointToPoint_zeroLocus_le (I : Ideal (MvPolynomial σ k)) :
     pointToPoint '' MvPolynomial.zeroLocus I ≤ PrimeSpectrum.zeroLocus ↑I := fun J hJ =>
   let ⟨x, hx⟩ := hJ
   (le_trans (le_vanishingIdeal_zeroLocus I)
       (hx.2 ▸ vanishingIdeal_anti_mono (Set.singleton_subset_iff.2 hx.1)) :
     I ≤ J.asIdeal)
 #align mv_polynomial.point_to_point_zero_locus_le MvPolynomial.pointToPoint_zeroLocus_le
+-/
 
 variable [IsAlgClosed k] [Finite σ]
 
+#print MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton /-
 theorem isMaximal_iff_eq_vanishingIdeal_singleton (I : Ideal (MvPolynomial σ k)) :
     I.IsMaximal ↔ ∃ x : σ → k, I = vanishingIdeal {x} :=
   by
@@ -191,7 +228,9 @@ theorem isMaximal_iff_eq_vanishingIdeal_singleton (I : Ideal (MvPolynomial σ k)
   rw [mem_vanishing_ideal_singleton_iff, eval_eq'] at hp 
   simpa only [ϕ.map_sum, ϕ.map_mul, ϕ.map_prod, ϕ.map_pow, ϕ.map_zero, hx] using congr_arg ϕ hp
 #align mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton
+-/
 
+#print MvPolynomial.vanishingIdeal_zeroLocus_eq_radical /-
 /-- Main statement of the Nullstellensatz -/
 @[simp]
 theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal (MvPolynomial σ k)) :
@@ -211,12 +250,15 @@ theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal (MvPolynomial σ k)) :
             (vanishing_ideal_anti_mono fun y hy => hy.symm ▸ hx),
           MvPolynomial.vanishingIdeal_singleton_isMaximal⟩
 #align mv_polynomial.vanishing_ideal_zero_locus_eq_radical MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
+-/
 
+#print MvPolynomial.IsPrime.vanishingIdeal_zeroLocus /-
 @[simp]
 theorem IsPrime.vanishingIdeal_zeroLocus (P : Ideal (MvPolynomial σ k)) [h : P.IsPrime] :
     vanishingIdeal (zeroLocus P) = P :=
   trans (vanishingIdeal_zeroLocus_eq_radical P) h.radical
 #align mv_polynomial.is_prime.vanishing_ideal_zero_locus MvPolynomial.IsPrime.vanishingIdeal_zeroLocus
+-/
 
 end MvPolynomial
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "906ac61a5d70d514e968952d8e61f3c9dad8e22b",
+    "rev": "560173be01c0f8c8d968526264f09e3e7dec2817",
     "name": "lean3port",
-    "inputRev?": "906ac61a5d70d514e968952d8e61f3c9dad8e22b"}},
+    "inputRev?": "560173be01c0f8c8d968526264f09e3e7dec2817"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "cb02d09e1d5611d22efc2b406e7893f246b2f51e",
+    "rev": "409bee4eabf8072c4569950c3c2f310afd203abf",
     "name": "mathlib",
-    "inputRev?": "cb02d09e1d5611d22efc2b406e7893f246b2f51e"}},
+    "inputRev?": "409bee4eabf8072c4569950c3c2f310afd203abf"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-07-04-15"
+def tag : String := "nightly-2023-07-04-17"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"906ac61a5d70d514e968952d8e61f3c9dad8e22b"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"560173be01c0f8c8d968526264f09e3e7dec2817"
 
 @[default_target]
 lean_lib Mathbin where