Ideal.isJacobson_localization
theorem Ideal.isJacobson_localization :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
[inst_3 : IsLocalization.Away y S] [H : Ideal.IsJacobson R], Ideal.IsJacobson S
The theorem `Ideal.isJacobson_localization` states that for any commutative ring `R` and any `S` that is a localization of `R` at the powers of some element `y`, if `R` is a Jacobson ring, then `S` is also a Jacobson ring. A Jacobson ring is one where every prime ideal is an intersection of maximal ideals. In simple terms, this theorem says that the Jacobson property is preserved under taking localizations.
More concisely: If `R` is a commutative Jacobson ring and `S` is a localization of `R` at the powers of some element, then `S` is also a Jacobson ring.
|
Ideal.IsJacobson.out
theorem Ideal.IsJacobson.out :
∀ {R : Type u_3} [inst : CommRing R], Ideal.IsJacobson R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I
This theorem states that in a commutative ring `R`, if `R` has the property of being a Jacobson ring (i.e., `Ideal.IsJacobson R`), then for any ideal `I` of `R` that is a radical ideal (i.e., `Ideal.IsRadical I`), the Jacobson radical of `I` is equal to `I` itself. In mathematical notation, this can be written as: if `R` is a Jacobson ring and `I` is a radical ideal in `R`, then `I = J(I)` where `J(I)` denotes the Jacobson radical of `I`.
More concisely: In a commutative ring `R` with the property of being a Jacobson ring, a radical ideal `I` equals its Jacobson radical `J(I)`.
|
Ideal.isMaximal_of_isMaximal_disjoint
theorem Ideal.isMaximal_of_isMaximal_disjoint :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
[inst_3 : IsLocalization.Away y S] [inst_4 : Ideal.IsJacobson R] (I : Ideal R),
I.IsMaximal → y ∉ I → (Ideal.map (algebraMap R S) I).IsMaximal
This theorem states that in a Jacobson ring `R`, if an ideal `I` is maximal and it does not contain a specific element `y`, then the image of this ideal under the ring homomorphism induced by the algebra structure (given by `algebraMap R S`) in the ring `S` (which is the localization of `R` at `y`) will also be maximal. Here, localization refers to a process in algebra that adds multiplicative inverses to the ring for all elements of the submonoid generated by `y`. Jacobson ring refers to a ring where the Jacobson radical of every right ideal is the intersection of all maximal right ideals.
More concisely: In a Jacobson ring, if a maximal ideal does not contain an element and is taken under the algebra homomorphism to the localization of the ring at that element, the result is a maximal ideal.
|
Ideal.isMaximal_iff_isMaximal_disjoint
theorem Ideal.isMaximal_iff_isMaximal_disjoint :
∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
[inst_3 : IsLocalization.Away y S] [H : Ideal.IsJacobson R] (J : Ideal S),
J.IsMaximal ↔ (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
The theorem `Ideal.isMaximal_iff_isMaximal_disjoint` establishes a correspondence between maximal ideals in the localization of a Jacobson ring `R` at an element `y`, and maximal ideals in the original ring `R` that do not contain `y`. More specifically, for any ideal `J` in the localization, `J` is a maximal ideal if and only if the preimage of `J` under the ring homomorphism (given by the `Algebra` structure from `R` to the localization) is a maximal ideal in `R` and does not contain `y`.
More concisely: A local ideal in the localization of a Jacobson ring at an element is maximal if and only if its preimage in the original ring is a maximal ideal that does not contain that element.
|
Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient
theorem Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient :
∀ {R : Type u_1} [inst : CommRing R] {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
(P : Ideal (Polynomial R)),
∀ pX ∈ P,
∀ [inst_3 : Algebra (R ⧸ Ideal.comap Polynomial.C P) Rₘ]
[inst_4 :
IsLocalization.Away (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ]
[inst_5 : Algebra (Polynomial R ⧸ P) Sₘ]
[inst_6 :
IsLocalization
(Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯)
(Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff))
Sₘ],
(IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral
This theorem states that given a commutative ring `R` and a prime ideal `I` of the polynomial ring `R[X]`, if there's a non-constant polynomial `pX` in this ideal, then mapping `R` to the quotient ring `R[X]/I` results in an integral map when localized at the leading coefficient of the mapped polynomial `pX`. Here, localization is the process of adding multiplicative inverses to a ring, and an integral map is a ring homomorphism where the pre-image of any point in the target is integral over the origin ring. The theorem further specifies that `X` is integral as it satisfies the polynomial `pX` and, since constants are trivially integral, the entire extension will be integral due to the closure properties of addition and multiplication.
More concisely: Given a commutative ring `R`, a prime ideal `I` of the polynomial ring `R[X]`, and a non-constant polynomial `pX` in `I`, the natural homomorphism from `R` to the quotient ring `R[X]/I` is an integral ring homomorphism when localized at the leading coefficient of `pX`, with `X` being integral in the extension.
|
Ideal.isJacobson_iff_sInf_maximal
theorem Ideal.isJacobson_iff_sInf_maximal :
∀ {R : Type u_1} [inst : CommRing R],
Ideal.IsJacobson R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
A commutative ring `R` is defined as a Jacobson ring if and only if, for every prime ideal `I` of `R`, there exists a collection `M` of maximal ideals such that `I` equates to the infimum of the ideals in `M`. Note that the set `M` can also contain the top ideal. This is equivalent to the original definition but offers cleaner proofs.
More concisely: A commutative ring is Jacobson if and only if every prime ideal is the infimum of a collection of maximal ideals, possibly including the top ideal.
|
Ideal.Polynomial.jacobson_bot_of_integral_localization
theorem Ideal.Polynomial.jacobson_bot_of_integral_localization :
∀ {S : Type u_2} [inst : CommRing S] [inst_1 : IsDomain S] {R : Type u_5} [inst_2 : CommRing R]
[inst_3 : IsDomain R] [inst_4 : Ideal.IsJacobson R] (Rₘ : Type u_6) (Sₘ : Type u_7) [inst_5 : CommRing Rₘ]
[inst_6 : CommRing Sₘ] (φ : R →+* S),
Function.Injective ⇑φ →
∀ (x : R),
x ≠ 0 →
∀ [inst_7 : Algebra R Rₘ] [inst_8 : IsLocalization.Away x Rₘ] [inst_9 : Algebra S Sₘ]
[inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ],
(IsLocalization.map Sₘ φ ⋯).IsIntegral → ⊥.jacobson = ⊥
This theorem states that, given a Jacobson ring `R` and a commutative ring `S`, if a function `f : R → S` can be extended to an integral map in the localization of `R` at some non-zero element `x`, then the intersection of all maximal ideals in `S` is trivial, i.e., it contains only the zero element. The extended function is injective, ensuring that distinct elements in `R` map to distinct elements in `S`. The localization of `R` at `x` is isomorphic to a commutative ring `Rₘ`, and the image of the submonoid generated by `x` under `f` defines a localization of `S` isomorphic to a commutative ring `Sₘ`. In this context, an element of an algebra over a commutative ring is said to be integral if it is a root of some monic polynomial with coefficients in the ring.
More concisely: Given a Jacobson ring `R`, a commutative ring `S`, and a function `f : R → S` extendable to integral maps in their respective localizations at some non-zero element `x`, then the intersection of all maximal ideals in `S` is the zero ideal and `f` is an injective homomorphism from `R` to `Sₘ`, where `Rₘ` and `Sₘ` are the localizations of `R` and `S` at `x`, respectively.
|
Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson
theorem Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal],
((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral
The theorem `Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson` states that for any commutative ring `R` that is a Jacobson ring, and any `P` which is a maximal ideal of the polynomial ring `R[X]`, the composed map from `R` to the quotient ring `R[X]/P` that first applies the constant polynomial map `Polynomial.C` and then applies the quotienting map `Ideal.Quotient.mk P`, is an integral map. In other words, every element in `R` gets mapped to an element in the quotient ring `R[X]/P` that is a root of some monic polynomial with coefficients in `R`.
More concisely: For any commutative Jacobson ring `R` and maximal ideal `P` of `R[X]`, the constant polynomial map `Polynomial.C` followed by the quotienting map `Ideal.Quotient.mk P` is an integral map from `R` to `R[X]/P`.
|
Ideal.isJacobson_of_surjective
theorem Ideal.isJacobson_of_surjective :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [H : Ideal.IsJacobson R],
(∃ f, Function.Surjective ⇑f) → Ideal.IsJacobson S
The theorem `Ideal.isJacobson_of_surjective` states that for any two types `R` and `S` (representing rings), if `R` is a Jacobson ring (as indicated by `Ideal.IsJacobson R`), and if there exists a surjective function `f` from `R` to `S` (meaning that each element in `S` can be mapped from an element in `R` using the function `f`), then `S` is also a Jacobson ring. This theorem is defined in the context of two commutative rings `R` and `S` (`CommRing R` and `CommRing S`).
More concisely: If `R` is a Jacobson ring and there exists a surjective homomorphism from `R` to a commutative ring `S`, then `S` is also a Jacobson ring.
|
Ideal.isJacobson_iff_prime_eq
theorem Ideal.isJacobson_iff_prime_eq :
∀ {R : Type u_1} [inst : CommRing R], Ideal.IsJacobson R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
A commutative ring `R` is defined to be a Jacobson ring if and only if for all prime ideals `P` in `R`, the Jacobson radical of `P` is equal to `P` itself. In other words, in a Jacobson ring, every prime ideal is equal to its Jacobson radical. The Jacobson radical of an ideal is the intersection of all maximal ideals containing the ideal. A prime ideal is an ideal in a ring that behaves analogously to a prime number in the integers: if a product of elements is contained in the prime ideal, then at least one of the factors must be too.
More concisely: A commutative ring is a Jacobson ring if and only if every prime ideal equals its Jacobson radical.
|