diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean index 920ac15a81fe7..277022c5e12d0 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean @@ -22,11 +22,11 @@ import Mathlib.RingTheory.Jacobson open Ideal -variable {R : Type*} [CommRing R] [IsJacobson R] +variable {R : Type*} [CommRing R] [IsJacobsonRing R] namespace PrimeSpectrum -lemma exists_isClosed_singleton_of_isJacobson +lemma exists_isClosed_singleton_of_isJacobsonRing (s : (Set (PrimeSpectrum R))) (hs : IsOpen s) (hs' : s.Nonempty) : ∃ x ∈ s, IsClosed {x} := by simp_rw [isClosed_singleton_iff_isMaximal] @@ -48,12 +48,12 @@ If `R` is both noetherian and jacobson, then the following are equivalent for `x 3. `{x}` is both closed and stable under generalization (i.e. `x` is both a minimal prime and a maximal ideal) -/ -lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobson +lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing [IsNoetherianRing R] (x : PrimeSpectrum R) : List.TFAE [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}] := by tfae_have 1 → 2 · intro h - obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobson _ h + obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h ⟨x, Set.mem_singleton x⟩ exact ⟨h', h⟩ tfae_have 2 → 3 diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index aaa724fa39606..2ac7515b51697 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -15,53 +15,56 @@ The following conditions are equivalent for a ring `R`: 3. Every prime ideal `I` is equal to its Jacobson radical Any ring satisfying any of these equivalent conditions is said to be Jacobson. Some particular examples of Jacobson rings are also proven. -`isJacobson_quotient` says that the quotient of a Jacobson ring is Jacobson. -`isJacobson_localization` says the localization of a Jacobson ring to a single element is Jacobson. -`isJacobson_polynomial_iff_isJacobson` says polynomials over a Jacobson ring form a Jacobson ring. +`isJacobsonRing_quotient` says that the quotient of a Jacobson ring is Jacobson. +`isJacobsonRing_localization` says the localization of a Jacobson ring + to a single element is Jacobson. +`isJacobsonRing_polynomial_iff_isJacobsonRing` says polynomials over a Jacobson ring + form a Jacobson ring. ## Main definitions Let `R` be a commutative ring. Jacobson rings are defined using the first of the above conditions -* `IsJacobson R` is the proposition that `R` is a Jacobson ring. It is a class, +* `IsJacobsonRing R` is the proposition that `R` is a Jacobson ring. It is a class, implemented as the predicate that for any ideal, `I.isRadical` implies `I.jacobson = I`. ## Main statements -* `isJacobson_iff_prime_eq` is the equivalence between conditions 1 and 3 above. -* `isJacobson_iff_sInf_maximal` is the equivalence between conditions 1 and 2 above. -* `isJacobson_of_surjective` says that if `R` is a Jacobson ring and `f : R →+* S` is surjective, - then `S` is also a Jacobson ring -* `MvPolynomial.isJacobson` says that multi-variate polynomials over a Jacobson ring are Jacobson. +* `isJacobsonRing_iff_prime_eq` is the equivalence between conditions 1 and 3 above. +* `isJacobsonRing_iff_sInf_maximal` is the equivalence between conditions 1 and 2 above. +* `isJacobsonRing_of_surjective` says that if `R` is a Jacobson ring and + `f : R →+* S` is surjective, then `S` is also a Jacobson ring +* `MvPolynomial.isJacobsonRing` says that multi-variate polynomials + over a Jacobson ring are Jacobson. ## Tags Jacobson, Jacobson Ring -/ universe u -namespace Ideal - -open Polynomial open Polynomial +open Ideal -section IsJacobson +section IsJacobsonRing variable {R S : Type*} [CommRing R] [CommRing S] {I : Ideal R} /-- A ring is a Jacobson ring if for every radical ideal `I`, the Jacobson radical of `I` is equal to `I`. - See `isJacobson_iff_prime_eq` and `isJacobson_iff_sInf_maximal` for equivalent definitions. -/ -class IsJacobson (R : Type*) [CommRing R] : Prop where + See `isJacobsonRing_iff_prime_eq` and `isJacobsonRing_iff_sInf_maximal` + for equivalent definitions. -/ +class IsJacobsonRing (R : Type*) [CommRing R] : Prop where out' : ∀ I : Ideal R, I.IsRadical → I.jacobson = I -theorem isJacobson_iff {R} [CommRing R] : - IsJacobson R ↔ ∀ I : Ideal R, I.IsRadical → I.jacobson = I := +theorem isJacobsonRing_iff {R} [CommRing R] : + IsJacobsonRing R ↔ ∀ I : Ideal R, I.IsRadical → I.jacobson = I := ⟨fun h => h.1, fun h => ⟨h⟩⟩ -theorem IsJacobson.out {R} [CommRing R] : - IsJacobson R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I := - isJacobson_iff.1 +theorem IsJacobsonRing.out {R} [CommRing R] : + IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I := + isJacobsonRing_iff.1 /-- A ring is a Jacobson ring if and only if for all prime ideals `P`, the Jacobson radical of `P` is equal to `P`. -/ -theorem isJacobson_iff_prime_eq : IsJacobson R ↔ ∀ P : Ideal R, IsPrime P → P.jacobson = P := by - refine isJacobson_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩ +theorem isJacobsonRing_iff_prime_eq : + IsJacobsonRing R ↔ ∀ P : Ideal R, IsPrime P → P.jacobson = P := by + refine isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩ refine fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx) rw [← hI.radical, radical_eq_sInf I, mem_sInf] intro P hP @@ -73,50 +76,51 @@ theorem isJacobson_iff_prime_eq : IsJacobson R ↔ ∀ P : Ideal R, IsPrime P /-- A ring `R` is Jacobson if and only if for every prime ideal `I`, `I` can be written as the infimum of some collection of maximal ideals. Allowing ⊤ in the set `M` of maximal ideals is equivalent, but makes some proofs cleaner. -/ -theorem isJacobson_iff_sInf_maximal : IsJacobson R ↔ ∀ {I : Ideal R}, I.IsPrime → +theorem isJacobsonRing_iff_sInf_maximal : IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M : Set (Ideal R), (∀ J ∈ M, IsMaximal J ∨ J = ⊤) ∧ I = sInf M := ⟨fun H _I h => eq_jacobson_iff_sInf_maximal.1 (H.out h.isRadical), fun H => - isJacobson_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal.2 (H hP)⟩ + isJacobsonRing_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal.2 (H hP)⟩ -theorem isJacobson_iff_sInf_maximal' : IsJacobson R ↔ ∀ {I : Ideal R}, I.IsPrime → +/-- A variant of `isJacobsonRing_iff_sInf_maximal` with a different spelling of "maximal or `⊤`". -/ +theorem isJacobsonRing_iff_sInf_maximal' : IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M : Set (Ideal R), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M := ⟨fun H _I h => eq_jacobson_iff_sInf_maximal'.1 (H.out h.isRadical), fun H => - isJacobson_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal'.2 (H hP)⟩ + isJacobsonRing_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal'.2 (H hP)⟩ -theorem radical_eq_jacobson [H : IsJacobson R] (I : Ideal R) : I.radical = I.jacobson := +theorem Ideal.radical_eq_jacobson [H : IsJacobsonRing R] (I : Ideal R) : I.radical = I.jacobson := le_antisymm (le_sInf fun _J ⟨hJ, hJ_max⟩ => (IsPrime.radical_le_iff hJ_max.isPrime).mpr hJ) (H.out (radical_isRadical I) ▸ jacobson_mono le_radical) /-- Fields have only two ideals, and the condition holds for both of them. -/ -instance (priority := 100) isJacobson_field {K : Type*} [Field K] : IsJacobson K := +instance (priority := 100) isJacobsonRing_field {K : Type*} [Field K] : IsJacobsonRing K := ⟨fun I _ => Or.recOn (eq_bot_or_top I) (fun h => le_antisymm (sInf_le ⟨le_rfl, h.symm ▸ bot_isMaximal⟩) (h.symm ▸ bot_le)) fun h => by rw [h, jacobson_eq_top_iff]⟩ -theorem isJacobson_of_surjective [H : IsJacobson R] : - (∃ f : R →+* S, Function.Surjective ↑f) → IsJacobson S := by +theorem isJacobsonRing_of_surjective [H : IsJacobsonRing R] : + (∃ f : R →+* S, Function.Surjective ↑f) → IsJacobsonRing S := by rintro ⟨f, hf⟩ - rw [isJacobson_iff_sInf_maximal] + rw [isJacobsonRing_iff_sInf_maximal] intro p hp use map f '' { J : Ideal R | comap f p ≤ J ∧ J.IsMaximal } use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm have : p = map f (comap f p).jacobson := - (IsJacobson.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm + (IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ) -instance (priority := 100) isJacobson_quotient [IsJacobson R] : IsJacobson (R ⧸ I) := - isJacobson_of_surjective ⟨Quotient.mk I, by +instance (priority := 100) isJacobsonRing_quotient [IsJacobsonRing R] : IsJacobsonRing (R ⧸ I) := + isJacobsonRing_of_surjective ⟨Ideal.Quotient.mk I, by rintro ⟨x⟩ use x rfl⟩ -theorem isJacobson_iso (e : R ≃+* S) : IsJacobson R ↔ IsJacobson S := - ⟨fun h => @isJacobson_of_surjective _ _ _ _ h ⟨(e : R →+* S), e.surjective⟩, fun h => - @isJacobson_of_surjective _ _ _ _ h ⟨(e.symm : S →+* R), e.symm.surjective⟩⟩ +theorem isJacobsonRing_iso (e : R ≃+* S) : IsJacobsonRing R ↔ IsJacobsonRing S := + ⟨fun h => @isJacobsonRing_of_surjective _ _ _ _ h ⟨(e : R →+* S), e.surjective⟩, fun h => + @isJacobsonRing_of_surjective _ _ _ _ h ⟨(e.symm : S →+* R), e.symm.surjective⟩⟩ -theorem isJacobson_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] (hR : IsJacobson R) : - IsJacobson S := by - rw [isJacobson_iff_prime_eq] +theorem isJacobsonRing_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] [IsJacobsonRing R] : + IsJacobsonRing S := by + rw [isJacobsonRing_iff_prime_eq] intro P hP by_cases hP_top : comap (algebraMap R S) P = ⊤ · simp [comap_eq_top_iff.1 hP_top] @@ -124,7 +128,7 @@ theorem isJacobson_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] (hR : Is rw [jacobson_eq_iff_jacobson_quotient_eq_bot] refine eq_bot_of_comap_eq_bot (R := R ⧸ comap (algebraMap R S) P) ?_ rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1 - ((isJacobson_iff_prime_eq.1 hR) (comap (algebraMap R S) P) (comap_isPrime _ _)), + ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)), comap_jacobson] refine sInf_le_sInf fun J hJ => ?_ simp only [true_and, Set.mem_image, bot_le, Set.mem_setOf_eq] @@ -132,13 +136,14 @@ theorem isJacobson_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] (hR : Is exact exists_ideal_over_maximal_of_isIntegral J (comap_bot_le_of_injective _ algebraMap_quotient_injective) -theorem isJacobson_of_isIntegral' (f : R →+* S) (hf : f.IsIntegral) (hR : IsJacobson R) : - IsJacobson S := +/-- A variant of `isJacobsonRing_of_isIntegral` that takes `RingHom.IsIntegral` instead. -/ +theorem isJacobsonRing_of_isIntegral' (f : R →+* S) (hf : f.IsIntegral) [IsJacobsonRing R] : + IsJacobsonRing S := let _ : Algebra R S := f.toAlgebra have : Algebra.IsIntegral R S := ⟨hf⟩ - isJacobson_of_isIntegral hR + isJacobsonRing_of_isIntegral (R := R) -end IsJacobson +end IsJacobsonRing section Localization @@ -153,7 +158,7 @@ variable (S) correspond to maximal ideals in the original ring `R` that don't contain `y`. This lemma gives the correspondence in the particular case of an ideal and its comap. See `le_relIso_of_maximal` for the more general relation isomorphism -/ -theorem isMaximal_iff_isMaximal_disjoint [H : IsJacobson R] (J : Ideal S) : +theorem IsLocalization.isMaximal_iff_isMaximal_disjoint [H : IsJacobsonRing R] (J : Ideal S) : J.IsMaximal ↔ (comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J := by constructor · refine fun h => ⟨?_, fun hy => @@ -161,22 +166,22 @@ theorem isMaximal_iff_isMaximal_disjoint [H : IsJacobson R] (J : Ideal S) : have hJ : J.IsPrime := IsMaximal.isPrime h rw [isPrime_iff_isPrime_disjoint (Submonoid.powers y)] at hJ have : y ∉ (comap (algebraMap R S) J).1 := Set.disjoint_left.1 hJ.right (Submonoid.mem_powers _) - erw [← H.out hJ.left.isRadical, mem_sInf] at this + erw [← H.out hJ.left.isRadical, Ideal.mem_sInf] at this push_neg at this rcases this with ⟨I, hI, hI'⟩ convert hI.right - by_cases hJ : J = map (algebraMap R S) I + by_cases hJ : J = I.map (algebraMap R S) · rw [hJ, comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI.right)] rwa [disjoint_powers_iff_not_mem y hI.right.isPrime.isRadical] - · have hI_p : (map (algebraMap R S) I).IsPrime := by + · have hI_p : (I.map (algebraMap R S)).IsPrime := by refine isPrime_of_isPrime_disjoint (powers y) _ I hI.right.isPrime ?_ rwa [disjoint_powers_iff_not_mem y hI.right.isPrime.isRadical] - have : J ≤ map (algebraMap R S) I := map_comap (Submonoid.powers y) S J ▸ map_mono hI.left + have : J ≤ I.map (algebraMap R S) := map_comap (Submonoid.powers y) S J ▸ map_mono hI.left exact absurd (h.1.2 _ (lt_of_le_of_ne this hJ)) hI_p.1 · refine fun h => ⟨⟨fun hJ => h.1.ne_top (eq_top_iff.2 ?_), fun I hI => ?_⟩⟩ · rwa [eq_top_iff, ← (IsLocalization.orderEmbedding (powers y) S).le_iff_le] at hJ - · have := congr_arg (map (algebraMap R S)) (h.1.1.2 _ ⟨comap_mono (le_of_lt hI), ?_⟩) - · rwa [map_comap (powers y) S I, map_top] at this + · have := congr_arg (Ideal.map (algebraMap R S)) (h.1.1.2 _ ⟨comap_mono (le_of_lt hI), ?_⟩) + · rwa [map_comap (powers y) S I, Ideal.map_top] at this refine fun hI' => hI.right ?_ rw [← map_comap (powers y) S I, ← map_comap (powers y) S J] exact map_mono hI' @@ -187,8 +192,9 @@ variable {S} correspond to maximal ideals in the original ring `R` that don't contain `y`. This lemma gives the correspondence in the particular case of an ideal and its map. See `le_relIso_of_maximal` for the more general statement, and the reverse of this implication -/ -theorem isMaximal_of_isMaximal_disjoint [IsJacobson R] (I : Ideal R) (hI : I.IsMaximal) - (hy : y ∉ I) : (map (algebraMap R S) I).IsMaximal := by +theorem IsLocalization.isMaximal_of_isMaximal_disjoint + [IsJacobsonRing R] (I : Ideal R) (hI : I.IsMaximal) + (hy : y ∉ I) : (I.map (algebraMap R S)).IsMaximal := by rw [isMaximal_iff_isMaximal_disjoint S y, comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI) ((disjoint_powers_iff_not_mem y hI.isPrime.isRadical).2 hy)] @@ -196,7 +202,7 @@ theorem isMaximal_of_isMaximal_disjoint [IsJacobson R] (I : Ideal R) (hI : I.IsM /-- If `R` is a Jacobson ring, then maximal ideals in the localization at `y` correspond to maximal ideals in the original ring `R` that don't contain `y` -/ -def orderIsoOfMaximal [IsJacobson R] : +def IsLocalization.orderIsoOfMaximal [IsJacobsonRing R] : { p : Ideal S // p.IsMaximal } ≃o { p : Ideal R // p.IsMaximal ∧ y ∉ p } where toFun p := ⟨Ideal.comap (algebraMap R S) p.1, (isMaximal_iff_isMaximal_disjoint S y p.1).1 p.2⟩ invFun p := ⟨Ideal.map (algebraMap R S) p.1, isMaximal_of_isMaximal_disjoint y p.1 p.2.1 p.2.2⟩ @@ -210,8 +216,8 @@ def orderIsoOfMaximal [IsJacobson R] : include y in /-- If `S` is the localization of the Jacobson ring `R` at the submonoid generated by `y : R`, then `S` is Jacobson. -/ -theorem isJacobson_localization [H : IsJacobson R] : IsJacobson S := by - rw [isJacobson_iff_prime_eq] +theorem isJacobsonRing_localization [H : IsJacobsonRing R] : IsJacobsonRing S := by + rw [isJacobsonRing_iff_prime_eq] refine fun P' hP' => le_antisymm ?_ le_jacobson obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP' have hP := H.out hP'.isRadical @@ -221,7 +227,7 @@ theorem isJacobson_localization [H : IsJacobson R] : IsJacobson S := by comap (algebraMap R S) P' := by intro x hx have hxy : x * y ∈ (comap (algebraMap R S) P').jacobson := by - rw [Ideal.jacobson, mem_sInf] + rw [Ideal.jacobson, Ideal.mem_sInf] intro J hJ by_cases h : y ∈ J · exact J.mul_mem_left x h @@ -282,20 +288,20 @@ variable {Rₘ Sₘ : Type*} [CommRing Rₘ] [CommRing Sₘ] so integrality of the entire extension follows by closure under addition and multiplication. -/ theorem isIntegral_isLocalization_polynomial_quotient (P : Ideal R[X]) (pX : R[X]) (hpX : pX ∈ P) [Algebra (R ⧸ P.comap (C : R →+* R[X])) Rₘ] - [IsLocalization.Away (pX.map (Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff Rₘ] - [Algebra (R[X] ⧸ P) Sₘ] [IsLocalization ((Submonoid.powers (pX.map (Quotient.mk (P.comap + [IsLocalization.Away (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff Rₘ] + [Algebra (R[X] ⧸ P) Sₘ] [IsLocalization ((Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff).map (quotientMap P C le_rfl) : Submonoid (R[X] ⧸ P)) Sₘ] : - (IsLocalization.map Sₘ (quotientMap P C le_rfl) (Submonoid.powers (pX.map (Quotient.mk + (IsLocalization.map Sₘ (quotientMap P C le_rfl) (Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff).le_comap_map : Rₘ →+* Sₘ).IsIntegral := by let P' : Ideal R := P.comap C let M : Submonoid (R ⧸ P') := - Submonoid.powers (pX.map (Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff + Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff let M' : Submonoid (R[X] ⧸ P) := - (Submonoid.powers (pX.map (Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff).map + (Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff).map (quotientMap P C le_rfl) let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C le_rfl let φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ M.le_comap_map - have hφ' : φ.comp (Quotient.mk P') = (Quotient.mk P).comp C := rfl + have hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C := rfl intro p obtain ⟨⟨p', ⟨q, hq⟩⟩, hp⟩ := IsLocalization.surj M' p suffices φ'.IsIntegralElem (algebraMap (R[X] ⧸ P) Sₘ p') by @@ -307,14 +313,14 @@ theorem isIntegral_isLocalization_polynomial_quotient rw [RingHom.comp_apply] dsimp at hp refine @IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ' - ((algebraMap (R[X] ⧸ P) Sₘ).comp (Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_ + ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_ ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_ · rintro x ⟨p, hp, rfl⟩ simp only [Set.mem_insert_iff] at hp cases' hp with hy hy · rw [hy] - refine φ.isIntegralElem_localization_at_leadingCoeff ((Quotient.mk P) X) - (pX.map (Quotient.mk P')) ?_ M ?_ + refine φ.isIntegralElem_localization_at_leadingCoeff ((Ideal.Quotient.mk P) X) + (pX.map (Ideal.Quotient.mk P')) ?_ M ?_ · rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X] · use 1 simp only [pow_one] @@ -322,7 +328,7 @@ theorem isIntegral_isLocalization_polynomial_quotient -- Porting note: was `refine' hy.symm ▸` -- `⟨X - C (algebraMap _ _ ((Quotient.mk P') (p.coeff 0))), monic_X_sub_C _, _⟩` rw [hy] - use X - C (algebraMap (R ⧸ P') Rₘ ((Quotient.mk P') (p.coeff 0))) + use X - C (algebraMap (R ⧸ P') Rₘ ((Ideal.Quotient.mk P') (p.coeff 0))) constructor · apply monic_X_sub_C · simp only [eval₂_sub, eval₂_X, eval₂_C] @@ -336,7 +342,8 @@ theorem isIntegral_isLocalization_polynomial_quotient /-- If `f : R → S` descends to an integral map in the localization at `x`, and `R` is a Jacobson ring, then the intersection of all maximal ideals in `S` is trivial -/ -theorem jacobson_bot_of_integral_localization {R : Type*} [CommRing R] [IsDomain R] [IsJacobson R] +theorem jacobson_bot_of_integral_localization + {R : Type*} [CommRing R] [IsDomain R] [IsJacobsonRing R] (Rₘ Sₘ : Type*) [CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective ↑φ) (x : R) (hx : x ≠ 0) [Algebra R Rₘ] [IsLocalization.Away x Rₘ] [Algebra S Sₘ] [IsLocalization ((Submonoid.powers x).map φ : Submonoid S) Sₘ] @@ -351,7 +358,8 @@ theorem jacobson_bot_of_integral_localization {R : Type*} [CommRing R] [IsDomain have hϕ' : comap (algebraMap S Sₘ) (⊥ : Ideal Sₘ) = (⊥ : Ideal S) := by rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot] exact IsLocalization.injective Sₘ hM - have hSₘ : IsJacobson Sₘ := isJacobson_of_isIntegral' φ' hφ' (isJacobson_localization x) + have hRₘ : IsJacobsonRing Rₘ := isJacobsonRing_localization x + have hSₘ : IsJacobsonRing Sₘ := isJacobsonRing_of_isIntegral' φ' hφ' refine eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ')) rw [← hSₘ.out isRadical_bot_of_noZeroDivisors, comap_jacobson] exact sInf_le_sInf fun j hj => ⟨bot_le, @@ -366,7 +374,7 @@ theorem jacobson_bot_of_integral_localization {R : Type*} [CommRing R] [IsDomain let f := quotientMap (I.comap (algebraMap S Sₘ)) φ le_rfl let g := quotientMap I (algebraMap S Sₘ) le_rfl have := isMaximal_comap_of_isIntegral_of_isMaximal' φ' hφ' I - have := ((isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left + have := ((IsLocalization.isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left have : ((I.comap (algebraMap S Sₘ)).comap φ).IsMaximal := by rwa [comap_comap, hcomm, ← comap_comap] at this rw [← bot_quotient_isMaximal_iff] at this ⊢ @@ -378,10 +386,10 @@ theorem jacobson_bot_of_integral_localization {R : Type*} [CommRing R] [IsDomain (IsLocalization.surjective_quotientMap_of_maximal_of_localization (Submonoid.powers x) Rₘ (by rwa [comap_comap, hcomm, ← bot_quotient_isMaximal_iff]))).trans _ _ (hφ'.quotient _)) -/-- Used to bootstrap the proof of `isJacobson_polynomial_iff_isJacobson`. +/-- Used to bootstrap the proof of `isJacobsonRing_polynomial_iff_isJacobsonRing`. That theorem is more general and should be used instead of this one. -/ -private theorem isJacobson_polynomial_of_domain (R : Type*) [CommRing R] [IsDomain R] - [hR : IsJacobson R] (P : Ideal R[X]) [IsPrime P] (hP : ∀ x : R, C x ∈ P → x = 0) : +private theorem isJacobsonRing_polynomial_of_domain (R : Type*) [CommRing R] [IsDomain R] + [hR : IsJacobsonRing R] (P : Ideal R[X]) [IsPrime P] (hP : ∀ x : R, C x ∈ P → x = 0) : P.jacobson = P := by by_cases Pb : P = ⊥ · exact Pb.symm ▸ @@ -389,9 +397,9 @@ private theorem isJacobson_polynomial_of_domain (R : Type*) [CommRing R] [IsDoma · rw [jacobson_eq_iff_jacobson_quotient_eq_bot] let P' := P.comap (C : R →+* R[X]) haveI : P'.IsPrime := comap_isPrime C P - haveI hR' : IsJacobson (R ⧸ P') := by infer_instance + haveI hR' : IsJacobsonRing (R ⧸ P') := by infer_instance obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP - let x := (Polynomial.map (Quotient.mk P') p).leadingCoeff + let x := (Polynomial.map (Ideal.Quotient.mk P') p).leadingCoeff have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero] let φ : R ⧸ P' →+* R[X] ⧸ P := Ideal.quotientMap P (C : R →+* R[X]) le_rfl let hφ : Function.Injective ↑φ := quotientMap_injective @@ -401,22 +409,23 @@ private theorem isJacobson_polynomial_of_domain (R : Type*) [CommRing R] [IsDoma haveI islocSₘ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ := by infer_instance exact @isIntegral_isLocalization_polynomial_quotient R _ Rₘ Sₘ _ _ P p pP _ _ _ islocSₘ -theorem isJacobson_polynomial_of_isJacobson (hR : IsJacobson R) : IsJacobson R[X] := by - rw [isJacobson_iff_prime_eq] +theorem isJacobsonRing_polynomial_of_isJacobsonRing (hR : IsJacobsonRing R) : + IsJacobsonRing R[X] := by + rw [isJacobsonRing_iff_prime_eq] intro I hI - let R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range - let i : R →+* R' := ((Quotient.mk I).comp C).rangeRestrict - have hi : Function.Surjective ↑i := ((Quotient.mk I).comp C).rangeRestrict_surjective + let R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range + let i : R →+* R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict + have hi : Function.Surjective ↑i := ((Ideal.Quotient.mk I).comp C).rangeRestrict_surjective have hi' : RingHom.ker (mapRingHom i) ≤ I := by intro f hf apply polynomial_mem_ideal_of_coeff_mem_ideal I f intro n - replace hf := congrArg (fun g : Polynomial ((Quotient.mk I).comp C).range => g.coeff n) hf - change (Polynomial.map ((Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf + replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf + change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf rw [coeff_map, Subtype.ext_iff] at hf rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply] - have R'_jacob : IsJacobson R' := isJacobson_of_surjective ⟨i, hi⟩ - let J := map (mapRingHom i) I + have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩ + let J := I.map (mapRingHom i) -- Porting note: moved ↓ this up a few lines, so that it can be used in the `have` have h_surj : Function.Surjective (mapRingHom i) := Polynomial.map_surjective i hi have : IsPrime J := map_isPrime_of_surjective h_surj hi' @@ -426,17 +435,17 @@ theorem isJacobson_polynomial_of_isJacobson (hR : IsJacobson R) : IsJacobson R[X comap_map_of_surjective _ h_surj] at h refine le_antisymm ?_ le_jacobson exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi')) - apply isJacobson_polynomial_of_domain R' J + apply isJacobsonRing_polynomial_of_domain R' J exact eq_zero_of_polynomial_mem_map_range I -theorem isJacobson_polynomial_iff_isJacobson : IsJacobson R[X] ↔ IsJacobson R := by - refine ⟨?_, isJacobson_polynomial_of_isJacobson⟩ +theorem isJacobsonRing_polynomial_iff_isJacobsonRing : IsJacobsonRing R[X] ↔ IsJacobsonRing R := by + refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩ intro H - exact isJacobson_of_surjective ⟨eval₂RingHom (RingHom.id _) 1, fun x => + exact isJacobsonRing_of_surjective ⟨eval₂RingHom (RingHom.id _) 1, fun x => ⟨C x, by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]⟩⟩ -instance [IsJacobson R] : IsJacobson R[X] := - isJacobson_polynomial_iff_isJacobson.mpr ‹IsJacobson R› +instance [IsJacobsonRing R] : IsJacobsonRing R[X] := + isJacobsonRing_polynomial_iff_isJacobsonRing.mpr ‹IsJacobsonRing R› end CommRing @@ -445,7 +454,7 @@ section variable {R : Type*} [CommRing R] variable (P : Ideal R[X]) [hP : P.IsMaximal] -theorem isMaximal_comap_C_of_isMaximal [IsJacobson R] [Nontrivial R] +theorem isMaximal_comap_C_of_isMaximal [IsJacobsonRing R] [Nontrivial R] (hP' : ∀ x : R, C x ∈ P → x = 0) : IsMaximal (comap (C : R →+* R[X]) P : Ideal R) := by let P' := comap (C : R →+* R[X]) P @@ -455,12 +464,12 @@ theorem isMaximal_comap_C_of_isMaximal [IsJacobson R] [Nontrivial R] have hm' : m ≠ 0 := by simpa [Submodule.coe_eq_zero] using hm let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P (C : R →+* R[X]) le_rfl - let a : R ⧸ P' := (m.map (Quotient.mk P')).leadingCoeff + let a : R ⧸ P' := (m.map (Ideal.Quotient.mk P')).leadingCoeff let M : Submonoid (R ⧸ P') := Submonoid.powers a rw [← bot_quotient_isMaximal_iff] have hp0 : a ≠ 0 := fun hp0' => - hm' <| map_injective (Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R)) - ((injective_iff_map_eq_zero (Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))).2 + hm' <| map_injective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R)) + ((injective_iff_map_eq_zero (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))).2 fun x hx => by rwa [Quotient.eq_zero_iff_mem, (by rwa [eq_bot_iff] : (P.comap C : Ideal R) = ⊥)] at hx) (by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0') @@ -468,7 +477,8 @@ theorem isMaximal_comap_C_of_isMaximal [IsJacobson R] [Nontrivial R] suffices (⊥ : Ideal (Localization M)).IsMaximal by rw [← IsLocalization.comap_map_of_isPrime_disjoint M (Localization M) ⊥ bot_prime (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))] - exact ((isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp (by rwa [map_bot])).1 + exact ((IsLocalization.isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp + (by rwa [Ideal.map_bot])).1 let M' : Submonoid (R[X] ⧸ P) := M.map φ have hM' : (0 : R[X] ⧸ P) ∉ M' := fun ⟨z, hz⟩ => hM (quotientMap_injective (_root_.trans hz.2 φ.map_zero.symm) ▸ hz.1) @@ -483,20 +493,21 @@ theorem isMaximal_comap_C_of_isMaximal [IsJacobson R] [Nontrivial R] exact @isIntegral_isLocalization_polynomial_quotient R _ (Localization M) (Localization M') _ _ P m hmem_P _ _ _ isloc rw [(map_bot.symm : - (⊥ : Ideal (Localization M')) = map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)] + (⊥ : Ideal (Localization M')) = Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)] let bot_maximal := (bot_quotient_isMaximal_iff _).mpr hP refine map.isMaximal (algebraMap (R[X] ⧸ P) (Localization M')) ?_ bot_maximal apply IsField.localization_map_bijective hM' rwa [← Quotient.maximal_ideal_iff_isField_quotient, ← bot_quotient_isMaximal_iff] /-- Used to bootstrap the more general `quotient_mk_comp_C_isIntegral_of_jacobson` -/ -private theorem quotient_mk_comp_C_isIntegral_of_jacobson' [Nontrivial R] (hR : IsJacobson R) - (hP' : ∀ x : R, C x ∈ P → x = 0) : ((Quotient.mk P).comp C : R →+* R[X] ⧸ P).IsIntegral := by +private theorem quotient_mk_comp_C_isIntegral_of_jacobson' [Nontrivial R] (hR : IsJacobsonRing R) + (hP' : ∀ x : R, C x ∈ P → x = 0) : + ((Ideal.Quotient.mk P).comp C : R →+* R[X] ⧸ P).IsIntegral := by refine (isIntegral_quotientMap_iff _).mp ?_ let P' : Ideal R := P.comap C obtain ⟨pX, hpX, hp0⟩ := exists_nonzero_mem_of_ne_bot (ne_of_lt (bot_lt_of_maximal P polynomial_not_isField)).symm hP' - let a : R ⧸ P' := (pX.map (Quotient.mk P')).leadingCoeff + let a : R ⧸ P' := (pX.map (Ideal.Quotient.mk P')).leadingCoeff let M : Submonoid (R ⧸ P') := Submonoid.powers a let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C le_rfl haveI hP'_prime : P'.IsPrime := comap_isPrime C P @@ -524,16 +535,16 @@ private theorem quotient_mk_comp_C_isIntegral_of_jacobson' [Nontrivial R] (hR : (Localization M) (Localization M') _ _ P pX hpX _ _ _ isloc rw [IsLocalization.map_comp M.le_comap_map] -variable [IsJacobson R] +variable [IsJacobsonRing R] /-- If `R` is a Jacobson ring, and `P` is a maximal ideal of `R[X]`, then `R → R[X]/P` is an integral map. -/ -theorem quotient_mk_comp_C_isIntegral_of_jacobson : - ((Quotient.mk P).comp C : R →+* R[X] ⧸ P).IsIntegral := by +theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing : + ((Ideal.Quotient.mk P).comp C : R →+* R[X] ⧸ P).IsIntegral := by let P' : Ideal R := P.comap C haveI : P'.IsPrime := comap_isPrime C P - let f : R[X] →+* Polynomial (R ⧸ P') := Polynomial.mapRingHom (Quotient.mk P') - have hf : Function.Surjective ↑f := map_surjective (Quotient.mk P') Quotient.mk_surjective + let f : R[X] →+* Polynomial (R ⧸ P') := Polynomial.mapRingHom (Ideal.Quotient.mk P') + have hf : Function.Surjective ↑f := map_surjective (Ideal.Quotient.mk P') Quotient.mk_surjective have hPJ : P = (P.map f).comap f := by rw [comap_map_of_surjective _ hf] refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_) @@ -542,33 +553,28 @@ theorem quotient_mk_comp_C_isIntegral_of_jacobson : simpa only [f, coeff_map, coe_mapRingHom] using (Polynomial.ext_iff.mp hp) n refine RingHom.IsIntegral.tower_bot _ _ (injective_quotient_le_comap_map P) ?_ rw [← quotient_mk_maps_eq] - refine ((Quotient.mk P').isIntegral_of_surjective Quotient.mk_surjective).trans _ _ ?_ - have : IsMaximal (map (mapRingHom (Quotient.mk (comap C P))) P) := + refine ((Ideal.Quotient.mk P').isIntegral_of_surjective Quotient.mk_surjective).trans _ _ ?_ + have : IsMaximal (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P) := Or.recOn (map_eq_top_or_isMaximal_of_surjective f hf hP) (fun h => absurd (_root_.trans (h ▸ hPJ : P = comap f ⊤) comap_top : P = ⊤) hP.ne_top) id apply quotient_mk_comp_C_isIntegral_of_jacobson' _ ?_ (fun x hx => ?_) - any_goals exact Ideal.isJacobson_quotient + any_goals exact isJacobsonRing_quotient obtain ⟨z, rfl⟩ := Quotient.mk_surjective x rwa [Quotient.eq_zero_iff_mem, mem_comap, hPJ, mem_comap, coe_mapRingHom, map_C] -theorem isMaximal_comap_C_of_isJacobson : (P.comap (C : R →+* R[X])).IsMaximal := by +theorem isMaximal_comap_C_of_isJacobsonRing : (P.comap (C : R →+* R[X])).IsMaximal := by rw [← @mk_ker _ _ P, RingHom.ker_eq_comap_bot, comap_comap] have := (bot_quotient_isMaximal_iff _).mpr hP - exact isMaximal_comap_of_isIntegral_of_isMaximal' _ (quotient_mk_comp_C_isIntegral_of_jacobson P) - ⊥ + exact isMaximal_comap_of_isIntegral_of_isMaximal' _ + (quotient_mk_comp_C_isIntegral_of_isJacobsonRing P) ⊥ -lemma isMaximal_comap_C_of_isJacobson' {P : Ideal R[X]} (hP : IsMaximal P) : - (P.comap (C : R →+* R[X])).IsMaximal := by - haveI := hP - exact isMaximal_comap_C_of_isJacobson P - -theorem comp_C_integral_of_surjective_of_jacobson {S : Type*} [Field S] (f : R[X] →+* S) +theorem comp_C_integral_of_surjective_of_isJacobsonRing {S : Type*} [Field S] (f : R[X] →+* S) (hf : Function.Surjective ↑f) : (f.comp C).IsIntegral := by haveI : f.ker.IsMaximal := RingHom.ker_isMaximal_of_surjective f hf let g : R[X] ⧸ (RingHom.ker f) →+* S := Ideal.Quotient.lift (RingHom.ker f) f fun _ h => h - have hfg : g.comp (Quotient.mk (RingHom.ker f)) = f := ringHom_ext' rfl rfl + have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f := ringHom_ext' rfl rfl rw [← hfg, RingHom.comp_assoc] - refine (quotient_mk_comp_C_isIntegral_of_jacobson (RingHom.ker f)).trans _ g + refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f)).trans _ g (g.isIntegral_of_surjective ?_) rw [← hfg] at hf norm_num at hf @@ -582,24 +588,24 @@ open MvPolynomial RingHom namespace MvPolynomial -theorem isJacobson_MvPolynomial_fin {R : Type u} [CommRing R] [H : IsJacobson R] : - ∀ n : ℕ, IsJacobson (MvPolynomial (Fin n) R) - | 0 => (isJacobson_iso ((renameEquiv R (Equiv.equivPEmpty (Fin 0))).toRingEquiv.trans +theorem isJacobsonRing_MvPolynomial_fin {R : Type u} [CommRing R] [H : IsJacobsonRing R] : + ∀ n : ℕ, IsJacobsonRing (MvPolynomial (Fin n) R) + | 0 => (isJacobsonRing_iso ((renameEquiv R (Equiv.equivPEmpty (Fin 0))).toRingEquiv.trans (isEmptyRingEquiv R PEmpty.{u+1}))).mpr H - | n + 1 => (isJacobson_iso (finSuccEquiv R n).toRingEquiv).2 - (Polynomial.isJacobson_polynomial_iff_isJacobson.2 (isJacobson_MvPolynomial_fin n)) + | n + 1 => (isJacobsonRing_iso (finSuccEquiv R n).toRingEquiv).2 + (Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing.2 (isJacobsonRing_MvPolynomial_fin n)) /-- General form of the Nullstellensatz for Jacobson rings, since in a Jacobson ring we have `Inf {P maximal | P ≥ I} = Inf {P prime | P ≥ I} = I.radical`. Fields are always Jacobson, and in that special case this is (most of) the classical Nullstellensatz, since `I(V(I))` is the intersection of maximal ideals containing `I`, which is then `I.radical` -/ -instance isJacobson {R : Type*} [CommRing R] {ι : Type*} [Finite ι] [IsJacobson R] : - IsJacobson (MvPolynomial ι R) := by +instance isJacobsonRing {R : Type*} [CommRing R] {ι : Type*} [Finite ι] [IsJacobsonRing R] : + IsJacobsonRing (MvPolynomial ι R) := by cases nonempty_fintype ι haveI := Classical.decEq ι let e := Fintype.equivFin ι - rw [isJacobson_iso (renameEquiv R e).toRingEquiv] - exact isJacobson_MvPolynomial_fin _ + rw [isJacobsonRing_iso (renameEquiv R e).toRingEquiv] + exact isJacobsonRing_MvPolynomial_fin _ variable {n : ℕ} @@ -611,7 +617,7 @@ private noncomputable def Cₐ (R : Type u) (S : Type v) { Polynomial.C with commutes' := fun r => by rfl } private lemma aux_IH {R : Type u} {S : Type v} {T : Type w} - [CommRing R] [CommRing S] [CommRing T] [IsJacobson S] [Algebra R S] [Algebra R T] + [CommRing R] [CommRing S] [CommRing T] [IsJacobsonRing S] [Algebra R S] [Algebra R T] (IH : ∀ (Q : Ideal S), (IsMaximal Q) → RingHom.IsIntegral (algebraMap R (S ⧸ Q))) (v : S[X] ≃ₐ[R] T) (P : Ideal T) (hP : P.IsMaximal) : RingHom.IsIntegral (algebraMap R (T ⧸ P)) := by @@ -631,17 +637,17 @@ private lemma aux_IH {R : Type u} {S : Type v} {T : Type w} apply RingHom.IsIntegral.trans · apply RingHom.IsIntegral.trans · apply IH - apply Polynomial.isMaximal_comap_C_of_isJacobson' - exact hQ + apply Polynomial.isMaximal_comap_C_of_isJacobsonRing · suffices w'.toRingHom = Ideal.quotientMap Q (Polynomial.C) le_rfl by rw [this] rw [isIntegral_quotientMap_iff _] - apply Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson + apply Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing rfl · apply RingHom.isIntegral_of_surjective exact w.surjective -private theorem quotient_mk_comp_C_isIntegral_of_jacobson' {R : Type*} [CommRing R] [IsJacobson R] +private theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing' + {R : Type*} [CommRing R] [IsJacobsonRing R] (P : Ideal (MvPolynomial (Fin n) R)) (hP : P.IsMaximal) : RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P)) := by induction' n with n IH @@ -650,14 +656,14 @@ private theorem quotient_mk_comp_C_isIntegral_of_jacobson' {R : Type*} [CommRing exact C_surjective (Fin 0) · apply aux_IH IH (finSuccEquiv R n).symm P hP -theorem quotient_mk_comp_C_isIntegral_of_jacobson {R : Type*} [CommRing R] [IsJacobson R] +theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R] (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal] : - RingHom.IsIntegral (RingHom.comp (Quotient.mk P) (MvPolynomial.C)) := by + RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) (MvPolynomial.C)) := by change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P)) - apply quotient_mk_comp_C_isIntegral_of_jacobson' + apply quotient_mk_comp_C_isIntegral_of_isJacobsonRing' infer_instance -theorem comp_C_integral_of_surjective_of_jacobson {R : Type*} [CommRing R] [IsJacobson R] +theorem comp_C_integral_of_surjective_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R] {σ : Type*} [Finite σ] {S : Type*} [Field S] (f : MvPolynomial σ R →+* S) (hf : Function.Surjective ↑f) : (f.comp C).IsIntegral := by cases nonempty_fintype σ @@ -669,9 +675,10 @@ theorem comp_C_integral_of_surjective_of_jacobson {R : Type*} [CommRing R] [IsJa haveI : f'.ker.IsMaximal := ker_isMaximal_of_surjective f' hf' let g : MvPolynomial _ R ⧸ (RingHom.ker f') →+* S := Ideal.Quotient.lift (RingHom.ker f') f' fun _ h => h - have hfg : g.comp (Quotient.mk (RingHom.ker f')) = f' := ringHom_ext (fun r => rfl) fun i => rfl + have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' := + ringHom_ext (fun r => rfl) fun i => rfl rw [← hfg, RingHom.comp_assoc] - refine (quotient_mk_comp_C_isIntegral_of_jacobson (RingHom.ker f')).trans _ g + refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g (g.isIntegral_of_surjective ?_) rw [← hfg] at hf' norm_num at hf' @@ -683,4 +690,65 @@ theorem comp_C_integral_of_surjective_of_jacobson {R : Type*} [CommRing R] [IsJa end MvPolynomial +namespace Ideal + +@[deprecated (since := "2024-10-27")] +alias IsJacobson := IsJacobsonRing +@[deprecated (since := "2024-10-27")] +alias isJacobson_iff := isJacobsonRing_iff +@[deprecated (since := "2024-10-27")] +alias IsJacobson.out := IsJacobsonRing.out +@[deprecated (since := "2024-10-27")] +alias isJacobson_iff_prime_eq := isJacobsonRing_iff_prime_eq +@[deprecated (since := "2024-10-27")] +alias isJacobson_iff_sInf_maximal := isJacobsonRing_iff_sInf_maximal +@[deprecated (since := "2024-10-27")] +alias isJacobson_iff_sInf_maximal' := isJacobsonRing_iff_sInf_maximal' +@[deprecated (since := "2024-10-27")] +alias isJacobson_of_surjective := isJacobsonRing_of_surjective +@[deprecated (since := "2024-10-27")] +alias isJacobson_iso := isJacobsonRing_iso +@[deprecated (since := "2024-10-27")] +alias isJacobson_of_isIntegral := isJacobsonRing_of_isIntegral +@[deprecated (since := "2024-10-27")] +alias isJacobson_of_isIntegral' := isJacobsonRing_of_isIntegral' +@[deprecated (since := "2024-10-27")] +alias isMaximal_iff_isMaximal_disjoint := IsLocalization.isMaximal_iff_isMaximal_disjoint +@[deprecated (since := "2024-10-27")] +alias isMaximal_of_isMaximal_disjoint := IsLocalization.isMaximal_of_isMaximal_disjoint +@[deprecated (since := "2024-10-27")] +alias isJacobson_localization := isJacobsonRing_localization + +namespace Polynomial + +@[deprecated (since := "2024-10-27")] +alias isIntegral_isLocalization_polynomial_quotient := isIntegral_isLocalization_polynomial_quotient +@[deprecated (since := "2024-10-27")] +alias jacobson_bot_of_integral_localization := jacobson_bot_of_integral_localization +@[deprecated (since := "2024-10-27")] +alias isJacobson_polynomial_of_isJacobson := isJacobsonRing_polynomial_of_isJacobsonRing +@[deprecated (since := "2024-10-27")] +alias isJacobson_polynomial_iff_isJacobson := isJacobsonRing_polynomial_iff_isJacobsonRing +@[deprecated (since := "2024-10-27")] +alias isMaximal_comap_C_of_isMaximal := isMaximal_comap_C_of_isMaximal +@[deprecated (since := "2024-10-27")] +alias quotient_mk_comp_C_isIntegral_of_jacobson := + Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing +@[deprecated (since := "2024-10-27")] +alias isMaximal_comap_C_of_isJacobson := isMaximal_comap_C_of_isJacobsonRing +@[deprecated (since := "2024-10-27")] +alias comp_C_integral_of_surjective_of_jacobson := + Polynomial.comp_C_integral_of_surjective_of_isJacobsonRing + +end Polynomial + +@[deprecated (since := "2024-10-27")] +alias MvPolynomial.isJacobson_MvPolynomial_fin := isJacobsonRing_MvPolynomial_fin +@[deprecated (since := "2024-10-27")] +alias MvPolynomial.quotient_mk_comp_C_isIntegral_of_jacobson := + MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing +@[deprecated (since := "2024-10-27")] +alias MvPolynomial.comp_C_integral_of_surjective_of_jacobson := + MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing + end Ideal diff --git a/Mathlib/RingTheory/Nullstellensatz.lean b/Mathlib/RingTheory/Nullstellensatz.lean index 4b18643ff516f..c253b46a84278 100644 --- a/Mathlib/RingTheory/Nullstellensatz.lean +++ b/Mathlib/RingTheory/Nullstellensatz.lean @@ -162,7 +162,7 @@ theorem isMaximal_iff_eq_vanishingIdeal_singleton (I : Ideal (MvPolynomial σ k) have hϕ : Function.Bijective ϕ := ⟨quotient_mk_comp_C_injective _ _ I hI.ne_top, IsAlgClosed.algebraMap_surjective_of_isIntegral' ϕ - (MvPolynomial.comp_C_integral_of_surjective_of_jacobson _ Quotient.mk_surjective)⟩ + (MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing _ Quotient.mk_surjective)⟩ obtain ⟨φ, hφ⟩ := Function.Surjective.hasRightInverse hϕ.2 let x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s)) have hx : ∀ s : σ, ϕ (x s) = (Ideal.Quotient.mk I) (X s) := fun s =>