instFaithfulNonemptyFinLinOrdSkeletalFunctor

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor

English

The skeletal functor is faithful: it reflects distinct morphisms, i.e., maps f ≠ g to different morphisms.

Русский

SkeletalFunctor корректен (faithful): различные морфизмы отображаются различными образами.

LaTeX

$$$\\text{The skeletalFunctor is faithful}$$$

Lean4

instance : skeletalFunctor.Faithful where
  map_injective {_ _ f g}
    h := by
    ext : 3
    exact CategoryTheory.congr_fun h _

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

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

Разделы

Аффилиация

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