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.equivMatricesOverandTwoSidedIdeal.orderIsoMatricesOverestablish 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)
:
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' := ⋯ }
Instances For
@[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]
:
theorem
Ideal.matricesOver_strictMono_of_nonempty
{R : Type u_1}
[Semiring R]
(n : Type u_2)
[Fintype n]
[DecidableEq n]
[Nonempty n]
:
@[simp]
theorem
Ideal.matricesOver_bot
{R : Type u_1}
[Semiring R]
(n : Type u_2)
[Fintype n]
[DecidableEq n]
:
@[simp]
theorem
Ideal.matricesOver_top
{R : Type u_1}
[Semiring R]
(n : Type u_2)
[Fintype n]
[DecidableEq 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} ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
@[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
@[simp]
@[simp]
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)
@[simp]
theorem
TwoSidedIdeal.equivMatricesOver_apply
{R : Type u_1}
[Ring R]
{n : Type u_3}
[Fintype n]
[DecidableEq n]
(i : n)
(j : n)
(I : TwoSidedIdeal R)
:
@[simp]
theorem
TwoSidedIdeal.equivMatricesOver_symm_apply
{R : Type u_1}
[Ring R]
{n : Type u_3}
[Fintype n]
[DecidableEq 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.equivMatricesOver
{R : Type u_1}
[Ring R]
{n : Type u_3}
[Fintype n]
[DecidableEq 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.
Instances For
@[simp]
theorem
TwoSidedIdeal.orderIsoMatricesOver_symm_apply_ringCon_r
{R : Type u_1}
[Ring R]
{n : Type u_3}
[Fintype n]
[DecidableEq 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]
[DecidableEq 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
def
TwoSidedIdeal.orderIsoMatricesOver
{R : Type u_1}
[Ring R]
{n : Type u_3}
[Fintype n]
[DecidableEq 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' := ⋯ }