equivalenceSingleObj — Mathlib

English

There is an explicit equivalence between Mat R and Mat_(SingleObj (R^op)) given by the inverse equivalence and its quasi-inverse constructed above.

Русский

Существует явная эквивалентность между Mat R и Mat_(SingleObj (R^op)) благодаря обратной эквивалентности и её квазиизоморфному образу.

LaTeX

$$$\mathrm{equivalenceSingleObj} : \mathrm{Mat}(R) \simeq \mathrm{Mat}_{\mathrm{SingleObj}(R^{op})}$$$

Lean4

/-- The categorical equivalence between the category of matrices over a ring,
and the category of matrices over that ring considered as a single-object category. -/
def equivalenceSingleObj : Mat R ≌ Mat_ (SingleObj Rᵐᵒᵖ) :=
  (equivalenceSingleObjInverse R).asEquivalence.symm

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