mapIso_injective

Mathlib.CategoryTheory.Functor.FullyFaithful

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

← MathLib Explorer

English

If F is faithful, then the map on isomorphisms F.mapIso is injective.

Русский

Если F верный, то отображение изоморфизмов F.mapIso инъективно.

LaTeX

$$$F.mapIso\\;\\text{ is injective}$$$

Lean4

theorem mapIso_injective (F : C ⥤ D) [Faithful F] : Function.Injective <| (F.mapIso : (X ≅ Y) → (F.obj X ≅ F.obj Y)) :=
  fun _ _ h => Iso.ext (map_injective F (congr_arg Iso.hom h :))

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

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

Разделы

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

Аффилиация

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