Iterated corner rings

If e : R is idempotent and f ∈ CornerSubring idem_e is idempotent, then the corner subring of f inside eRe agrees (as a ring) with the corner subring of f viewed in R.

theorem LeanPool.ArtinWedderburn.val_mul_subring {R : Type u_1} [Ring R] (S : NonUnitalSubring R) (a b : ↥S) : ↑(a * b) = ↑a * ↑b

def LeanPool.ArtinWedderburn.nonUnitalSubringEq {R : Type u_1} [Ring R] {S : NonUnitalSubring R} [Ring ↥S] (ha : ∀ (x y : ↥S), ↑(x + y) = ↑x + ↑y) (hs : ∀ (x y : ↥S), ↑(x * y) = ↑x * ↑y) {A : NonUnitalSubring ↥S} {B : NonUnitalSubring R} (h : Subtype.val '' A.carrier = B.carrier) : ↥A ≃+* ↥B

A non-unital subring A of S ⊆ R is isomorphic to any non-unital subring B of R whose carrier matches the image of A under S.val.

Equations

• LeanPool.ArtinWedderburn.nonUnitalSubringEq ha hs h = { toFun := fun (a : ↥A) => ⟨↑↑a, ⋯⟩, invFun := fun (b : ↥B) => ⟨⟨↑b, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

theorem LeanPool.ArtinWedderburn.double_corner_set_eq {R : Type u_2} [Ring R] {e : R} {idem_e : IsIdempotentElem e} (f : ↥(CornerSubring idem_e)) : Subtype.val '' (CornerSubringNonUnital f).carrier = (CornerSubringNonUnital ↑f).carrier

def LeanPool.ArtinWedderburn.cornerRingEqLemma {R : Type u_2} [Ring R] {e : R} {idem_e : IsIdempotentElem e} (f : ↥(CornerSubring idem_e)) (h : Subtype.val '' (CornerSubringNonUnital f).carrier = (CornerSubringNonUnital ↑f).carrier) : ↥(CornerSubringNonUnital f) ≃+* ↥(CornerSubringNonUnital ↑f)

Specialisation of nonUnitalSubringEq to the corner subrings of f and f.val, isolated to work around an elaboration issue with direct application.

Equations

• LeanPool.ArtinWedderburn.cornerRingEqLemma f h = LeanPool.ArtinWedderburn.nonUnitalSubringEq ⋯ ⋯ h

def LeanPool.ArtinWedderburn.cornerRingNonUnitalEq {R : Type u_2} [Ring R] {e : R} {idem_e : IsIdempotentElem e} (f : ↥(CornerSubring idem_e)) : ↥(CornerSubringNonUnital f) ≃+* ↥(CornerSubringNonUnital ↑f)

The non-unital corner subring of f inside the corner ring eRe is isomorphic to the non-unital corner subring of f.val inside R.

Equations

• LeanPool.ArtinWedderburn.cornerRingNonUnitalEq f = LeanPool.ArtinWedderburn.cornerRingEqLemma f ⋯

def LeanPool.ArtinWedderburn.cornerRingUnitalEq {R : Type u_2} [Ring R] {e : R} {idem_e : IsIdempotentElem e} {f : ↥(CornerSubring idem_e)} (idem_f : IsIdempotentElem f) : ↥(CornerSubring idem_f) ≃+* ↥(CornerSubring ⋯)

Unital variant of cornerRingNonUnitalEq: the corner subring of f inside eRe is isomorphic to the corner subring of f.val in R.

Equations

• LeanPool.ArtinWedderburn.cornerRingUnitalEq idem_f = id (LeanPool.ArtinWedderburn.cornerRingNonUnitalEq f)