feat(ring_theory/ideal_over): lemmas for nonzero ideals lying over no…

…nzero ideals (#3385)

Let `f` be a ring homomorphism from `R` to `S` and `I` be an ideal in `S`. To show that `I.comap f` is not the zero ideal, we can show `I` contains a non-zero root of some non-zero polynomial `p : polynomial R`. As a corollary, if `S` is algebraic over `R` (e.g. the integral closure of `R`), nonzero ideals in `S` lie over nonzero ideals in `R`.

I created a new file because `integral_closure.comap_ne_bot` depends on `comap_ne_bot_of_algebraic_mem`, but `ring_theory/algebraic.lean` imports `ring_theory/integral_closure.lean` and I didn't see any obvious join in the dependency graph where they both belonged.



Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

src/linear_algebra/basic.lean

@@ -438,6 +438,13 @@ instance : order_bot (submodule R M) :=
   bot_le := λ p x, by simp {contextual := tt},
   ..submodule.partial_order }
 
+protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
+⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
+  λ h, eq_bot_iff.mpr (λ x hx, (mem_bot R).mpr (h x hx)) ⟩
+
+protected lemma ne_bot_iff (p : submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M) :=
+by { haveI := classical.prop_decidable, simp_rw [ne.def, p.eq_bot_iff, not_forall] }
+
 /-- The universal set is the top element of the lattice of submodules. -/
 instance : has_top (submodule R M) :=
 ⟨{ carrier := univ, smul_mem' := λ _ _ _, trivial, .. (⊤ : add_submonoid M)}⟩

src/ring_theory/ideal_over.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2020 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Anne Baanen
+-/
+
+import ring_theory.algebraic
+
+/-!
+# Ideals over/under ideals
+
+This file concerns ideals lying over other ideals.
+Let `f : R →+* S` be a ring homomorphism (typically a ring extension), `I` an ideal of `R` and
+`J` an ideal of `S`. We say `J` lies over `I` (and `I` under `J`) if `I` is the `f`-preimage of `J`.
+This is expressed here by writing `I = J.comap f`.
+-/
+
+variables {R : Type*} [comm_ring R]
+
+namespace ideal
+
+open polynomial
+open submodule
+
+section comm_ring
+variables {S : Type*} [comm_ring S] {f : R →+* S} {I : ideal S}
+
+lemma coeff_zero_mem_comap_of_root_mem {r : S} (hr : r ∈ I) {p : polynomial R}
+  (hp : p.eval₂ f r = 0) : p.coeff 0 ∈ I.comap f :=
+begin
+  rw [←p.div_X_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp,
+  refine mem_comap.mpr ((I.add_mem_iff_right _).mp (by simpa only [←hp] using I.zero_mem)),
+  exact I.mul_mem_left hr
+end
+end comm_ring
+
+section integral_domain
+variables {S : Type*} [integral_domain S] {f : R →+* S} {I : ideal S}
+
+lemma exists_coeff_ne_zero_mem_comap_of_root_mem {r : S} (r_ne_zero : r ≠ 0) (hr : r ∈ I)
+  {p : polynomial R} : ∀ (p_ne_zero : p ≠ 0) (hp : p.eval₂ f r = 0),
+  ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ I.comap f :=
+begin
+  refine p.rec_on_horner _ _ _,
+  { intro h, contradiction },
+  { intros p a coeff_eq_zero a_ne_zero ih p_ne_zero hp,
+    refine ⟨0, _, coeff_zero_mem_comap_of_root_mem hr hp⟩,
+    simp [coeff_eq_zero, a_ne_zero] },
+  { intros p p_nonzero ih mul_nonzero hp,
+    rw [eval₂_mul, eval₂_X, mul_eq_zero] at hp,
+    obtain ⟨i, hi, mem⟩ := ih p_nonzero (or.resolve_right hp r_ne_zero),
+    refine ⟨i + 1, _, _⟩; simp [hi, mem] }
+end
+
+lemma comap_ne_bot_of_root_mem {r : S} (r_ne_zero : r ≠ 0) (hr : r ∈ I)
+  {p : polynomial R} (p_ne_zero : p ≠ 0) (hp : p.eval₂ f r = 0) :
+  I.comap f ≠ ⊥ :=
+λ h, let ⟨i, hi, mem⟩ := exists_coeff_ne_zero_mem_comap_of_root_mem r_ne_zero hr p_ne_zero hp in
+absurd ((mem_bot _).mp (eq_bot_iff.mp h mem)) hi
+
+variables [algebra R S]
+
+lemma comap_ne_bot_of_algebraic_mem {I : ideal S} {x : S}
+  (x_ne_zero : x ≠ 0) (x_mem : x ∈ I) (hx : is_algebraic R x) : I.comap (algebra_map R S) ≠ ⊥ :=
+let ⟨p, p_ne_zero, hp⟩ := hx
+in comap_ne_bot_of_root_mem x_ne_zero x_mem p_ne_zero hp
+
+lemma comap_ne_bot_of_integral_mem [nontrivial R] {I : ideal S} {x : S}
+  (x_ne_zero : x ≠ 0) (x_mem : x ∈ I) (hx : is_integral R x) : I.comap (algebra_map R S) ≠ ⊥ :=
+comap_ne_bot_of_algebraic_mem x_ne_zero x_mem (hx.is_algebraic R)
+
+lemma integral_closure.comap_ne_bot [nontrivial R] {I : ideal (integral_closure R S)}
+  (I_ne_bot : I ≠ ⊥) : I.comap (algebra_map R (integral_closure R S)) ≠ ⊥ :=
+let ⟨x, x_mem, x_ne_zero⟩ := I.ne_bot_iff.mp I_ne_bot in
+comap_ne_bot_of_integral_mem x_ne_zero x_mem (integral_closure.is_integral x)
+
+lemma integral_closure.eq_bot_of_comap_eq_bot [nontrivial R] {I : ideal (integral_closure R S)} :
+  I.comap (algebra_map R (integral_closure R S)) = ⊥ → I = ⊥ :=
+imp_of_not_imp_not _ _ integral_closure.comap_ne_bot
+
+end integral_domain
+
+end ideal

src/ring_theory/integral_closure.lean

@@ -235,6 +235,14 @@ theorem mem_integral_closure_iff_mem_fg {r : A} :
 ⟨λ hr, ⟨algebra.adjoin R {r}, fg_adjoin_singleton_of_integral _ hr, algebra.subset_adjoin rfl⟩,
 λ ⟨M, Hf, hrM⟩, is_integral_of_mem_of_fg M Hf _ hrM⟩
 
+variables {R} {A}
+
+lemma integral_closure.is_integral (x : integral_closure R A) : is_integral R x :=
+exists_imp_exists
+  (λ p, and.imp_right (λ hp, show aeval R (integral_closure R A) x p = 0,
+    from subtype.ext (trans (p.hom_eval₂ _ (integral_closure R A).val.to_ring_hom x) hp)))
+  x.2
+
 theorem integral_closure_idem : integral_closure (integral_closure R A : set A) A = ⊥ :=
 begin
   rw eq_bot_iff, intros r hr,