sum_obj_inl

Mathlib.CategoryTheory.Sums.Basic

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

English

A simp lemma: applying homInduction to inl f yields the left-hand constructor.

Русский

Лемма-simp: применение homInduction к inl f даёт левый конструктор.

LaTeX

$$$$ \mathrm{homInduction}_{left} \; ((\mathrm{inl}_ C D).map f) = \mathrm{inl} x y f. $$$$

Lean4

@[simp]
theorem sum_obj_inl (F : A ⥤ B) (G : C ⥤ D) (a : A) : (F.sum G).obj (inl a) = inl (F.obj a) :=
  rfl

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

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

Разделы

Аффилиация

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