English
Let R be a nonassociative semiring and n a finite type. For any RingCon structure c on the matrix algebra M_n(R), the matrix obtained by applying the matrix-construction to c is exactly c; i.e. matrix n (ofMatrix c) = c.
Русский
Пусть R — неассоциативное полугоследование; пусть n — конечное множество индексов. Для любой структуры RingCon на алгебру матриц M_n(R) матрица, полученная конструированием matrix из c, равна самой c; то есть matrix n (ofMatrix c) = c.
LaTeX
$$$$ \\mathrm{matrix}_n(\\mathrm{ofMatrix}(c)) = c $$$$
Lean4
/-- 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ℤ`. -/
@[simp]
theorem matrix_ofMatrix [DecidableEq n] (c : RingCon (Matrix n n R)) : matrix n (ofMatrix c) = c :=
by
ext x y
classical
constructor
· intro h
rw [matrix_eq_sum_single x, matrix_eq_sum_single y]
refine c.finset_sum _ fun i _ ↦ c.finset_sum _ fun j _ ↦ h i j i j
· intro h i' j' i j
simpa using c.mul (c.mul (c.refl <| single i i' 1) h) (c.refl <| single j' j 1)
