ιFunctorObj_πFunctorObj

Mathlib.CategoryTheory.SmallObject.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj

English

The composite ιFunctorObj f πX ≫ πFunctorObj f πX equals the identity map πX.

Русский

Сложение ιFunctorObj f πX ≫ πFunctorObj f πX даёт тождественный переход πX.

LaTeX

$$$ ιFunctorObj f πX \;\circ\; πFunctorObj f πX = πX $$$

Lean4

@[reassoc (attr := simp)]
theorem ιFunctorObj_πFunctorObj : ιFunctorObj f πX ≫ πFunctorObj f πX = πX := by simp [ιFunctorObj, πFunctorObj]

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

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

Разделы

Аффилиация

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