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).

Main results

• TwoSidedIdeal.equivMatricesOver and TwoSidedIdeal.orderIsoMatricesOver establish an order isomorphism between two-sided ideals in $R$ and those in $Mₙ(R)$.

Left ideals in a matrix ring

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 ∈ Ideal.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 (Ideal.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 (Ideal.matricesOver n)

@[simp]

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

@[simp]

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

Two-sided ideals in a matrix ring

def TwoSidedIdeal.matricesOver {R : Type u_1} [Ring R] (n : Type u_2) [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 = TwoSidedIdeal.mk' {M : Matrix n n R | ∀ (i j : n), M i j ∈ I} ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

def TwoSidedIdeal.equivMatricesOver {R : Type u_1} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : 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} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : n) (I : TwoSidedIdeal R) : (TwoSidedIdeal.equivMatricesOver i j) I = TwoSidedIdeal.matricesOver n I

@[simp]

theorem TwoSidedIdeal.equivMatricesOver_symm_apply {R : Type u_1} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : n) (J : TwoSidedIdeal (Matrix n n R)) : (TwoSidedIdeal.equivMatricesOver i j).symm J = TwoSidedIdeal.mk' {x : R | ∃ N ∈ J, N i j = x} ⋯ ⋯ ⋯ ⋯ ⋯

def TwoSidedIdeal.orderIsoMatricesOver {R : Type u_1} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : 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 i j = { toEquiv := TwoSidedIdeal.equivMatricesOver i j, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.orderIsoMatricesOver_symm_apply_ringCon_r {R : Type u_1} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : n) (J : TwoSidedIdeal (Matrix n n R)) (x : R) (y : R) : ((RelIso.symm (TwoSidedIdeal.orderIsoMatricesOver i j)) J).ringCon.toSetoid x y = ∃ N ∈ J, N i j = x - y

@[simp]

theorem TwoSidedIdeal.orderIsoMatricesOver_apply_ringCon_r {R : Type u_1} [Ring R] {n : Type u_3} [Fintype n] (i : n) (j : n) (I : TwoSidedIdeal R) (x : Matrix n n R) (y : Matrix n n R) : ((TwoSidedIdeal.orderIsoMatricesOver i j) I).ringCon.toSetoid x y = ∀ (i j : n), x i j - y i j ∈ I