instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse

English

The inverse equivalence is faithful; i.e., it reflects distinct morphisms in Mat_(SingleObj (R^op)) to distinct morphisms in Mat R.

Русский

Обратная эквивалентность является верной: она отображает различные морфизмы в разные морфизмы в Mat R.

LaTeX

$$$\text{(equivalenceSingleObjInverse R).Faithful}$$$

Lean4

instance : (equivalenceSingleObjInverse R).Faithful where
  map_injective
    w := by
    ext
    apply_fun MulOpposite.unop using MulOpposite.unop_injective
    exact congr_fun (congr_fun w _) _

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