instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse

Mathlib.CategoryTheory.Preadditive.Mat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse

English

The inverse equivalence is full; every morphism in Mat R is the image of some morphism from Mat_ (SingleObj (R^op)).

Русский

Обратная эквивалентность полно: любой морфизм в Mat R есть изображение некоторого морфизма из Mat_(SingleObj (R^op)).

LaTeX

$$Full II$$

Lean4

instance : (equivalenceSingleObjInverse R).Full where map_surjective f := ⟨fun i j => MulOpposite.op (f i j), rfl⟩

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

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

Разделы

Аффилиация

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