Ideal.le_jacobson
theorem Ideal.le_jacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I ≤ I.jacobson
This theorem states that for any ring `R` and any ideal `I` in `R`, `I` is a subset of or equal to the Jacobson radical of `I`. In other words, given any ring `R` and an ideal `I` of that ring, every element of `I` is also included in its Jacobson radical. Here, the Jacobson radical of an ideal is defined as the infimum or the greatest lower bound of all maximal left ideals containing `I`.
More concisely: For any ring `R` and ideal `I` in `R`, `I` is contained in the Jacobson radical of `I`.
|
Ideal.IsLocal.out
theorem Ideal.IsLocal.out : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} [self : I.IsLocal], I.jacobson.IsMaximal
This theorem states that for any commutative ring `R` and any ideal `I` in `R`, if `I` is local (i.e., it has the property that it's the only maximal ideal of the ring), then the Jacobson radical of `I` is a maximal ideal. The Jacobson radical of an ideal in a ring is the intersection of all maximal ideals containing that ideal. In simpler terms, this theorem says that in a local ring, the intersection of all maximal ideals that contain a certain ideal also forms a maximal ideal.
More concisely: In a commutative ring, if an ideal is local and maximal, then it is equal to its own Jacobson radical.
|
Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot
theorem Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot :
∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson
This theorem states that for any commutative ring 'R' and an ideal 'I' of 'R', the standard radical of 'I' is equal to its Jacobson radical if and only if the nilradical of the quotient ring 'R/I' is equal to its Jacobson radical. In other words, we can determine if the standard radical and Jacobson radical of an ideal in a commutative ring are the same based on whether the nilradical and Jacobson radical of the corresponding quotient ring coincide.
More concisely: For a commutative ring 'R' and its ideal 'I', the standard radical of 'I' equals the Jacobson radical if and only if the nilradical of 'R/I' equals the Jacobson radical of 'R/I'.
|
Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot
theorem Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot :
∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.jacobson = I ↔ ⊥.jacobson = ⊥
An ideal `I` in a commutative ring `R` is equal to its Jacobson radical if and only if the Jacobson radical of the quotient ring `R/I` is the zero ideal. In other words, for any commutative ring `R` and any ideal `I` in `R`, `I` is the same as its Jacobson radical if and only if the Jacobson radical of the quotient ring formed by `R` over `I` is equivalent to the zero ideal. This theorem provides a criterion to check if an ideal is equal to its Jacobson radical by examining the properties of the quotient ring.
More concisely: An ideal in a commutative ring is equal to its Jacobson radical if and only if the Jacobson radical of the quotient ring formed by the ideal is the zero ideal.
|
Ideal.map_jacobson_of_surjective
theorem Ideal.map_jacobson_of_surjective :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {I : Ideal R} {f : R →+* S},
Function.Surjective ⇑f → RingHom.ker f ≤ I → Ideal.map f I.jacobson = (Ideal.map f I).jacobson
The theorem `Ideal.map_jacobson_of_surjective` states that for any rings `R` and `S`, any ideal `I` of `R`, and any surjective ring homomorphism `f` from `R` to `S`, if the kernel of `f` is a subset of the ideal `I`, then mapping the Jacobson radical of `I` under `f` is equal to the Jacobson radical of the image of `I` under `f`. In other words, under these conditions, the process of taking the Jacobson radical commutes with the process of mapping under a surjective ring homomorphism.
More concisely: If `R` is a ring, `S` is another ring, `I` is an ideal of `R`, and `f : R -> S` is a surjective ring homomorphism with kernel contained in `I`, then `J(f(I)) = f(J(I))`, where `J(X)` denotes the Jacobson radical of `X`.
|
Ideal.eq_jacobson_iff_not_mem
theorem Ideal.eq_jacobson_iff_not_mem :
∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M := by
sorry
This theorem states that for any given ring `R` and an ideal `I` of `R`, `I` is equal to its Jacobson radical if and only if for every element `x` that is not in `I`, there exists a maximal ideal `M` which contains `I` (i.e., `I` is a subset of `M`) and `x` does not belong to `M`. The Jacobson radical of an ideal is the intersection of all maximal ideals containing that ideal. The condition is bidirectional, meaning if `I` equals its Jacobson radical, then every element outside `I` lies outside of a maximal ideal containing `I`, and vice versa.
More concisely: For a ring `R` and ideal `I`, `I` equals its Jacobson radical if and only if for every element `x` not in `I`, there exists a maximal ideal `M` containing `I` such that `x` is not in `M`.
|
Ideal.eq_jacobson_iff_sInf_maximal
theorem Ideal.eq_jacobson_iff_sInf_maximal :
∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = I ↔ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
This theorem states that for any ring `R` and any ideal `I` of `R`, `I` is equal to its Jacobson radical if and only if there exists a set `M` of ideals such that each ideal in `M` is either maximal or equal to the top ideal (`⊤`), and `I` is equal to the intersection of all ideals in `M`. The condition allowing the top ideal in the set `M` is included to simplify some proofs.
More concisely: A ring ideal is equal to its Jacobson radical if and only if there exists a set of ideals, some of which are maximal and some are the top ideal, whose intersection is equal to the ideal.
|