feat(ring_theory/*): various lemmas about quotients, localizations, a…

…nd polynomials (#5249)

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

src/ring_theory/ideal/operations.lean

@@ -1145,7 +1145,11 @@ lemma quotient_map_mk {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ I.c
   {x : R} : quotient_map I f H (quotient.mk J x) = quotient.mk I (f x) :=
 quotient.lift_mk J _ _
 
-/-- If we take `J = I.comap f` then `quotient_map` is injective -/
+lemma quotient_map_comp_mk {J : ideal R} {I : ideal S} {f : R →+* S} {H : J ≤ I.comap f} :
+  (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) :=
 begin
@@ -1155,7 +1159,12 @@ begin
   rwa quotient.eq_zero_iff_mem at ha ⊢
 end
 
-/-- Commutativity of a square is preserved when taking quotients by an ideal -/
+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
+  let ⟨y, hy⟩ := hf x in ⟨(quotient.mk J) y, by simp [hx, hy]⟩
+
+/-- Commutativity of a square is preserved when taking quotients by an ideal. -/
 lemma comp_quotient_map_eq_of_comp_eq {R' S' : Type*} [comm_ring R'] [comm_ring S']
   {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f)
   (I : ideal S') : (quotient_map I g' le_rfl).comp (quotient_map (I.comap g') f le_rfl) =

src/ring_theory/integral_closure.lean

@@ -450,8 +450,15 @@ lemma is_integral_tower_bot_of_is_integral_field {R A B : Type*} [comm_ring R] [
   {x : A} (h : is_integral R (algebra_map A B x)) : is_integral R x :=
 is_integral_tower_bot_of_is_integral (algebra_map A B).injective h
 
+lemma ring_hom.is_integral_elem_of_is_integral_elem_comp {x : T}
+  (h : (g.comp f).is_integral_elem x) : g.is_integral_elem x :=
+let ⟨p, ⟨hp, hp'⟩⟩ := h in ⟨p.map f, monic_map f hp, by rwa ← eval₂_map at hp'⟩
+
+lemma ring_hom.is_integral_tower_top_of_is_integral (h : (g.comp f).is_integral) : g.is_integral :=
+λ x, ring_hom.is_integral_elem_of_is_integral_elem_comp f g (h x)
+
 /-- If `R → A → B` is an algebra tower,
-then if the entire tower is an integral extension so is `A → B` -/
+then if the entire tower is an integral extension so is `A → B`. -/
 lemma is_integral_tower_top_of_is_integral {x : B} (h : is_integral R x) : is_integral A x :=
 begin
   rcases h with ⟨p, ⟨hp, hp'⟩⟩,
@@ -473,7 +480,18 @@ lemma is_integral_quotient_of_is_integral {I : ideal A} (hRA : is_integral R A)
   is_integral (I.comap (algebra_map R A)).quotient I.quotient :=
 (algebra_map R A).is_integral_quotient_of_is_integral hRA
 
-/-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field -/
+lemma is_integral_quotient_map_iff {I : ideal S} :
+  (ideal.quotient_map I f le_rfl).is_integral ↔
+    ((ideal.quotient.mk I).comp f : R →+* I.quotient).is_integral :=
+begin
+  let g := ideal.quotient.mk (I.comap f),
+  have := @ideal.quotient_map_comp_mk R S _ _ _ I f le_rfl,
+  refine ⟨λ h, _, λ h, ring_hom.is_integral_tower_top_of_is_integral g _ (this ▸ h)⟩,
+  refine this ▸ ring_hom.is_integral_trans g (ideal.quotient_map I f le_rfl) _ h,
+  exact ring_hom.is_integral_of_surjective g ideal.quotient.mk_surjective,
+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 : is_integral R S) (hRS : function.injective (algebra_map R S))
   (hS : is_field S) : is_field R :=

src/ring_theory/jacobson.lean

@@ -89,7 +89,7 @@ lemma is_jacobson_iff_Inf_maximal' : is_jacobson R ↔
 ⟨λ H I h, eq_jacobson_iff_Inf_maximal'.1 (H _ (is_prime.radical h)),
   λ H , is_jacobson_iff_prime_eq.2 (λ P hP, eq_jacobson_iff_Inf_maximal'.2 (H hP))⟩
 
-lemma radical_eq_jacobson (H : is_jacobson R) (I : ideal R) : I.radical = I.jacobson :=
+lemma radical_eq_jacobson [H : is_jacobson R] (I : ideal R) : I.radical = I.jacobson :=
 le_antisymm (le_Inf (λ J ⟨hJ, hJ_max⟩, (is_prime.radical_le_iff hJ_max.is_prime).mpr hJ))
             ((H I.radical (radical_idem I)) ▸ (jacobson_mono le_radical))
 

src/ring_theory/localization.lean

@@ -1202,6 +1202,17 @@ end
 end localization
 end at_prime
 
+/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
+lemma localization_map_bijective_of_field {R Rₘ : Type*} [integral_domain R] [comm_ring Rₘ]
+  {M : submonoid R} (hM : (0 : R) ∉ M) (hR : is_field R)
+  (f : localization_map M Rₘ) : function.bijective f.to_map :=
+begin
+  refine ⟨f.injective (le_non_zero_divisors_of_domain hM), λ x, _⟩,
+  obtain ⟨r, ⟨m, hm⟩, rfl⟩ := f.mk'_surjective x,
+  obtain ⟨n, hn⟩ := hR.mul_inv_cancel (λ hm0, hM (hm0 ▸ hm) : m ≠ 0),
+  exact ⟨r * n, by erw [f.eq_mk'_iff_mul_eq, ← f.to_map.map_mul, mul_assoc, mul_comm n, hn, mul_one]⟩
+end
+
 variables (R) {A : Type*} [integral_domain A]
 variables (K : Type*)
 
@@ -1455,19 +1466,28 @@ lemma algebra_map_mk' (r : R) (m : 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)) :=
+/-- Injectivity of a map descends to the map induced on localizations. -/
+lemma map_injective_of_injective {R S : Type*} [comm_ring R] [comm_ring S]
+  (ϕ : R →+* S) (hϕ : function.injective ϕ) (M : submonoid R)
+  (f : localization_map M Rₘ) (g : localization_map (M.map ϕ : submonoid S) Sₘ)
+  (hM : (M.map ϕ : submonoid S) ≤ non_zero_divisors S) :
+  function.injective (f.map (M.mem_map_of_mem (ϕ : R →* S)) 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 _)),
+  rw [localization_map.map_mk' f _ a b, localization_map.map_mk' f _ c d,
+    localization_map.mk'_eq_iff_eq] at hxy,
+  refine (localization_map.mk'_eq_iff_eq f).2 (congr_arg f.to_map (hϕ _)),
   convert g.injective hM hxy; simp,
 end
 
+/-- 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)) :=
+map_injective_of_injective (algebra_map R S) hRS M f g hM
+
 open polynomial
 
 lemma ring_hom.is_integral_elem_localization_at_leading_coeff

src/ring_theory/polynomial/basic.lean

@@ -330,6 +330,34 @@ begin
   exact hx,
 end
 
+/-- `polynomial R` is never a field for any ring `R`. -/
+lemma polynomial_not_is_field : ¬ is_field (polynomial R) :=
+begin
+  by_contradiction hR,
+  by_cases hR' : ∃ (x y : R), x ≠ y,
+  { haveI : nontrivial R := let ⟨x, y, hxy⟩ := hR' in nontrivial_of_ne x y hxy,
+    obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero,
+    by_cases hp0 : p = 0,
+    { replace hp := congr_arg degree hp,
+      rw [hp0, mul_zero, degree_zero, degree_one] at hp,
+      contradiction },
+    { have : p.degree < (X * p).degree := (mul_comm p X) ▸ degree_lt_degree_mul_X hp0,
+      rw [congr_arg degree hp, degree_one, nat.with_bot.lt_zero_iff, degree_eq_bot] at this,
+      exact hp0 this } },
+  { push_neg at hR',
+    exact let ⟨x, y, hxy⟩ := hR.exists_pair_ne in hxy (polynomial.ext (λ n, hR' _ _)) }
+end
+
+/-- The only constant in a maximal ideal over a field is `0`. -/
+lemma eq_zero_of_constant_mem_of_maximal (hR : is_field R)
+  (I : ideal (polynomial R)) [hI : I.is_maximal] (x : R) (hx : C x ∈ I) : x = 0 :=
+begin
+  refine classical.by_contradiction (λ hx0, hI.1 ((eq_top_iff_one I).2 _)),
+  obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0,
+  convert I.smul_mem (C y) hx,
+  rw [smul_eq_mul, ← C.map_mul, mul_comm y x, hy, ring_hom.map_one],
+end
+
 /-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
 def of_polynomial (I : ideal (polynomial R)) : submodule R (polynomial R) :=
 { carrier := I.carrier,