From 0344aeed039e0cf38a30a39a47fbae32cdf8ba2e Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Sat, 12 Dec 2020 07:16:56 +0000 Subject: [PATCH] feat(ring_theory/*): various lemmas about quotients, localizations, and polynomials (#5249) Co-authored-by: Devon Tuma --- src/ring_theory/ideal/operations.lean | 13 +++++++++-- src/ring_theory/integral_closure.lean | 22 ++++++++++++++++-- src/ring_theory/jacobson.lean | 2 +- src/ring_theory/localization.lean | 32 ++++++++++++++++++++++----- src/ring_theory/polynomial/basic.lean | 28 +++++++++++++++++++++++ 5 files changed, 86 insertions(+), 11 deletions(-) diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean index 68651882e6796..983a67f46608e 100644 --- a/src/ring_theory/ideal/operations.lean +++ b/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) = diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean index 18493d655cdab..12ee52da61928 100644 --- a/src/ring_theory/integral_closure.lean +++ b/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 := diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index 9be8f1b137d10..f45c0fbf8226d 100644 --- a/src/ring_theory/jacobson.lean +++ b/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)) diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean index 459722beb54b3..7c4a7d3db71c6 100644 --- a/src/ring_theory/localization.lean +++ b/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 diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean index f33e7cb343f4e..ba2d71e0dece4 100644 --- a/src/ring_theory/polynomial/basic.lean +++ b/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,