The Jacobson radical, and semiprimary rings, are left-right symmetric

Ring.jacobson R is the intersection of the maximal left ideals of R, so nothing about the definition is symmetric in the two sides. Mathlib knows the resulting ideal is two-sided, but it does not record the sharper statement that the same ideal is cut out by the maximal right ideals, and consequently it leaves the transfer of IsSemiprimaryRing to the opposite ring as a proof_wanted in Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean, annotated "Need left-right symmetry of Jacobson radical".

This file supplies that symmetry and the two consequences it was wanted for. The route is the elementwise description of the radical: x lies in Ring.jacobson R exactly when 1 + y * x is a unit for every y, and hence, by TauCeti.isUnit_one_add_mul_comm, exactly when 1 + x * y is a unit for every y. The second description is the first one read in Rᵐᵒᵖ, so the radical of the opposite ring is the opposite of the radical.

Mathlib proves the elementwise description only over a commutative ring (Ideal.mem_jacobson_bot), where left-right symmetry is vacuous; the noncommutative statement here is what carries the content. The one extra step over the commutative case is that membership in the radical only supplies a left inverse for 1 + y * x, so the argument has to promote that left inverse to a two-sided one.

Main results

• TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left and TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_right: the two elementwise descriptions of the Jacobson radical of a ring.
• TauCeti.Ring.op_mem_jacobson_mulOpposite_iff: MulOpposite.op x lies in Ring.jacobson Rᵐᵒᵖ exactly when x lies in Ring.jacobson R -- the left-right symmetry, in membership form.
• TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv: the resulting identification Rᵐᵒᵖ ⧸ Ring.jacobson Rᵐᵒᵖ ≃+* (R ⧸ Ring.jacobson R)ᵐᵒᵖ.
• TauCeti.isSemiprimaryRing_mulOpposite_iff and TauCeti.IsSemiprimaryRing.mulOpposite: semiprimarity passes to the opposite ring.
• TauCeti.IsArtinianRing.isNoetherianRing_iff_isArtinianRing_mulOpposite: a left Artinian ring is right Noetherian exactly when it is right Artinian, the statement that WedderburnArtin.lean records as waiting on the same symmetry.

theorem TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left {R : Type u_1} [Ring R] {x : R} : x ∈ Ring.jacobson R ↔ ∀ (y : R), IsUnit (1 + y * x)

The Jacobson radical of a ring is {x | ∀ y, IsUnit (1 + y * x)}.

Mathlib's Ideal.mem_jacobson_bot is this statement over a commutative ring.

theorem TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_right {R : Type u_1} [Ring R] {x : R} : x ∈ Ring.jacobson R ↔ ∀ (y : R), IsUnit (1 + x * y)

The right-handed description of the Jacobson radical: it is also {x | ∀ y, IsUnit (1 + x*y)}.

This is where the left-right symmetry enters: the two descriptions differ only by the swap TauCeti.isUnit_one_add_mul_comm.

theorem TauCeti.Ring.op_mem_jacobson_mulOpposite_iff {R : Type u_1} [Ring R] {x : R} : MulOpposite.op x ∈ Ring.jacobson Rᵐᵒᵖ ↔ x ∈ Ring.jacobson R

Left-right symmetry of the Jacobson radical: the intersection of the maximal left ideals of Rᵐᵒᵖ is the opposite of the intersection of the maximal left ideals of R, which is to say that the Jacobson radical of R is also the intersection of its maximal right ideals.

@[simp]

theorem TauCeti.Ring.mem_jacobson_mulOpposite_iff {R : Type u_1} [Ring R] {X : Rᵐᵒᵖ} : X ∈ Ring.jacobson Rᵐᵒᵖ ↔ MulOpposite.unop X ∈ Ring.jacobson R

TauCeti.Ring.op_mem_jacobson_mulOpposite_iff phrased for an element of Rᵐᵒᵖ.

theorem TauCeti.Ring.coe_jacobson_mulOpposite (R : Type u_2) [Ring R] : ↑(Ring.jacobson Rᵐᵒᵖ) = MulOpposite.unop ⁻¹' ↑(Ring.jacobson R)

The Jacobson radical of Rᵐᵒᵖ is, as a set, the op-image of the Jacobson radical of R.

theorem TauCeti.Ring.op_mem_jacobson_mulOpposite_pow_iff {R : Type u_1} [Ring R] {x : R} {n : ℕ} : MulOpposite.op x ∈ Ring.jacobson Rᵐᵒᵖ ^ n ↔ x ∈ Ring.jacobson R ^ n

The left-right symmetry of the Jacobson radical, at the level of powers: op x lies in the n-th power of Ring.jacobson Rᵐᵒᵖ exactly when x lies in the n-th power of Ring.jacobson R.

@[simp]

theorem TauCeti.Ring.mem_jacobson_mulOpposite_pow_iff {R : Type u_1} [Ring R] {X : Rᵐᵒᵖ} {n : ℕ} : X ∈ Ring.jacobson Rᵐᵒᵖ ^ n ↔ MulOpposite.unop X ∈ Ring.jacobson R ^ n

TauCeti.Ring.op_mem_jacobson_mulOpposite_pow_iff phrased for an element of Rᵐᵒᵖ.

theorem TauCeti.Ring.isNilpotent_jacobson_mulOpposite_iff (R : Type u_1) [Ring R] : IsNilpotent (Ring.jacobson Rᵐᵒᵖ) ↔ IsNilpotent (Ring.jacobson R)

Nilpotence of the Jacobson radical is left-right symmetric: the two radicals have the same vanishing powers.

noncomputable def TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv (R : Type u_1) [Ring R] : Rᵐᵒᵖ ⧸ Ring.jacobson Rᵐᵒᵖ ≃+* (R ⧸ Ring.jacobson R)ᵐᵒᵖ

Reduction modulo the Jacobson radical commutes with passing to the opposite ring.

Equations

• TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv R = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

@[simp]

theorem TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv_mk (R : Type u_1) [Ring R] (x : R) : (quotientJacobsonMulOppositeRingEquiv R) ((Ideal.Quotient.mk (Ring.jacobson Rᵐᵒᵖ)) (MulOpposite.op x)) = MulOpposite.op ((Ideal.Quotient.mk (Ring.jacobson R)) x)

TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv is reduction modulo the radical read in Rᵐᵒᵖ: it sends the class of op x to the opposite of the class of x.

@[simp]

theorem TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv_symm_op_mk (R : Type u_1) [Ring R] (x : R) : (quotientJacobsonMulOppositeRingEquiv R).symm (MulOpposite.op ((Ideal.Quotient.mk (Ring.jacobson R)) x)) = (Ideal.Quotient.mk (Ring.jacobson Rᵐᵒᵖ)) (MulOpposite.op x)

The inverse of TauCeti.Ring.quotientJacobsonMulOppositeRingEquiv, on generators.

theorem TauCeti.Ring.isSemisimpleRing_quotient_jacobson_mulOpposite_iff (R : Type u_1) [Ring R] : IsSemisimpleRing (Rᵐᵒᵖ ⧸ Ring.jacobson Rᵐᵒᵖ) ↔ IsSemisimpleRing (R ⧸ Ring.jacobson R)

Semisimplicity of the quotient by the Jacobson radical is left-right symmetric.

theorem TauCeti.isSemiprimaryRing_mulOpposite_iff (R : Type u_1) [Ring R] : IsSemiprimaryRing Rᵐᵒᵖ ↔ IsSemiprimaryRing R

Semiprimarity is left-right symmetric, discharging Mathlib's proof_wanted isSemiprimaryRing_mulOpposite_iff.

instance TauCeti.IsSemiprimaryRing.mulOpposite (R : Type u_1) [Ring R] [IsSemiprimaryRing R] : IsSemiprimaryRing Rᵐᵒᵖ

The opposite of a semiprimary ring is semiprimary, discharging Mathlib's proof_wanted IsSemiprimaryRing.mulOpposite.

theorem TauCeti.IsArtinianRing.isNoetherianRing_iff_isArtinianRing_mulOpposite (R : Type u_1) [Ring R] [IsArtinianRing R] : IsNoetherianRing Rᵐᵒᵖ ↔ IsArtinianRing Rᵐᵒᵖ

For a left Artinian ring, being right Noetherian and being right Artinian coincide: the opposite ring is semiprimary, so Hopkins-Levitzki applies to it. This is the example that Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean leaves open.