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.equivMatrix and TwoSidedIdeal.orderIsoMatrix establish an order isomorphism between two-sided ideals in $R$ and those in $Mₙ(R)$.
• TwoSidedIdeal.jacobson_matrix shows that $J(Mₙ(I)) = Mₙ(J(I))$ for any two-sided ideal $I ≤ R$.

Left ideals in a matrix semiring

def Ideal.matrix {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.matrix n I = { toAddSubmonoid := I.matrix, smul_mem' := ⋯ }

@[deprecated Ideal.matrix (since := "2025-07-28")]

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)

Alias of Ideal.matrix.

---

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

Equations

• @Ideal.matricesOver = @Ideal.matrix

@[simp]

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

@[deprecated Ideal.mem_matrix (since := "2025-07-28")]

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 ∈ matrix n I ↔ ∀ (i j : n), M i j ∈ I

Alias of Ideal.mem_matrix.

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

@[deprecated Ideal.matrix_monotone (since := "2025-07-28")]

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

Alias of Ideal.matrix_monotone.

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

@[deprecated Ideal.matrix_strictMono_of_nonempty (since := "2025-07-28")]

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

Alias of Ideal.matrix_strictMono_of_nonempty.

@[simp]

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

@[deprecated Ideal.matrix_bot (since := "2025-07-28")]

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

Alias of Ideal.matrix_bot.

@[simp]

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

@[deprecated Ideal.matrix_top (since := "2025-07-28")]

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

Alias of Ideal.matrix_top.

Jacobson radicals of left ideals in a matrix ring

theorem Ideal.single_mem_jacobson_matrix {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 ∈ (matrix 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_matrix (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 ∈ (matrix n I).jacobson

Alias of Ideal.single_mem_jacobson_matrix.

---

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_matrix (since := "2025-07-28")]

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 ∈ (matrix n I).jacobson

Alias of Ideal.single_mem_jacobson_matrix.

---

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

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

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

@[deprecated Ideal.matrix_jacobson_le (since := "2025-07-28")]

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

Alias of Ideal.matrix_jacobson_le.

---

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.matrix {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.matrix n I = { ringCon := RingCon.matrix n I.ringCon }

@[simp]

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

@[deprecated TwoSidedIdeal.matrix (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix.

---

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

Equations

• @TwoSidedIdeal.matricesOver = @TwoSidedIdeal.matrix

@[simp]

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

@[deprecated TwoSidedIdeal.mem_matrix (since := "2025-07-28")]

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 ∈ matrix n I ↔ ∀ (i j : n), M i j ∈ I

Alias of TwoSidedIdeal.mem_matrix.

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

@[deprecated TwoSidedIdeal.matrix_monotone (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix_monotone.

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

@[deprecated TwoSidedIdeal.matrix_strictMono_of_nonempty (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix_strictMono_of_nonempty.

@[simp]

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

@[deprecated TwoSidedIdeal.matrix_bot (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix_bot.

@[simp]

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

@[deprecated TwoSidedIdeal.matrix_top (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix_top.

def TwoSidedIdeal.equivMatrix {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.equivMatrix_apply {R : Type u_1} {n : Type u_2} [NonAssocRing R] [Fintype n] [Nonempty n] [DecidableEq n] (I : TwoSidedIdeal R) : equivMatrix I = matrix n I

@[simp]

theorem TwoSidedIdeal.equivMatrix_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)) : (equivMatrix.symm J).ringCon = J.ringCon.ofMatrix

@[deprecated TwoSidedIdeal.equivMatrix (since := "2025-07-28")]

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)

Alias of TwoSidedIdeal.equivMatrix.

---

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

• @TwoSidedIdeal.equivMatricesOver = @TwoSidedIdeal.equivMatrix

theorem TwoSidedIdeal.coe_equivMatrix_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) : ↑(equivMatrix.symm I) = {x : R | ∃ N ∈ I, N i j = x}

@[deprecated TwoSidedIdeal.coe_equivMatrix_symm_apply (since := "2025-07-28")]

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) : ↑(equivMatrix.symm I) = {x : R | ∃ N ∈ I, N i j = x}

Alias of TwoSidedIdeal.coe_equivMatrix_symm_apply.

def TwoSidedIdeal.orderIsoMatrix {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 equivMatrix.

Equations

• TwoSidedIdeal.orderIsoMatrix = { toEquiv := TwoSidedIdeal.equivMatrix, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.orderIsoMatrix_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 orderIsoMatrix) J).ringCon.toSetoid x y = ∀ (i j : n), J.ringCon (Matrix.single i j x) (Matrix.single i j y)

@[simp]

theorem TwoSidedIdeal.orderIsoMatrix_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) : (orderIsoMatrix I).ringCon.toSetoid M N = ∀ (i j : n), I.ringCon (M i j) (N i j)

@[deprecated TwoSidedIdeal.orderIsoMatrix (since := "2025-07-28")]

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)

Alias of TwoSidedIdeal.orderIsoMatrix.

---

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

Equations

• @TwoSidedIdeal.orderIsoMatricesOver = @TwoSidedIdeal.orderIsoMatrix

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

@[deprecated TwoSidedIdeal.asIdeal_matrix (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.asIdeal_matrix.

Jacobson radicals of two-sided ideals in a matrix ring

@[deprecated _private.Mathlib.LinearAlgebra.Matrix.Ideal.0.TwoSidedIdeal.jacobson_matrix_le (since := "2025-07-28")]

theorem TwoSidedIdeal.jacobson_matricesOver_le {R : Type u_1} [Ring R] {n : Type u_2} [Fintype n] [DecidableEq n] (I : TwoSidedIdeal R) : (matrix n I).jacobson ≤ matrix n I.jacobson

Alias of _private.Mathlib.LinearAlgebra.Matrix.Ideal.0.TwoSidedIdeal.jacobson_matrix_le.

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

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

@[deprecated TwoSidedIdeal.jacobson_matrix (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.jacobson_matrix.

---

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

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

@[deprecated TwoSidedIdeal.matrix_jacobson_bot (since := "2025-07-28")]

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

Alias of TwoSidedIdeal.matrix_jacobson_bot.