congr_map

Mathlib.Combinatorics.Quiver.ReflQuiver

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ReflPrefunctor.congr_map

English

If two prefunctors are equal, then their action on morphisms is equal.

Русский

Если два префункторa равны, то их действие на морфизмы совпадает.

LaTeX

$$$\\text{If } e:\\ F=G,\\; F.map f = G.map f$ for all f$$$

Lean4

theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) :
    F.map f = F.map g :=
  congrArg F.map h

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

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

Разделы

Аффилиация

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