[Merged by Bors] - feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials

src/data/mv_polynomial/basic.lean

@@ -147,6 +147,17 @@ lemma C_injective (σ : Type*) (R : Type*) [comm_semiring R] :
   function.injective (C : R → mv_polynomial σ R) :=
 finsupp.single_injective _
 
+lemma C_surjective {R : Type*} [comm_semiring R] (σ : Type*) (hσ : ¬ nonempty σ) :
+  function.surjective (C : R → mv_polynomial σ R) :=
+begin
+  refine λ p, ⟨p.to_fun 0, finsupp.ext (λ a, _)⟩,
+  simpa [(finsupp.ext (λ x, absurd (nonempty.intro x) hσ) : a = 0), C, monomial],
+end
+
+lemma C_surjective_fin_0 {R : Type*} [comm_ring R] :
+  function.surjective (mv_polynomial.C : R → mv_polynomial (fin 0) R) :=
+C_surjective (fin 0) (λ h, let ⟨n⟩ := h in fin_zero_elim n)
+
 @[simp] lemma C_inj {σ : Type*} (R : Type*) [comm_semiring R] (r s : R) :
   (C r : mv_polynomial σ R) = C s ↔ r = s :=
 (C_injective σ R).eq_iff

src/data/mv_polynomial/equiv.lean

@@ -262,6 +262,18 @@ end
     (λ i : fin (n+1), fin.cases polynomial.X (λ k, polynomial.C (X k)) i) p :=
 by { rw ← fin_succ_equiv_eq, refl }
 
+lemma fin_succ_equiv_comp_C_eq_C {R : Type u} [comm_semiring R] (n : ℕ) :
+  ((mv_polynomial.fin_succ_equiv R n).symm.to_ring_hom).comp
+    ((polynomial.C).comp (mv_polynomial.C))
+    = (mv_polynomial.C : R →+* mv_polynomial (fin n.succ) R) :=
+begin
+  refine ring_hom.ext (λ x, _),
+  rw ring_hom.comp_apply,
+  refine (mv_polynomial.fin_succ_equiv R n).injective
+    (trans ((mv_polynomial.fin_succ_equiv R n).apply_symm_apply _) _),
+  simp only [mv_polynomial.fin_succ_equiv_apply, mv_polynomial.eval₂_hom_C],
+end
+
 end
 
 end equiv

src/ring_theory/ideal/basic.lean

@@ -79,6 +79,16 @@ theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I :=
 theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I :=
 not_congr I.eq_top_iff_one
 
+lemma exists_mem_ne_zero_iff_ne_bot : (∃ p ∈ I, p ≠ (0 : α)) ↔ I ≠ ⊥ :=
+begin
+  refine ⟨λ h, let ⟨p, hp, hp0⟩ := h in λ h, absurd (h ▸ hp : p ∈ (⊥ : ideal α)) hp0,  λ h, _⟩,
+  contrapose! h,
+  exact eq_bot_iff.2 (λ x hx, (h x hx).symm ▸ (ideal.zero_mem ⊥)),
+end
+
+lemma exists_mem_ne_zero_of_ne_bot (hI : I ≠ ⊥) : ∃ p ∈ I, p ≠ (0 : α) :=
+(exists_mem_ne_zero_iff_ne_bot I).mpr hI
+
 @[simp]
 theorem unit_mul_mem_iff_mem {x y : α} (hy : is_unit y) : y * x ∈ I ↔ x ∈ I :=
 begin
@@ -409,6 +419,13 @@ def lift (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0
 @[simp] lemma lift_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) :
   lift S f H (mk S a) = f a := rfl
 
+@[simp] lemma lift_comp_mk (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0) :
+  (lift S f H).comp (mk S) = f := ring_hom.ext (λ _, rfl)
+
+lemma lift_surjective (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → f a = 0)
+  (hf : function.surjective f) : function.surjective (lift S f H) :=
+λ x, let ⟨y, hy⟩ := hf x in ⟨(quotient.mk S) y, by simpa⟩
+
 end quotient
 
 section lattice

src/ring_theory/ideal/operations.lean

@@ -1149,16 +1149,21 @@ lemma quotient_map_comp_mk {J : ideal R} {I : ideal S} {f : R →+* S} {H : J 
   (quotient_map I f H).comp (quotient.mk J) = (quotient.mk I).comp f :=
 ring_hom.ext (λ x, by simp only [function.comp_app, ring_hom.coe_comp, ideal.quotient_map_mk])
 
-/-- If we take `J = I.comap f` then `quotient_map` is injective. -/
-lemma quotient_map_injective {I : ideal S} {f : R →+* S} :
-  function.injective (quotient_map I f le_rfl) :=
+/-- `H` and `h` are kept as seperate hypothesis since H is used in constructing the quotient map -/
+lemma quotient_map_injective' {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ I.comap f}
+  (h : I.comap f ≤ J) : function.injective (quotient_map I f H) :=
 begin
-  refine (quotient_map I f le_rfl).injective_iff.2 (λ a ha, _),
+  refine (quotient_map I f H).injective_iff.2 (λ a ha, _),
   obtain ⟨r, rfl⟩ := quotient.mk_surjective a,
-  rw quotient_map_mk at ha,
-  rwa quotient.eq_zero_iff_mem at ha ⊢
+  rw [quotient_map_mk, quotient.eq_zero_iff_mem] at ha,
+  exact (quotient.eq_zero_iff_mem).mpr (h ha),
 end
 
+/-- If we take `J = I.comap f` then `quotient_map` is injective automatically. -/
+lemma quotient_map_injective {I : ideal S} {f : R →+* S} :
+  function.injective (quotient_map I f le_rfl) :=
+quotient_map_injective' le_rfl
+
 lemma quotient_map_surjective {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ I.comap f}
   (hf : function.surjective f) : function.surjective (quotient_map I f H) :=
 λ x, let ⟨x, hx⟩ := quotient.mk_surjective x in