Ideals in a matrix ring

This file defines left (resp. two-sided) ideals in a matrix semiring (resp. ring) over left (resp. two-sided) ideals in the base semiring (resp. ring). We also characterize Jacobson radicals of ideals in such rings.

Main results

• TwoSidedIdeal.equivMatricesOver and TwoSidedIdeal.orderIsoMatricesOver establish an order isomorphism between two-sided ideals in $R$ and those in $Mₙ(R)$.
• TwoSidedIdeal.jacobson_matricesOver shows that $J(Mₙ(I)) = Mₙ(J(I))$ for any two-sided ideal $I ≤ R$.

Left ideals in a matrix semiring

def Ideal.matricesOver {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] (I : Ideal R) : Ideal (Matrix n n R)

The left ideal of matrices with entries in I ≤ R.

Equations

• Ideal.matricesOver n I = { carrier := {M : Matrix n n R | ∀ (i j : n), M i j ∈ I}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Ideal.mem_matricesOver {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] (I : Ideal R) (M : Matrix n n R) : M ∈ matricesOver n I ↔ ∀ (i j : n), M i j ∈ I

theorem Ideal.matricesOver_monotone {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] : Monotone (matricesOver n)

theorem Ideal.matricesOver_strictMono_of_nonempty {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] [Nonempty n] : StrictMono (matricesOver n)

@[simp]

theorem Ideal.matricesOver_bot {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] : matricesOver n ⊥ = ⊥

@[simp]

theorem Ideal.matricesOver_top {R : Type u_1} [Semiring R] (n : Type u_2) [Fintype n] [DecidableEq n] : matricesOver n ⊤ = ⊤

Jacobson radicals of left ideals in a matrix ring

theorem Ideal.single_mem_jacobson_matricesOver {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] (I : Ideal R) (x : R) : x ∈ I.jacobson → ∀ (i j : n), Matrix.single i j x ∈ (matricesOver n I).jacobson

A standard basis matrix is in $J(Mₙ(I))$ as long as its one possibly non-zero entry is in $J(I)$.

@[deprecated Ideal.single_mem_jacobson_matricesOver (since := "2025-05-05")]

theorem Ideal.stdBasisMatrix_mem_jacobson_matricesOver {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] (I : Ideal R) (x : R) : x ∈ I.jacobson → ∀ (i j : n), Matrix.single i j x ∈ (matricesOver n I).jacobson

Alias of Ideal.single_mem_jacobson_matricesOver.

---

A standard basis matrix is in $J(Mₙ(I))$ as long as its one possibly non-zero entry is in $J(I)$.

theorem Ideal.matricesOver_jacobson_le {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] (I : Ideal R) : matricesOver n I.jacobson ≤ (matricesOver n I).jacobson

For any left ideal $I ≤ R$, we have $Mₙ(J(I)) ≤ J(Mₙ(I))$.

Two-sided ideals in a matrix ring

def RingCon.matrix {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] (c : RingCon R) : RingCon (Matrix n n R)

The ring congruence of matrices with entries related by c.

Equations

• RingCon.matrix n c = { r := fun (M N : Matrix n n R) => ∀ (i j : n), c (M i j) (N i j), iseqv := ⋯, mul' := ⋯, add' := ⋯ }

@[simp]

theorem RingCon.matrix_apply {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] {c : RingCon R} {M N : Matrix n n R} : (matrix n c) M N ↔ ∀ (i j : n), c (M i j) (N i j)

@[simp]

theorem RingCon.matrix_apply_single {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] [DecidableEq n] {c : RingCon R} {i j : n} {x y : R} : (matrix n c) (Matrix.single i j x) (Matrix.single i j y) ↔ c x y

@[deprecated RingCon.matrix_apply_single (since := "2025-05-05")]

theorem RingCon.matrix_apply_stdBasisMatrix {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] [DecidableEq n] {c : RingCon R} {i j : n} {x y : R} : (matrix n c) (Matrix.single i j x) (Matrix.single i j y) ↔ c x y

Alias of RingCon.matrix_apply_single.

theorem RingCon.matrix_monotone {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] : Monotone (matrix n)

theorem RingCon.matrix_injective {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] [Nonempty n] : Function.Injective (matrix n)

theorem RingCon.matrix_strictMono_of_nonempty {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] [Nonempty n] : StrictMono (matrix n)

@[simp]

theorem RingCon.matrix_bot {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] : matrix n ⊥ = ⊥

@[simp]

theorem RingCon.matrix_top {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocSemiring R] [Fintype n] : matrix n ⊤ = ⊤

def RingCon.ofMatrix {R : Type u_1} {n : Type u_2} [NonUnitalNonAssocSemiring R] [Fintype n] [DecidableEq n] (c : RingCon (Matrix n n R)) : RingCon R

The congruence relation induced by c on single i j.

Equations

• c.ofMatrix = { r := fun (x y : R) => ∀ (i j : n), c (Matrix.single i j x) (Matrix.single i j y), iseqv := ⋯, mul' := ⋯, add' := ⋯ }

@[simp]

theorem RingCon.ofMatrix_rel {R : Type u_1} {n : Type u_2} [NonUnitalNonAssocSemiring R] [Fintype n] [DecidableEq n] {c : RingCon (Matrix n n R)} {x y : R} : c.ofMatrix x y ↔ ∀ (i j : n), c (Matrix.single i j x) (Matrix.single i j y)

@[simp]

theorem RingCon.ofMatrix_matrix {R : Type u_1} {n : Type u_2} [NonUnitalNonAssocSemiring R] [Fintype n] [DecidableEq n] [Nonempty n] (c : RingCon R) : (matrix n c).ofMatrix = c

@[simp]

theorem RingCon.matrix_ofMatrix {R : Type u_1} {n : Type u_2} [NonAssocSemiring R] [Fintype n] [DecidableEq n] (c : RingCon (Matrix n n R)) : matrix n c.ofMatrix = c

Note that this does not apply to a non-unital ring, with counterexample where the elementwise congruence relation !![⊤,⊤;⊤,(· ≡ · [PMOD 4])] is a ring congruence over Matrix (Fin 2) (Fin 2) 2ℤ.

theorem RingCon.ofMatrix_rel' {R : Type u_1} {n : Type u_2} [NonAssocSemiring R] [Fintype n] [DecidableEq n] {c : RingCon (Matrix n n R)} {x y : R} (i j : n) : c.ofMatrix x y ↔ c (Matrix.single i j x) (Matrix.single i j y)

A version of ofMatrix_rel for a single matrix index, rather than all indices.

theorem RingCon.coe_ofMatrix_eq_relationMap {R : Type u_1} {n : Type u_2} [NonAssocSemiring R] [Fintype n] [DecidableEq n] {c : RingCon (Matrix n n R)} (i j : n) : ⇑c.ofMatrix = Relation.Map (⇑c) (fun (x : Matrix n n R) => x i j) fun (x : Matrix n n R) => x i j

def TwoSidedIdeal.matricesOver {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] (I : TwoSidedIdeal R) : TwoSidedIdeal (Matrix n n R)

The two-sided ideal of matrices with entries in I ≤ R.

Equations

• TwoSidedIdeal.matricesOver n I = { ringCon := RingCon.matrix n I.ringCon }

@[simp]

theorem TwoSidedIdeal.matricesOver_ringCon {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] (I : TwoSidedIdeal R) : (matricesOver n I).ringCon = RingCon.matrix n I.ringCon

@[simp]

theorem TwoSidedIdeal.mem_matricesOver {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] (I : TwoSidedIdeal R) (M : Matrix n n R) : M ∈ matricesOver n I ↔ ∀ (i j : n), M i j ∈ I

theorem TwoSidedIdeal.matricesOver_monotone {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] : Monotone (matricesOver n)

theorem TwoSidedIdeal.matricesOver_strictMono_of_nonempty {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] [h : Nonempty n] : StrictMono (matricesOver n)

@[simp]

theorem TwoSidedIdeal.matricesOver_bot {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] : matricesOver n ⊥ = ⊥

@[simp]

theorem TwoSidedIdeal.matricesOver_top {R : Type u_1} (n : Type u_2) [NonUnitalNonAssocRing R] [Fintype n] : matricesOver n ⊤ = ⊤

def TwoSidedIdeal.equivMatricesOver {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] : TwoSidedIdeal R ≃ TwoSidedIdeal (Matrix n n R)

Two-sided ideals in $R$ correspond bijectively to those in $Mₙ(R)$. Given an ideal $I ≤ R$, we send it to $Mₙ(I)$. Given an ideal $J ≤ Mₙ(R)$, we send it to $\{Nᵢⱼ ∣ ∃ N ∈ J\}$.

Equations

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

@[simp]

theorem TwoSidedIdeal.equivMatricesOver_apply {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (I : TwoSidedIdeal R) : equivMatricesOver I = matricesOver n I

@[simp]

theorem TwoSidedIdeal.equivMatricesOver_symm_apply_ringCon {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (J : TwoSidedIdeal (Matrix n n R)) : (equivMatricesOver.symm J).ringCon = J.ringCon.ofMatrix

theorem TwoSidedIdeal.coe_equivMatricesOver_symm_apply {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (I : TwoSidedIdeal (Matrix n n R)) (i j : n) : ↑(equivMatricesOver.symm I) = {x : R | ∃ N ∈ I, N i j = x}

def TwoSidedIdeal.orderIsoMatricesOver {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] : TwoSidedIdeal R ≃o TwoSidedIdeal (Matrix n n R)

Two-sided ideals in $R$ are order-isomorphic with those in $Mₙ(R)$. See also equivMatricesOver.

Equations

• TwoSidedIdeal.orderIsoMatricesOver = { toEquiv := TwoSidedIdeal.equivMatricesOver, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.orderIsoMatricesOver_symm_apply_ringCon_r {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (J : TwoSidedIdeal (Matrix n n R)) (x y : R) : ((RelIso.symm orderIsoMatricesOver) J).ringCon.toSetoid x y = ∀ (i j : n), J.ringCon (Matrix.single i j x) (Matrix.single i j y)

@[simp]

theorem TwoSidedIdeal.orderIsoMatricesOver_apply_ringCon_r {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (I : TwoSidedIdeal R) (M N : Matrix n n R) : (orderIsoMatricesOver I).ringCon.toSetoid M N = ∀ (i j : n), I.ringCon (M i j) (N i j)

theorem TwoSidedIdeal.asIdeal_matricesOver {R : Type u_1} (n : Type u_2) [Ring R] [Fintype n] [DecidableEq n] (I : TwoSidedIdeal R) : asIdeal (matricesOver n I) = Ideal.matricesOver n (asIdeal I)

Jacobson radicals of two-sided ideals in a matrix ring

theorem TwoSidedIdeal.jacobson_matricesOver {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] (I : TwoSidedIdeal R) : (matricesOver n I).jacobson = matricesOver n I.jacobson

For any two-sided ideal $I ≤ R$, we have $J(Mₙ(I)) = Mₙ(J(I))$.

theorem TwoSidedIdeal.matricesOver_jacobson_bot {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] : matricesOver n ⊥.jacobson = ⊥.jacobson