map_preimage

Mathlib.CategoryTheory.Functor.FullyFaithful

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

English

For a full functor F and morphism f in the image, F.map (preimage F f) = f.

Русский

Для полного функторa F и морфизма f в образе, F.map (preimage F f) = f.

LaTeX

$$$F.map(\\mathrm{preimage}\\,F\\,f) = f$$$

Lean4

@[simp]
theorem map_preimage (F : C ⥤ D) [Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (preimage F f) = f :=
  (F.map_surjective f).choose_spec

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

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

Разделы

Аффилиация

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