Quotients of idempotent corners

For an idempotent e of a ring A and a two-sided ideal I, taking the corner commutes with passing to the quotient:

eAe / eIe ≃ e'(A/I)e', where e' is the image of e.

Here eIe consists of the elements of the corner whose ambient value lies in I. The quotient map is surjective on corners: lift an element of the target and multiply its lift by e on both sides. Its kernel is precisely eIe. The equivalence is also an algebra equivalence when A is an algebra over a commutative semiring.

The ideal eIe is nilpotent whenever I is nilpotent, with the same vanishing exponent. Applied to the Jacobson radical of an Artinian algebra, these facts compute the quotient of a corner by a nilpotent ideal. This is the quotient calculation used when selecting one primitive idempotent from each simple-module isomorphism class to obtain a basic algebra.

The equivalences use Mathlib's first isomorphism theorem RingHom.quotientKerEquivOfSurjective.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Sections I.4 and I.6.

def IsIdempotentElem.cornerIdeal {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) : Ideal he.Corner

The left ideal I ∩ eAe of the corner: its elements have ambient value in I. For two-sided I, this is the ideal eIe.

@[simp]

theorem IsIdempotentElem.mem_cornerIdeal {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) (x : he.Corner) : x ∈ he.cornerIdeal I ↔ ↑x ∈ I

@[simp]

theorem IsIdempotentElem.cornerIdeal_bot {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) : he.cornerIdeal ⊥ = ⊥

@[simp]

theorem IsIdempotentElem.cornerIdeal_top {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) : he.cornerIdeal ⊤ = ⊤

instance IsIdempotentElem.cornerIdeal_isTwoSided {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] : (he.cornerIdeal I).IsTwoSided

theorem IsIdempotentElem.cornerIdeal_pow_le {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) (n : ℕ) : he.cornerIdeal I ^ n ≤ he.cornerIdeal (I ^ n)

The nth power of a restricted ideal is contained in the restriction of Iⁿ. The reverse inclusion need not hold.

theorem IsIdempotentElem.cornerIdeal_pow_eq_bot {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) {n : ℕ} (hI : I ^ n = ⊥) : he.cornerIdeal I ^ n = ⊥

A power vanishing in the ambient ring also vanishes in the corner ideal.

theorem IsIdempotentElem.isNilpotent_cornerIdeal {A : Type u_1} [Semiring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) (hI : IsNilpotent I) : IsNilpotent (he.cornerIdeal I)

Restricting a nilpotent ideal to an idempotent corner preserves nilpotence.

def IsIdempotentElem.cornerQuotientHom {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] : he.Corner →+* ⋯.Corner

The quotient homomorphism restricted to the corner eAe.

@[simp]

theorem IsIdempotentElem.val_cornerQuotientHom {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] (x : he.Corner) : ↑((he.cornerQuotientHom I) x) = (Ideal.Quotient.mk I) ↑x

theorem IsIdempotentElem.cornerQuotientHom_surjective {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] : Function.Surjective ⇑(he.cornerQuotientHom I)

The quotient homomorphism is surjective on the corner, even when e is not full.

@[simp]

theorem IsIdempotentElem.ker_cornerQuotientHom {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] : RingHom.ker (he.cornerQuotientHom I) = he.cornerIdeal I

noncomputable def IsIdempotentElem.cornerQuotientEquiv {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] : he.Corner ⧸ he.cornerIdeal I ≃+* ⋯.Corner

Taking an idempotent corner commutes with quotienting by a two-sided ideal.

@[simp]

theorem IsIdempotentElem.cornerQuotientEquiv_mk {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] (x : he.Corner) : (he.cornerQuotientEquiv I) ((Ideal.Quotient.mk (he.cornerIdeal I)) x) = (he.cornerQuotientHom I) x

noncomputable def IsIdempotentElem.cornerQuotientAlgEquiv {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] (R : Type u_2) [CommSemiring R] [Algebra R A] : (he.Corner ⧸ he.cornerIdeal I) ≃ₐ[R] ⋯.Corner

The corner quotient equivalence preserves the scalar algebra structure.

@[simp]

theorem IsIdempotentElem.cornerQuotientAlgEquiv_mk {A : Type u_1} [Ring A] {e : A} (he : IsIdempotentElem e) (I : Ideal A) [I.IsTwoSided] (R : Type u_2) [CommSemiring R] [Algebra R A] (x : he.Corner) : (he.cornerQuotientAlgEquiv I R) ((Ideal.Quotient.mk (he.cornerIdeal I)) x) = (he.cornerQuotientHom I) x