instFaithfulEmbedding

Mathlib.CategoryTheory.Preadditive.Mat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mat_.Embedding.instFaithfulEmbedding

English

The embedding functor (Mat_.embedding C) is faithful; morphisms are detected componentwise.

Русский

Функтор embedded Mat_.embedding C верен; морфизмы детектируются по компонентам.

LaTeX

$$instFaithfulEmbedding$$

Lean4

instance : (embedding C).Faithful where map_injective h := congr_fun (congr_fun h PUnit.unit) PUnit.unit

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

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

Разделы

Аффилиация

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