equivMatrix

Mathlib.LinearAlgebra.Matrix.Ideal

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.equivMatrix

Lean4

/-- 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\}$.
-/
@[simps]
def equivMatrix [Nonempty n] [DecidableEq n] : TwoSidedIdeal R ≃ TwoSidedIdeal (Matrix n n R)
    where
  toFun I := I.matrix n
  invFun J := { ringCon := J.ringCon.ofMatrix }
  right_inv _ := ringCon_injective <| RingCon.matrix_ofMatrix _
  left_inv _ := ringCon_injective <| RingCon.ofMatrix_matrix _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru