Documentation

TauCeti.RingTheory.Idempotents.Matrix

The corner of a diagonal matrix unit #

For a ring α and an index i, the diagonal matrix unit Eᵢᵢ = Matrix.single i i 1 is an idempotent of Matrix n n α. Its corner Eᵢᵢ · Matrix n n α · Eᵢᵢ consists of the matrices supported on the entry (i, i), so it is a copy of α; and Eᵢᵢ is full, generating the whole matrix ring as a two-sided ideal, because 1 = ∑ⱼ Eⱼᵢ Eᵢᵢ Eᵢⱼ.

Together these say that α is a full idempotent corner of Matrix n n α, the standard instance of Morita equivalence. In a product of matrix rings over division rings, one such unit per factor selects a full idempotent whose corner is a product of division rings.

Main definitions #

Main results #

source
@[simp]
theorem Matrix.isIdempotentElem_single_one {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [NonAssocSemiring α] (i : n) :
IsIdempotentElem (single i i 1)

The diagonal matrix unit Eᵢᵢ is idempotent.

source
theorem Matrix.single_apply_eq_of_mem_corner {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [Semiring α] {i : n} {x : Matrix n n α} (hx : x ∈ Subsemigroup.corner (single i i 1)) :
single i i (x i i) = x

A matrix in the corner of Eᵢᵢ is supported on the entry (i, i).

source
def Matrix.cornerSingleOneEquiv {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [Semiring α] (i : n) :
⋯.Corner ≃+* α

The corner of the diagonal matrix unit Eᵢᵢ is the coefficient ring, through the (i, i) entry.

Instances For
    source
    @[simp]
    theorem Matrix.cornerSingleOneEquiv_apply {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [Semiring α] (i : n) (x : ⋯.Corner) :
    (cornerSingleOneEquiv i) x = ↑x i i
    source
    @[simp]
    theorem Matrix.val_cornerSingleOneEquiv_symm_apply {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [Semiring α] (i : n) (a : α) :
    ↑((cornerSingleOneEquiv i).symm a) = single i i a
    source
    theorem Matrix.twoSidedIdeal_span_single_one_eq_top {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [NonAssocRing α] (i : n) :
    TwoSidedIdeal.span {single i i 1} = ⊤

    The diagonal matrix unit Eᵢᵢ is full: it generates Matrix n n α as a two-sided ideal, since 1 = ∑ⱼ Eⱼᵢ Eᵢᵢ Eᵢⱼ.