mapSkeleton_injective

Mathlib.CategoryTheory.Skeletal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.mapSkeleton_injective

← MathLib Explorer

English

If F is full and faithful, then the object-level mapSkeleton.obj is injective.

Русский

Если F полон и верен, тогда отображение объектов Skeleton.obj инъективно.

LaTeX

$$[F.Full] [F.Faithful] ⇒ Injective(F.mapSkeleton.obj)$$

Lean4

theorem mapSkeleton_injective [F.Full] [F.Faithful] : Function.Injective F.mapSkeleton.obj := fun _ _ h ↦
  skeleton_skeletal C ⟨F.mapSkeleton.preimageIso <| eqToIso h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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