feat(ring_theory/ideal_operations): Chinese Remainder Theorem

Author: kckennylau

src/ring_theory/ideal_operations.lean

@@ -151,6 +151,55 @@ end submodule
 
 namespace ideal
 
+section chinese_remainder
+variables {R : Type u} [comm_ring R] {ι : Type v}
+
+theorem exists_sub_one_mem_and_mem (s : finset ι) {f : ι → ideal R}
+  (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ⊔ f j = ⊤) (i : ι) (his : i ∈ s) :
+  ∃ r : R, r - 1 ∈ f i ∧ ∀ j ∈ s, j ≠ i → r ∈ f j :=
+begin
+  have : ∀ j ∈ s, j ≠ i → ∃ r : R, ∃ H : r - 1 ∈ f i, r ∈ f j,
+  { intros j hjs hji, specialize hf i his j hjs hji.symm,
+    rw [eq_top_iff_one, submodule.mem_sup] at hf,
+    rcases hf with ⟨r, hri, s, hsj, hrs⟩, refine ⟨1 - r, _, _⟩,
+    { rw [sub_right_comm, sub_self, zero_sub], exact (f i).neg_mem hri },
+    { rw [← hrs, add_sub_cancel'], exact hsj } },
+  classical,
+  have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j,
+  { choose g hg1 hg2,
+    refine ⟨λ j, if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, λ j, _, λ j, _⟩,
+    { split_ifs with h, { apply hg1 }, rw sub_self, exact (f i).zero_mem },
+    { intros hjs hji, rw dif_pos, { apply hg2 }, exact ⟨hjs, hji⟩ } },
+  rcases this with ⟨g, hgi, hgj⟩, use (s.erase i).prod g, split,
+  { rw [← quotient.eq, quotient.mk_one, ← finset.prod_hom (quotient.mk (f i))],
+    apply finset.prod_eq_one, intros, rw [← quotient.mk_one, quotient.eq], apply hgi },
+  intros j hjs hji, rw [← quotient.eq_zero_iff_mem, ← finset.prod_hom (quotient.mk (f j))],
+  refine finset.prod_eq_zero (finset.mem_erase_of_ne_of_mem hji hjs) _,
+  rw quotient.eq_zero_iff_mem, exact hgj j hjs hji
+end
+
+/-- Chinese Remainder Theorem. Atiyah-Macdonald 1.10, Eisenbud Ex.2.6, Stacks 10.14.4 (00DT) -/
+theorem exists_sub_mem [fintype ι] {f : ι → ideal R}
+  (hf : ∀ i j, i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) :
+  ∃ r : R, ∀ i, r - g i ∈ f i :=
+begin
+  have : ∃ φ : ι → R, (∀ i, φ i - 1 ∈ f i) ∧ (∀ i j, i ≠ j → φ i ∈ f j),
+  { have := exists_sub_one_mem_and_mem (finset.univ : finset ι) (λ i _ j _ hij, hf i j hij),
+    choose φ hφ, use λ i, φ i (finset.mem_univ i),
+    exact ⟨λ i, (hφ i _).1, λ i j hij, (hφ i _).2 j (finset.mem_univ j) hij.symm⟩ },
+  rcases this with ⟨φ, hφ1, hφ2⟩,
+  use finset.univ.sum (λ i, g i * φ i),
+  intros i,
+  rw [← quotient.eq, ← finset.sum_hom (quotient.mk (f i))],
+  refine eq.trans (finset.sum_eq_single i _ _) _,
+  { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left (hφ2 j i hji) },
+  { intros hi, exact (hi $ finset.mem_univ i).elim },
+  specialize hφ1 i, rw [← quotient.eq, quotient.mk_one] at hφ1,
+  rw [quotient.mk_mul, hφ1, mul_one]
+end
+
+end chinese_remainder
+
 section mul_and_radical
 variables {R : Type u} [comm_ring R]
 variables {I J K L: ideal R}