feat(ring_theory/*): Various lemmas used to prove classical nullstell…

…ensatz (#5632)

src/field_theory/mv_polynomial.lean

@@ -7,6 +7,7 @@ Multivariate functions of the form `α^n → α` are isomorphic to multivariate
 `n` variables.
 -/
 
+import ring_theory.ideal.operations
 import linear_algebra.finsupp_vector_space
 import algebra.char_p.basic
 
@@ -23,6 +24,17 @@ variables {σ : Type u} {α : Type v}
 
 section
 variables (σ α) [field α] (m : ℕ)
+
+lemma quotient_mk_comp_C_injective (I : ideal (mv_polynomial σ α)) (hI : I ≠ ⊤) :
+  function.injective ((ideal.quotient.mk I).comp mv_polynomial.C) :=
+begin
+  refine (ring_hom.injective_iff _).2 (λ x hx, _),
+  rw [ring_hom.comp_apply, ideal.quotient.eq_zero_iff_mem] at hx,
+  refine classical.by_contradiction (λ hx0, absurd (I.eq_top_iff_one.2 _) hI),
+  have := I.smul_mem (mv_polynomial.C x⁻¹) hx,
+  rwa [smul_eq_mul, ← mv_polynomial.C.map_mul, inv_mul_cancel hx0, mv_polynomial.C_1] at this,
+end
+
 def restrict_total_degree : submodule α (mv_polynomial σ α) :=
 finsupp.supported _ _ {n | n.sum (λn e, e) ≤ m }
 

src/ring_theory/ideal/operations.lean

@@ -392,7 +392,7 @@ theorem radical_mono (H : I ≤ J) : radical I ≤ radical J :=
 λ r ⟨n, hrni⟩, ⟨n, H hrni⟩
 
 variables (I)
-theorem radical_idem : radical (radical I) = radical I :=
+@[simp] theorem radical_idem : radical (radical I) = radical I :=
 le_antisymm (λ r ⟨n, k, hrnki⟩, ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩) le_radical
 variables {I}
 
@@ -976,6 +976,11 @@ calc I = comap f (map f I) : ((rel_iso_of_bijective f hf).right_inv I).symm
 
 end bijective
 
+lemma ring_equiv.bot_maximal_iff (e : R ≃+* S) :
+  (⊥ : ideal R).is_maximal ↔ (⊥ : ideal S).is_maximal :=
+⟨λ h, (@map_bot _ _ _ _ e.to_ring_hom) ▸ map.is_maximal e.to_ring_hom e.bijective h,
+  λ h, (@map_bot _ _ _ _ e.symm.to_ring_hom) ▸ map.is_maximal e.symm.to_ring_hom e.symm.bijective h⟩
+
 end map_and_comap
 
 section is_primary

src/ring_theory/jacobson_ideal.lean

@@ -41,7 +41,7 @@ Jacobson, Jacobson radical, Local Ideal
 universes u v
 
 namespace ideal
-variables {R : Type u} [comm_ring R]
+variables {R : Type u} [comm_ring R] {I : ideal R}
 variables {S : Type v} [comm_ring S]
 
 section jacobson
@@ -50,36 +50,38 @@ section jacobson
 def jacobson (I : ideal R) : ideal R :=
 Inf {J : ideal R | I ≤ J ∧ is_maximal J}
 
-lemma le_jacobson {I : ideal R} : I ≤ jacobson I :=
+lemma le_jacobson : I ≤ jacobson I :=
 λ x hx, mem_Inf.mpr (λ J hJ, hJ.left hx)
 
-lemma radical_le_jacobson {I : ideal R} : radical I ≤ jacobson I :=
+@[simp] lemma jacobson_idem : jacobson (jacobson I) = jacobson I :=
+le_antisymm (Inf_le_Inf (λ J hJ, ⟨Inf_le hJ, hJ.2⟩)) le_jacobson
+
+lemma radical_le_jacobson : radical I ≤ jacobson I :=
 le_Inf (λ J hJ, (radical_eq_Inf I).symm ▸ Inf_le ⟨hJ.left, is_maximal.is_prime hJ.right⟩)
 
-lemma eq_radical_of_eq_jacobson {I : ideal R} : jacobson I = I → radical I = I :=
+lemma eq_radical_of_eq_jacobson : jacobson I = I → radical I = I :=
 λ h, le_antisymm (le_trans radical_le_jacobson (le_of_eq h)) le_radical
 
 @[simp] lemma jacobson_top : jacobson (⊤ : ideal R) = ⊤ :=
 eq_top_iff.2 le_jacobson
 
-@[simp] theorem jacobson_eq_top_iff {I : ideal R} : jacobson I = ⊤ ↔ I = ⊤ :=
+@[simp] theorem jacobson_eq_top_iff : jacobson I = ⊤ ↔ I = ⊤ :=
 ⟨λ H, classical.by_contradiction $ λ hi, let ⟨M, hm, him⟩ := exists_le_maximal I hi in
   lt_top_iff_ne_top.1 (lt_of_le_of_lt (show jacobson I ≤ M, from Inf_le ⟨him, hm⟩) $ lt_top_iff_ne_top.2 hm.1) H,
 λ H, eq_top_iff.2 $ le_Inf $ λ J ⟨hij, hj⟩, H ▸ hij⟩
 
-lemma jacobson_eq_bot {I : ideal R} : jacobson I = ⊥ → I = ⊥ :=
+lemma jacobson_eq_bot : jacobson I = ⊥ → I = ⊥ :=
 λ h, eq_bot_iff.mpr (h ▸ le_jacobson)
 
-lemma jacobson_eq_self_of_is_maximal  {I : ideal R} [H : is_maximal I] : I.jacobson = I :=
+lemma jacobson_eq_self_of_is_maximal [H : is_maximal I] : I.jacobson = I :=
 le_antisymm (Inf_le ⟨le_of_eq rfl, H⟩) le_jacobson
 
 @[priority 100]
-instance jacobson.is_maximal {I : ideal R} [H : is_maximal I] : is_maximal (jacobson I) :=
+instance jacobson.is_maximal [H : is_maximal I] : is_maximal (jacobson I) :=
 ⟨λ htop, H.left (jacobson_eq_top_iff.1 htop),
   λ J hJ, H.right _ (lt_of_le_of_lt le_jacobson hJ)⟩
 
-theorem mem_jacobson_iff {I : ideal R} {x : R} :
-  x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z + z - 1 ∈ I :=
+theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z + z - 1 ∈ I :=
 ⟨λ hx y, classical.by_cases
   (assume hxy : I ⊔ span {x * y + 1} = ⊤,
     let ⟨p, hpi, q, hq, hpq⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 hxy) in
@@ -100,7 +102,7 @@ theorem mem_jacobson_iff {I : ideal R} {x : R} :
 
 /-- An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals.
 Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs. -/
-theorem eq_jacobson_iff_Inf_maximal {I : ideal R} :
+theorem eq_jacobson_iff_Inf_maximal :
   I.jacobson = I ↔ ∃ M : set (ideal R), (∀ J ∈ M, is_maximal J ∨ J = ⊤) ∧ I = Inf M :=
 begin
   use λ hI, ⟨{J : ideal R | I ≤ J ∧ J.is_maximal}, ⟨λ _ hJ, or.inl hJ.right, hI.symm⟩⟩,
@@ -113,7 +115,7 @@ begin
   { exact is_top.symm ▸ submodule.mem_top }
 end
 
-theorem eq_jacobson_iff_Inf_maximal' {I : ideal R} :
+theorem eq_jacobson_iff_Inf_maximal' :
   I.jacobson = I ↔ ∃ M : set (ideal R), (∀ (J ∈ M) (K : ideal R), J < K → K = ⊤) ∧ I = Inf M :=
 eq_jacobson_iff_Inf_maximal.trans
   ⟨λ h, let ⟨M, hM⟩ := h in ⟨M, ⟨λ J hJ K hK, or.rec_on (hM.1 J hJ) (λ h, h.2 K hK)
@@ -123,7 +125,7 @@ eq_jacobson_iff_Inf_maximal.trans
 
 /-- An ideal `I` equals its Jacobson radical if and only if every element outside `I`
 also lies outside of a maximal ideal containing `I`. -/
-lemma eq_jacobson_iff_not_mem {I : ideal R} :
+lemma eq_jacobson_iff_not_mem :
   I.jacobson = I ↔ ∀ x ∉ I, ∃ M : ideal R, (I ≤ M ∧ M.is_maximal) ∧ x ∉ M :=
 begin
   split,
@@ -138,7 +140,7 @@ begin
     exact h x hx }
 end
 
-theorem map_jacobson_of_surjective {f : R →+* S} (hf : function.surjective f) {I : ideal R} :
+theorem map_jacobson_of_surjective {f : R →+* S} (hf : function.surjective f) :
   ring_hom.ker f ≤ I → map f (I.jacobson) = (map f I).jacobson :=
 begin
   intro h,
@@ -155,7 +157,7 @@ begin
     { exact set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩ } },
 end
 
-lemma map_jacobson_of_bijective {f : R →+* S} (hf : function.bijective f) {I : ideal R} :
+lemma map_jacobson_of_bijective {f : R →+* S} (hf : function.bijective f) :
   map f (I.jacobson) = (map f I).jacobson :=
 map_jacobson_of_surjective hf.right
   (le_trans (le_of_eq (f.injective_iff_ker_eq_bot.1 hf.left)) bot_le)
@@ -192,7 +194,7 @@ lemma mem_jacobson_bot {x : R} : x ∈ jacobson (⊥ : ideal R) ↔ ∀ y, is_un
 
 /-- An ideal `I` of `R` is equal to its Jacobson radical if and only if
 the Jacobson radical of the quotient ring `R/I` is the zero ideal -/
-theorem jacobson_eq_iff_jacobson_quotient_eq_bot {I : ideal R} :
+theorem jacobson_eq_iff_jacobson_quotient_eq_bot :
   I.jacobson = I ↔ jacobson (⊥ : ideal (I.quotient)) = ⊥ :=
 begin
   have hf : function.surjective (quotient.mk I) := submodule.quotient.mk_surjective I,
@@ -209,7 +211,7 @@ end
 
 /-- The standard radical and Jacobson radical of an ideal `I` of `R` are equal if and only if
 the nilradical and Jacobson radical of the quotient ring `R/I` coincide -/
-theorem radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot {I : ideal R} :
+theorem radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot :
   I.radical = I.jacobson ↔ radical (⊥ : ideal (I.quotient)) = jacobson ⊥ :=
 begin
   have hf : function.surjective (quotient.mk I) := submodule.quotient.mk_surjective I,
@@ -232,6 +234,11 @@ begin
   exact λ K ⟨hK, hK_max⟩, hx ⟨trans h hK, hK_max⟩
 end
 
+lemma jacobson_radical_eq_jacobson :
+  I.radical.jacobson = I.jacobson :=
+le_antisymm (le_trans (le_of_eq (congr_arg jacobson (radical_eq_Inf I)))
+  (Inf_le_Inf (λ J hJ, ⟨Inf_le ⟨hJ.1, hJ.2.is_prime⟩, hJ.2⟩))) (jacobson_mono le_radical)
+
 end jacobson
 
 section polynomial

src/ring_theory/polynomial/basic.lean

@@ -720,6 +720,17 @@ instance {R : Type u} {σ : Type v} [integral_domain R] :
   end⟩,
   .. (by apply_instance : comm_ring (mv_polynomial σ R)) }
 
+lemma map_mv_polynomial_eq_eval₂ {S : Type*} [comm_ring S] [fintype σ]
+  (ϕ : mv_polynomial σ R →+* S) (p : mv_polynomial σ R) :
+  ϕ p = mv_polynomial.eval₂ (ϕ.comp mv_polynomial.C) (λ s, ϕ (mv_polynomial.X s)) p :=
+begin
+  refine trans (congr_arg ϕ (mv_polynomial.as_sum p)) _,
+  rw [mv_polynomial.eval₂_eq', ϕ.map_sum],
+  congr,
+  ext,
+  simp only [monomial_eq, ϕ.map_pow, ϕ.map_prod, ϕ.comp_apply, ϕ.map_mul, finsupp.prod_pow],
+end
+
 end mv_polynomial
 
 namespace polynomial