The Jacobson radical of a corner ring

Let e be an idempotent of a ring A and eAe its corner ring (IsIdempotentElem.Corner), with unit e. This file proves that the Jacobson radical of the corner is the corner of the Jacobson radical:

J(eAe) = eJ(A)e = J(A) ∩ eAe.

The proof goes through units. An element x of the corner is a unit of eAe exactly when 1 - e + x is a unit of A (IsIdempotentElem.isUnit_corner_iff): the map x ↦ 1 - e + x is multiplicative, because the cross terms (1 - e) * x and x * (1 - e) vanish, and an inverse w of 1 - e + x in A cuts down to the inverse ewe of x in the corner. With the elementwise descriptions of the radical (TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left and its right-handed form) and the swap 1 + ab ↦ 1 + ba (TauCeti.isUnit_one_add_mul_comm), this compares the radicals.

Combined with the quotient calculation of TauCeti.RingTheory.Idempotents.Quotient, the radical quotient of the corner is the corner of the radical quotient, eAe ⧸ J(eAe) ≃ ē (A ⧸ J(A)) ē (IsIdempotentElem.cornerQuotientJacobsonEquiv). This is how the semisimple part of a corner ring is read off from that of the ambient ring, for instance to recognise a corner ring as basic.

Main definitions

• IsIdempotentElem.cornerQuotientJacobsonEquiv: the radical quotient of the corner eAe is the corner of the radical quotient of A.

Main results

• IsIdempotentElem.isUnit_corner_iff: x is a unit of eAe if and only if 1 - e + x is a unit of A.
• IsIdempotentElem.mem_jacobson_corner_iff: an element of eAe lies in its Jacobson radical if and only if it lies in the Jacobson radical of A.
• IsIdempotentElem.jacobson_corner: J(eAe) = eJ(A)e, as ideals of the corner.

References

• T. Y. Lam, A First Course in Noncommutative Rings, 2nd ed., GTM 131, Springer (2001), §21.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras I, CUP (2006), Section I.6.

theorem IsIdempotentElem.isUnit_corner_iff {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) {x : he.Corner} : IsUnit x ↔ IsUnit (1 - e + ↑x)

Units of a corner ring. An element x of the corner eAe is a unit there exactly when 1 - e + x is a unit of A.

@[simp]

theorem IsIdempotentElem.mem_jacobson_corner_iff {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) {x : he.Corner} : x ∈ Ring.jacobson he.Corner ↔ ↑x ∈ Ring.jacobson A

The Jacobson radical of a corner ring is cut out by the ambient radical. An element of the corner eAe lies in Ring.jacobson eAe exactly when it lies in Ring.jacobson A.

theorem IsIdempotentElem.jacobson_corner {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) : Ring.jacobson he.Corner = he.cornerIdeal (Ring.jacobson A)

J(eAe) = eJ(A)e. The Jacobson radical of the corner ring eAe is the restriction to the corner of the Jacobson radical of A.

noncomputable def IsIdempotentElem.cornerQuotientJacobsonEquiv {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) : he.Corner ⧸ Ring.jacobson he.Corner ≃+* ⋯.Corner

The radical quotient of a corner ring is the corner of the radical quotient: eAe ⧸ J(eAe) ≃ ē (A ⧸ J(A)) ē, where ē is the image of e.

@[simp]

theorem IsIdempotentElem.cornerQuotientJacobsonEquiv_mk {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (x : he.Corner) : he.cornerQuotientJacobsonEquiv ((Ideal.Quotient.mk (Ring.jacobson he.Corner)) x) = (he.cornerQuotientHom (Ring.jacobson A)) x