π_obj

Mathlib.CategoryTheory.Action

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ActionCategory.π_obj

English

The projection π maps each object to the unique unit object of M, i.e., each object is sent to star of M.

Русский

Проекция π отправляет каждый объект к уникальному элементу-единице M.

LaTeX

$$$\pi: ActionCategory M X \to SingleObj M, \; \pi( p ) = *$$$

Lean4

@[simp]
theorem π_obj (p : ActionCategory M X) : (π M X).obj p = SingleObj.star M :=
  Unit.ext _ _

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

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

Разделы

Аффилиация

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