Corner subrings eRe

For an idempotent e : R, the corner subring eRe is the non-unital subring of R consisting of elements of the form e * x * e. It becomes a (unital) ring with 1 = e. This file develops the basic theory: containment, artinianness, primality, lifts and pushes of ideals, and isomorphisms between corner subrings of equal idempotents.

def LeanPool.ArtinWedderburn.CornerRingSet {R : Type u_1} [Ring R] (e : R) : Set R

The carrier set of the corner ring eRe, defined as {e * x * e | x : R}.

Equations

• LeanPool.ArtinWedderburn.CornerRingSet e = LeanPool.ArtinWedderburn.bothMul e e

theorem LeanPool.ArtinWedderburn.corner_ring_set_mem {R : Type u_1} [Ring R] {e x : R} (idem_e : IsIdempotentElem e) : x ∈ CornerRingSet e ↔ x = e * x * e

theorem LeanPool.ArtinWedderburn.x_in_corner_x_eq_e_y_e {R : Type u_1} [Ring R] {e x : R} (h : x ∈ CornerRingSet e) : ∃ (y : R), x = e * y * e

@[reducible]

def LeanPool.ArtinWedderburn.CornerSubringNonUnital {R : Type u_1} [Ring R] (e : R) : NonUnitalSubring R

The nonunital corner subring eRe as a NonUnitalSubring.

Equations

• LeanPool.ArtinWedderburn.CornerSubringNonUnital e = { carrier := LeanPool.ArtinWedderburn.bothMul e e, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

theorem LeanPool.ArtinWedderburn.corner_ring_carrier {R : Type u_1} [Ring R] {e : R} : (CornerSubringNonUnital e).carrier = bothMul e e

theorem LeanPool.ArtinWedderburn.el_in_corner_ring {R : Type u_1} [Ring R] {e : R} (x : R) : x ∈ bothMul e e ↔ x ∈ CornerSubringNonUnital e

theorem LeanPool.ArtinWedderburn.eq_carrier_eq_corner {R : Type u_1} [Ring R] (x y : R) (h : bothMul x x = bothMul y y) : CornerSubringNonUnital x = CornerSubringNonUnital y

@[reducible]

def LeanPool.ArtinWedderburn.CornerSubring {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : NonUnitalSubring R

The corner subring eRe packaged as a NonUnitalSubring, tagged with the proof that e is idempotent. The proof argument lets later constructions attach the unital ring structure on eRe.

Equations

• LeanPool.ArtinWedderburn.CornerSubring idem_e = LeanPool.ArtinWedderburn.CornerSubringNonUnital e

theorem LeanPool.ArtinWedderburn.CornerSubringEq {R : Type u_1} [Ring R] {e : R} (idem_e idem_e' : IsIdempotentElem e) : CornerSubring idem_e = CornerSubring idem_e'

theorem LeanPool.ArtinWedderburn.subring_mem_idem {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) {x : R} : x ∈ CornerSubring idem_e ↔ x = e * x * e

theorem LeanPool.ArtinWedderburn.corner_ring_both_mul_mem {R : Type u_1} [Ring R] {e : R} (x w y : R) (hx : x ∈ CornerSubringNonUnital e) (hy : y ∈ CornerSubringNonUnital e) : x * w * y ∈ CornerSubringNonUnital e

theorem LeanPool.ArtinWedderburn.left_unit_mul {R : Type u_1} [Ring R] {e x : R} (idem_e : IsIdempotentElem e) (h : x ∈ CornerSubringNonUnital e) : e * x = x

theorem LeanPool.ArtinWedderburn.right_unit_mul {R : Type u_1} [Ring R] {e x : R} (idem_e : IsIdempotentElem e) (h : x ∈ CornerSubringNonUnital e) : x * e = x

@[reducible, inline]

abbrev LeanPool.ArtinWedderburn.CornerSubringIsNonUNitalRing {R : Type u_1} [Ring R] {e : R} : NonUnitalRing ↥(CornerSubringNonUnital e)

The non-unital ring instance on the corner subring eRe.

Equations

• LeanPool.ArtinWedderburn.CornerSubringIsNonUNitalRing = NonUnitalSubringClass.toNonUnitalRing (LeanPool.ArtinWedderburn.CornerSubringNonUnital e)

theorem LeanPool.ArtinWedderburn.corner_ring_hom {R : Type u_1} [Ring R] {e : R} (a b : ↥(CornerSubringNonUnital e)) : ↑(a * b) = ↑a * ↑b

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.CornerRingOne {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : One ↥(CornerSubring idem_e)

Equations

• LeanPool.ArtinWedderburn.CornerRingOne idem_e = { one := ⟨e, ⋯⟩ }

theorem LeanPool.ArtinWedderburn.corner_ring_one {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : ↑1 = e

theorem LeanPool.ArtinWedderburn.is_left_unit {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x : ↥(CornerSubring idem_e)) : 1 * x = x

theorem LeanPool.ArtinWedderburn.is_right_unit {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x : ↥(CornerSubring idem_e)) : x * 1 = x

theorem LeanPool.ArtinWedderburn.e_in_corner_ring {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : e ∈ CornerSubring idem_e

theorem LeanPool.ArtinWedderburn.both_mul_one_one_eq_R {R : Type u_1} [Ring R] : bothMul 1 1 = ⊤

def LeanPool.ArtinWedderburn.topSubringEquivRing {R : Type u_1} [Ring R] (S : NonUnitalSubring R) (h : S.carrier = ⊤) : ↥S ≃+* R

A non-unital subring whose carrier is all of R is ring-isomorphic to R.

Equations

• LeanPool.ArtinWedderburn.topSubringEquivRing S h = { toFun := fun (a : ↥S) => ↑a, invFun := fun (a : R) => ⟨a, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

def LeanPool.ArtinWedderburn.isoCornerOne {R : Type u_1} [Ring R] : ↥(CornerSubring ⋯) ≃+* R

The corner subring of 1 is ring-isomorphic to the ambient ring R.

Equations

• LeanPool.ArtinWedderburn.isoCornerOne = LeanPool.ArtinWedderburn.topSubringEquivRing (LeanPool.ArtinWedderburn.CornerSubring ⋯) ⋯

theorem LeanPool.ArtinWedderburn.nonzero {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x : ↥(CornerSubring idem_e)) : x ≠ 0 ↔ ↑x ≠ 0

theorem LeanPool.ArtinWedderburn.e_nonzero_corner_nontrivial (R : Type u_2) [Ring R] {e : R} (idem_e : IsIdempotentElem e) (e_nonzero : e ≠ 0) : Nontrivial ↥(CornerSubring idem_e)

theorem LeanPool.ArtinWedderburn.eq_iff_val {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x y z : ↥(CornerSubring idem_e)) : ↑(x + y) = ↑z ↔ ↑x + ↑y = ↑z

theorem LeanPool.ArtinWedderburn.e_x_e_in_corner {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x : R) : e * x * e ∈ CornerSubring idem_e

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.CornerRingIsRing {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : Ring ↥(CornerSubring idem_e)

Equations

• LeanPool.ArtinWedderburn.CornerRingIsRing idem_e = LeanPool.ArtinWedderburn.nonUnitalWEIsRing 1 ⋯ ⋯

def LeanPool.ArtinWedderburn.coercionToERe {R : Type u_1} [Ring R] (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (f_mem : f ∈ CornerSubring idem_e) (x : ↥(CornerSubring idem_f)) : ↥(CornerSubring idem_e)

Lift an element of the corner subring fRf (where f lies in eRe) to an element of the outer corner subring eRe.

Equations

• LeanPool.ArtinWedderburn.coercionToERe e f idem_e idem_f f_mem x = ⟨↑x, ⋯⟩

theorem LeanPool.ArtinWedderburn.corner_ring_division_e_nonzero {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (heRe : IsDivisionRing ↥(CornerSubring idem_e)) : e ≠ 0

def LeanPool.ArtinWedderburn.eqElIsoCorner {R : Type u_1} [Ring R] (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (e_eq_f : e = f) : ↥(CornerSubring idem_e) ≃+* ↥(CornerSubring idem_f)

If e = f, then the corner subrings eRe and fRf are ring-isomorphic via the identity on carriers.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.ArtinWedderburn.equalElIsoMatrixRings' {R : Type u_1} [Ring R] (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (e_eq_f : e = f) (n : ℕ) : Matrix (Fin n) (Fin n) ↥(CornerSubring idem_e) ≃+* Matrix (Fin n) (Fin n) ↥(CornerSubring idem_f)

Equal idempotents induce a ring isomorphism between the matrix rings over their corner subrings.

Equations

• LeanPool.ArtinWedderburn.equalElIsoMatrixRings' e f idem_e idem_f e_eq_f n = (LeanPool.ArtinWedderburn.eqElIsoCorner e f idem_e idem_f e_eq_f).mapMatrix

def LeanPool.ArtinWedderburn.equalElIsoMatrixRings {R : Type u_1} [Ring R] (e f : R) (idem_e : IsIdempotentElem e) (idem_f : IsIdempotentElem f) (e_eq_f : e = f) (n : ℕ) : Matrix (Fin n) (Fin n) ↥(CornerSubringNonUnital e) ≃+* Matrix (Fin n) (Fin n) ↥(CornerSubringNonUnital f)

Equal idempotents induce a ring isomorphism between matrix rings over their non-unital corner subrings.

Equations

• LeanPool.ArtinWedderburn.equalElIsoMatrixRings e f idem_e idem_f e_eq_f n = LeanPool.ArtinWedderburn.equalElIsoMatrixRings' e f idem_e idem_f e_eq_f n

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.instCoeOutSetSubtypeMemNonUnitalSubringCornerSubring {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : CoeOut (Set ↥(CornerSubring idem_e)) (Set R)

Equations

• LeanPool.ArtinWedderburn.instCoeOutSetSubtypeMemNonUnitalSubringCornerSubring idem_e = { coe := fun (X : Set ↥(LeanPool.ArtinWedderburn.CornerSubring idem_e)) => Subtype.val '' X }

def LeanPool.ArtinWedderburn.idealLift {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (I : Ideal ↥(CornerSubring idem_e)) : Ideal R

Lift a (left) ideal of the corner subring eRe to a (left) ideal of R by taking the R-span of its carrier.

Equations

• LeanPool.ArtinWedderburn.idealLift idem_e I = Ideal.span (Subtype.val '' I.carrier)

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.instCoeOutIdealSubtypeMemNonUnitalSubringCornerSubring {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) : CoeOut (Ideal ↥(CornerSubring idem_e)) (Ideal R)

Equations

• LeanPool.ArtinWedderburn.instCoeOutIdealSubtypeMemNonUnitalSubringCornerSubring idem_e = { coe := LeanPool.ArtinWedderburn.idealLift idem_e }

theorem LeanPool.ArtinWedderburn.lift_monotonicity {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (I J : Ideal ↥(CornerSubring idem_e)) : I ≤ J → idealLift idem_e I ≤ idealLift idem_e J

def LeanPool.ArtinWedderburn.elPush {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x : R) : ↥(CornerSubring idem_e)

Push an element x : R into the corner subring eRe via x ↦ e * x * e.

Equations

• LeanPool.ArtinWedderburn.elPush idem_e x = ⟨e * x * e, ⋯⟩

def LeanPool.ArtinWedderburn.idealPush {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (J : Ideal R) : Ideal ↥(CornerSubring idem_e)

Push a (left) ideal of R down to a (left) ideal of eRe by taking the elementwise image under elPush.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.ArtinWedderburn.add_el_push_eq_add {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x y : R) : elPush idem_e x + elPush idem_e y = elPush idem_e (x + y)

theorem LeanPool.ArtinWedderburn.el_push_smul_in_I {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (a y : R) (I : Ideal ↥(CornerSubring idem_e)) : y ∈ Subtype.val '' I.carrier → elPush idem_e (a • y) ∈ I

theorem LeanPool.ArtinWedderburn.ideal_push_pull_inclusion {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (I : Ideal ↥(CornerSubring idem_e)) (x : R) : x ∈ idealLift idem_e I → elPush idem_e x ∈ I

theorem LeanPool.ArtinWedderburn.push_pull {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (I : Ideal ↥(CornerSubring idem_e)) : idealPush idem_e (idealLift idem_e I) = I

theorem LeanPool.ArtinWedderburn.lift_strict_monotonicity {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (I J : Ideal ↥(CornerSubring idem_e)) : I < J → idealLift idem_e I < idealLift idem_e J

theorem LeanPool.ArtinWedderburn.lift_acc_then_ideal_acc {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (J : Ideal R) (h_J_is_lift : ∃ (I3 : Ideal ↥(CornerSubring idem_e)), J = idealLift idem_e I3) (h_acc_J : Acc (fun (x y : Ideal R) => x < y) J) : Acc (fun (x y : Ideal ↥(CornerSubring idem_e)) => x < y) (idealPush idem_e J)

theorem LeanPool.ArtinWedderburn.corner_ring_artinian {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) [h_ar : IsArtinian R R] : IsArtinian ↥(CornerSubring idem_e) ↥(CornerSubring idem_e)

theorem LeanPool.ArtinWedderburn.corner_ring_both_mul_mem' {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x y : ↥(CornerSubring idem_e)) (w : R) : ↑x * w * ↑y ∈ CornerSubring idem_e

theorem LeanPool.ArtinWedderburn.both_mul_lift {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (x y : ↥(CornerSubring idem_e)) : Subtype.val '' bothMul x y = bothMul ↑x ↑y

theorem LeanPool.ArtinWedderburn.corner_ring_prime {R : Type u_1} [Ring R] {e : R} (idem_e : IsIdempotentElem e) (hRP : IsPrimeRing R) : IsPrimeRing ↥(CornerSubring idem_e)

theorem LeanPool.ArtinWedderburn.div_subring_to_div_ring {R : Type u_1} [Ring R] (e : R) (idem_e : IsIdempotentElem e) (h : IsDivisionSubring (CornerSubringNonUnital e) e) : IsDivisionRing ↥(CornerSubring idem_e)