feat(ring_theory/ideal/over): Going up theorem for integral extensions (

#4064)

The main statement is `exists_ideal_over_prime_of_is_integral` which shows that for an integral extension, every prime ideal of the original ring lies under some prime ideal of the extension ring.

`is_field_of_is_integral_of_is_field` is a brute force proof that if `R → S` is an integral extension, and `S` is a field, then `R` is also a field (using the somewhat new `is_field` proposition). `is_maximal_comap_of_is_integral_of_is_maximal` Gives essentially the same statement in terms of maximal ideals.

`disjoint_compl` has also been replaced with `disjoint_compl_left` and `disjoint_compl_right` variants.



Co-authored-by: Devon Tuma <dtumad@gmail.com>

src/data/polynomial/eval.lean

@@ -179,6 +179,10 @@ ring_hom.of (eval₂ f x)
 
 lemma eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n := (eval₂_ring_hom _ _).map_pow _ _
 
+lemma eval₂_eq_sum_range :
+  p.eval₂ f x = ∑ i in finset.range (p.nat_degree + 1), f (p.coeff i) * x^i :=
+trans (congr_arg _ p.as_sum) (trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))
+
 end eval₂
 
 section eval

src/data/set/lattice.lean

@@ -1050,7 +1050,9 @@ ht.sup_right hu
 theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
 disjoint_iff.2 (inter_diff_self _ _)
 
-theorem disjoint_compl (s : set α) : disjoint s sᶜ := assume a ⟨h₁, h₂⟩, h₂ h₁
+theorem disjoint_compl_left (s : set α) : disjoint sᶜ s := assume a ⟨h₁, h₂⟩, h₁ h₂
+
+theorem disjoint_compl_right (s : set α) : disjoint s sᶜ := assume a ⟨h₁, h₂⟩, h₂ h₁
 
 theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
 by simp [set.disjoint_iff, subset_def]; exact iff.rfl

src/linear_algebra/basic.lean

@@ -2486,8 +2486,8 @@ lemma disjoint_std_basis_std_basis (I J : set ι) (h : disjoint I J) :
   disjoint (⨆i∈I, range (std_basis R φ i)) (⨆i∈J, range (std_basis R φ i)) :=
 begin
   refine disjoint.mono
-    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl I)
-    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl J) _,
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl_right I)
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl_right J) _,
   simp only [disjoint, submodule.le_def', mem_infi, mem_inf, mem_ker, mem_bot, proj_apply,
     funext_iff],
   rintros b ⟨hI, hJ⟩ i,

src/linear_algebra/finsupp.lean

@@ -70,8 +70,8 @@ lemma disjoint_lsingle_lsingle (s t : set α) (hs : disjoint s t) :
   disjoint (⨆a∈s, (lsingle a : M →ₗ[R] (α →₀ M)).range) (⨆a∈t, (lsingle a).range) :=
 begin
   refine disjoint.mono
-    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl s)
-    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl t)
+    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right s)
+    (lsingle_range_le_ker_lapply _ _ $ disjoint_compl_right t)
     (le_trans (le_infi $ assume i, _) infi_ker_lapply_le_bot),
   classical,
   by_cases his : i ∈ s,

src/linear_algebra/matrix.lean

@@ -588,7 +588,7 @@ begin
   simp only [comap_infi, (ker_comp _ _).symm, proj_diagonal, ker_smul'],
   have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ, { rw set.union_compl_self },
   exact (supr_range_std_basis_eq_infi_ker_proj K (λi:m, K)
-    (disjoint_compl {i | w i = 0}) this (finite.of_fintype _)).symm
+    (disjoint_compl_right {i | w i = 0}) this (finite.of_fintype _)).symm
 end
 
 lemma range_diagonal [decidable_eq m] (w : m → K) :
@@ -604,7 +604,7 @@ lemma rank_diagonal [decidable_eq m] [decidable_eq K] (w : m → K) :
   rank (diagonal w).to_lin = fintype.card { i // w i ≠ 0 } :=
 begin
   have hu : univ ⊆ {i : m | w i = 0}ᶜ ∪ {i : m | w i = 0}, { rw set.compl_union_self },
-  have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := (disjoint_compl {i | w i = 0}).symm,
+  have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := (disjoint_compl_right {i | w i = 0}).symm,
   have h₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (finite.of_fintype _),
   have h₂ := @infi_ker_proj_equiv K _ _ (λi:m, K) _ _ _ _ (by simp; apply_instance) hd hu,
   rw [rank, range_diagonal, h₁, ←@dim_fun' K],

src/measure_theory/measure_space.lean

@@ -723,7 +723,7 @@ ext $ λ t' ht', restrict_union_apply (h.mono inf_le_right inf_le_right) hs ht h
 
 @[simp] lemma restrict_add_restrict_compl {s : set α} (hs : is_measurable s) :
   μ.restrict s + μ.restrict sᶜ = μ :=
-by rw [← restrict_union (disjoint_compl _) hs hs.compl, union_compl_self, restrict_univ]
+by rw [← restrict_union (disjoint_compl_right _) hs hs.compl, union_compl_self, restrict_univ]
 
 @[simp] lemma restrict_compl_add_restrict {s : set α} (hs : is_measurable s) :
   μ.restrict sᶜ + μ.restrict s = μ :=

src/measure_theory/set_integral.lean

@@ -331,7 +331,7 @@ lemma integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [meas
 
 lemma integral_add_compl (hs : is_measurable s) (hfi : integrable f μ) :
   ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ :=
-by rw [← integral_union (disjoint_compl s) hs hs.compl hfi.integrable_on hfi.integrable_on,
+by rw [← integral_union (disjoint_compl_right s) hs hs.compl hfi.integrable_on hfi.integrable_on,
   union_compl_self, integral_univ]
 
 /-- For a measurable function `f` and a measurable set `s`, the integral of `indicator s f`

src/ring_theory/ideal/operations.lean

@@ -909,6 +909,31 @@ begin
     refine ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_is_prime_of_surjective hf (le_trans h hJ.left)⟩ },
 end
 
+section quotient_algebra
+
+/-- The ring hom `R/f⁻¹(I) →+* S/I` induced by a ring hom `f : R →+* S` -/
+def quotient_map {I : ideal R} (J : ideal S) (f : R →+* S) (hIJ : I ≤ J.comap f) :
+  I.quotient →+* J.quotient :=
+(quotient.lift I ((quotient.mk J).comp f) (λ _ ha,
+  by simpa [function.comp_app, ring_hom.coe_comp, quotient.eq_zero_iff_mem] using hIJ ha))
+
+variables {I : ideal R} {J: ideal S} [algebra R S]
+
+@[priority 100]
+instance quotient_algebra : algebra (J.comap (algebra_map R S)).quotient J.quotient :=
+(quotient_map J (algebra_map R S) (le_of_eq rfl)).to_algebra
+
+lemma algebra_map_quotient_injective :
+  function.injective (algebra_map (J.comap (algebra_map R S)).quotient J.quotient) :=
+begin
+  rintros ⟨a⟩ ⟨b⟩ hab,
+  replace hab := quotient.eq.mp hab,
+  rw ← ring_hom.map_sub at hab,
+  exact quotient.eq.mpr hab
+end
+
+end quotient_algebra
+
 end ideal
 
 namespace submodule

src/ring_theory/ideal/over.lean

@@ -5,6 +5,7 @@ Author: Anne Baanen
 -/
 
 import ring_theory.algebraic
+import ring_theory.localization
 
 /-!
 # Ideals over/under ideals
@@ -143,6 +144,15 @@ lemma is_maximal_of_is_integral_of_is_maximal_comap
   λ J I_lt_J, let ⟨I_le_J, x, hxJ, hxI⟩ := lt_iff_le_and_exists.mp I_lt_J
   in comap_eq_top_iff.mp (hI.2 _ (comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩ (hRS x))) ⟩
 
+lemma is_maximal_comap_of_is_integral_of_is_maximal (hRS_integral : ∀ (x : S), is_integral R x)
+  (I : ideal S) [hI : I.is_maximal] : is_maximal (I.comap (algebra_map R S)) :=
+begin
+  refine quotient.maximal_of_is_field _ _,
+  haveI : is_prime (I.comap (algebra_map R S)) := comap_is_prime _ _,
+  exact is_field_of_is_integral_of_is_field (is_integral_quotient_of_is_integral hRS_integral)
+    algebra_map_quotient_injective (by rwa ← quotient.maximal_ideal_iff_is_field_quotient),
+end
+
 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
@@ -163,6 +173,56 @@ lemma integral_closure.is_maximal_of_is_maximal_comap
   (hI : is_maximal (I.comap (algebra_map R (integral_closure R S)))) : is_maximal I :=
 is_maximal_of_is_integral_of_is_maximal_comap (λ x, integral_closure.is_integral x) I hI
 
+/-- `comap (algebra_map R S)` is a surjection from the prime spec of `R` to prime spec of `S`.
+`hP : (algebra_map R S).ker ≤ P` is a slight generalization of the extension being injective -/
+lemma exists_ideal_over_prime_of_is_integral' (H : ∀ x : S, is_integral R x)
+  (P : ideal R) [is_prime P] (hP : (algebra_map R S).ker ≤ P) :
+  ∃ (Q : ideal S), is_prime Q ∧ P = Q.comap (algebra_map R S) :=
+begin
+  have hP0 : (0 : S) ∉ algebra.algebra_map_submonoid S P.prime_compl,
+  { rintro ⟨x, ⟨hx, x0⟩⟩,
+    exact absurd (hP x0) hx },
+  let Rₚ := localization P.prime_compl,
+  let f := localization.of P.prime_compl,
+  let Sₚ := localization (algebra.algebra_map_submonoid S P.prime_compl),
+  let g := localization.of (algebra.algebra_map_submonoid S P.prime_compl),
+  letI : integral_domain (localization (algebra.algebra_map_submonoid S P.prime_compl)) :=
+    localization_map.integral_domain_localization (le_non_zero_divisors_of_domain hP0),
+  obtain ⟨Qₚ : ideal Sₚ, Qₚ_maximal⟩ := @exists_maximal Sₚ _ (by apply_instance),
+  haveI Qₚ_max : is_maximal (comap _ Qₚ) := @is_maximal_comap_of_is_integral_of_is_maximal Rₚ _ Sₚ _
+    (localization_algebra P.prime_compl f g)
+    (is_integral_localization f g H) _ Qₚ_maximal,
+  refine ⟨comap g.to_map Qₚ, ⟨comap_is_prime g.to_map Qₚ, _⟩⟩,
+  convert localization.at_prime.comap_maximal_ideal.symm,
+  rw [comap_comap, ← local_ring.eq_maximal_ideal Qₚ_max, ← f.map_comp _],
+  refl
+end
+
+/-- More general going-up theorem than `exists_ideal_over_prime_of_is_integral'`.
+TODO: Version of going-up theorem with arbitrary length chains (by induction on this)?
+  Not sure how best to write an ascending chain in Lean -/
+theorem exists_ideal_over_prime_of_is_integral (H : ∀ x : S, is_integral R x)
+  (P : ideal R) [is_prime P] (I : ideal S) [is_prime I] (hIP : I.comap (algebra_map R S) ≤ P) :
+  ∃ Q ≥ I, is_prime Q ∧ P = Q.comap (algebra_map R S) :=
+begin
+  obtain ⟨Q' : ideal I.quotient, ⟨Q'_prime, hQ'⟩⟩ := @exists_ideal_over_prime_of_is_integral'
+    (I.comap (algebra_map R S)).quotient _ I.quotient _
+    ideal.quotient_algebra
+    (is_integral_quotient_of_is_integral H)
+    (map (quotient.mk (I.comap (algebra_map R S))) P)
+    (map_is_prime_of_surjective quotient.mk_surjective (by simp [hIP]))
+    (le_trans
+      (le_of_eq ((ring_hom.injective_iff_ker_eq_bot _).1 algebra_map_quotient_injective))
+      bot_le),
+  haveI := Q'_prime,
+  refine ⟨Q'.comap _, le_trans (le_of_eq mk_ker.symm) (ker_le_comap _), ⟨comap_is_prime _ Q', _⟩⟩,
+  rw comap_comap,
+  refine trans _ (trans (congr_arg (comap (quotient.mk (comap (algebra_map R S) I))) hQ') _),
+  { refine trans ((sup_eq_left.2 _).symm) (comap_map_of_surjective _ quotient.mk_surjective _).symm,
+    simpa [← ring_hom.ker_eq_comap_bot] using hIP},
+  { simpa [comap_comap] },
+end
+
 end integral_domain
 
 end ideal

src/ring_theory/integral_closure.lean

@@ -371,6 +371,57 @@ begin
   exact hp',
 end
 
+lemma is_integral_quotient_of_is_integral {I : ideal A} (hRS : ∀ (x : A), is_integral R x) :
+  ∀ (x : I.quotient), is_integral (I.comap (algebra_map R A)).quotient x :=
+begin
+  rintros ⟨x⟩,
+  obtain ⟨p, ⟨p_monic, hpx⟩⟩ := hRS x,
+  refine ⟨p.map (ideal.quotient.mk _), ⟨monic_map _ p_monic, _⟩⟩,
+  simpa only [aeval_def, hom_eval₂, eval₂_map] using congr_arg (ideal.quotient.mk I) hpx
+end
+
+/-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field -/
+lemma is_field_of_is_integral_of_is_field {R S : Type*} [integral_domain R] [integral_domain S]
+  [algebra R S] (H : ∀ x : S, is_integral R x) (hRS : function.injective (algebra_map R S))
+  (hS : is_field S) : is_field R :=
+begin
+  refine ⟨⟨0, 1, zero_ne_one⟩, mul_comm, λ a ha, _⟩,
+  -- Let `a_inv` be the inverse of `algebra_map R S a`,
+  -- then we need to show that `a_inv` is of the form `algebra_map R S b`.
+  obtain ⟨a_inv, ha_inv⟩ := hS.mul_inv_cancel (λ h, ha (hRS (trans h (ring_hom.map_zero _).symm))),
+
+  -- Let `p : polynomial R` be monic with root `a_inv`,
+  -- and `q` be `p` with coefficients reversed (so `q(a) = q'(a) * a + 1`).
+  -- We claim that `q(a) = 0`, so `-q'(a)` is the inverse of `a`.
+  obtain ⟨p, p_monic, hp⟩ := H a_inv,
+  use -∑ (i : ℕ) in finset.range p.nat_degree, (p.coeff i) * a ^ (p.nat_degree - i - 1),
+
+  -- `q(a) = 0`, because multiplying everything with `a_inv^n` gives `p(a_inv) = 0`.
+  -- TODO: this could be a lemma for `polynomial.reverse`.
+  have hq : ∑ (i : ℕ) in finset.range (p.nat_degree + 1), (p.coeff i) * a ^ (p.nat_degree - i) = 0,
+  { apply (algebra_map R S).injective_iff.mp hRS,
+    have a_inv_ne_zero : a_inv ≠ 0 := right_ne_zero_of_mul (mt ha_inv.symm.trans one_ne_zero),
+    refine (mul_eq_zero.mp _).resolve_right (pow_ne_zero p.nat_degree a_inv_ne_zero),
+    rw [aeval_def, eval₂_eq_sum_range] at hp,
+    rw [ring_hom.map_sum, finset.sum_mul],
+    refine (finset.sum_congr rfl (λ i hi, _)).trans hp,
+    rw [ring_hom.map_mul, mul_assoc],
+    congr,
+    have : a_inv ^ p.nat_degree = a_inv ^ (p.nat_degree - i) * a_inv ^ i,
+    { rw [← pow_add a_inv, nat.sub_add_cancel (nat.le_of_lt_succ (finset.mem_range.mp hi))] },
+    rw [ring_hom.map_pow, this, ← mul_assoc, ← mul_pow, ha_inv, one_pow, one_mul] },
+
+  -- Since `q(a) = 0` and `q(a) = q'(a) * a + 1`, we have `a * -q'(a) = 1`.
+  -- TODO: we could use a lemma for `polynomial.div_X` here.
+  rw [finset.sum_range_succ, p_monic.coeff_nat_degree, one_mul, nat.sub_self, pow_zero,
+      add_eq_zero_iff_eq_neg, eq_comm] at hq,
+  rw [mul_comm, ← neg_mul_eq_neg_mul, finset.sum_mul],
+  convert hq using 2,
+  refine finset.sum_congr rfl (λ i hi, _),
+  have : 1 ≤ p.nat_degree - i := nat.le_sub_left_of_add_le (finset.mem_range.mp hi),
+  rw [mul_assoc, ← pow_succ', nat.sub_add_cancel this]
+end
+
 end algebra
 
 theorem integral_closure_idem {R : Type*} {A : Type*} [comm_ring R] [comm_ring A] [algebra R A] :

src/ring_theory/localization.lean

@@ -1111,6 +1111,49 @@ integral_domain_localization (le_non_zero_divisors_of_domain (by simpa only [] u
 
 end localization_map
 
+section at_prime
+namespace localization
+
+local attribute [instance] classical.prop_decidable
+
+/-- The image of `P` in the localization at `P.prime_compl` is a maximal ideal, and in particular
+it is the unique maximal ideal given by the local ring structure `at_prime.local_ring` -/
+lemma at_prime.map_eq_maximal_ideal {P : ideal R} [hP : ideal.is_prime P] :
+  ideal.map (localization.of P.prime_compl).to_map P =
+    (local_ring.maximal_ideal (localization P.prime_compl)) :=
+begin
+  let f := localization.of P.prime_compl,
+  ext x,
+  split; simp only [local_ring.mem_maximal_ideal, mem_nonunits_iff]; intro hx,
+  { exact λ h, (localization_map.is_prime_of_is_prime_disjoint f P hP
+      (set.disjoint_compl_left P.carrier)).1 (ideal.eq_top_of_is_unit_mem _ hx h) },
+  { obtain ⟨⟨a, b⟩, hab⟩ := localization_map.surj f x,
+    contrapose! hx,
+    rw is_unit_iff_exists_inv,
+    rw localization_map.mem_map_to_map_iff at hx,
+    obtain ⟨a', ha'⟩ := is_unit_iff_exists_inv.1
+      (localization_map.map_units f ⟨a, λ ha, hx ⟨⟨⟨a, ha⟩, b⟩, hab⟩⟩),
+    exact ⟨f.to_map b * a', by rwa [← mul_assoc, hab]⟩ }
+end
+
+/-- The unique maximal ideal of the localization at `P.prime_compl` lies over the ideal `P`. -/
+lemma at_prime.comap_maximal_ideal {P : ideal R} [ideal.is_prime P] :
+  ideal.comap (localization.of P.prime_compl).to_map (local_ring.maximal_ideal (localization P.prime_compl)) = P :=
+begin
+  let Pₚ := local_ring.maximal_ideal (localization P.prime_compl),
+  refine le_antisymm (λ x hx, _)
+    (le_trans ideal.le_comap_map (ideal.comap_mono (le_of_eq at_prime.map_eq_maximal_ideal))),
+  by_cases h0 : x = 0,
+  { exact h0.symm ▸ P.zero_mem },
+  { have : Pₚ.is_prime := ideal.is_maximal.is_prime (local_ring.maximal_ideal.is_maximal _),
+    rw localization_map.is_prime_iff_is_prime_disjoint (localization.of P.prime_compl) at this,
+    contrapose! h0 with hx',
+    simpa using this.2 ⟨hx', hx⟩ }
+end
+
+end localization
+end at_prime
+
 variables (R) {A : Type*} [integral_domain A]
 variables (K : Type*)
 
@@ -1359,6 +1402,24 @@ noncomputable def localization_algebra (M : submonoid R) (f : localization_map M
 variables (f : localization_map M Rₘ)
 variables (g : localization_map (algebra.algebra_map_submonoid S M) Sₘ)
 
+lemma algebra_map_mk' (r : R) (m : M) :
+  (@algebra_map Rₘ Sₘ _ _ (localization_algebra M f g)) (f.mk' r m) =
+    g.mk' (algebra_map R S r) ⟨algebra_map R S m, algebra.mem_algebra_map_submonoid_of_mem m⟩ :=
+localization_map.map_mk' f _ r m
+
+/-- Injectivity of the underlying `algebra_map` descends to the algebra induced by localization -/
+lemma localization_algebra_injective (hRS : function.injective (algebra_map R S))
+  (hM : algebra.algebra_map_submonoid S M ≤ non_zero_divisors S) :
+  function.injective (@algebra_map Rₘ Sₘ _ _ (localization_algebra M f g)) :=
+begin
+  rintros x y hxy,
+  obtain ⟨a, b, rfl⟩ := localization_map.mk'_surjective f x,
+  obtain ⟨c, d, rfl⟩ := localization_map.mk'_surjective f y,
+  rw [algebra_map_mk' f g a b, algebra_map_mk' f g c d, localization_map.mk'_eq_iff_eq] at hxy,
+  refine (localization_map.mk'_eq_iff_eq f).2 (congr_arg f.to_map (hRS _)),
+  convert g.injective hM hxy; simp,
+end
+
 open polynomial
 
 /-- Given a particular witness to an element being algebraic over an algebra `R → S`,