ιObj_πObj

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.ιObj_πObj

English

The composition ιObj I κ f followed by πObj I κ f equals the identity on f.

Русский

Составление ιObj I κ f затем πObj I κ f равно тождественному морфизмy на f.

LaTeX

$$$\\iota_{\\mathrm{Obj}}(f) ; \\pi_{\\mathrm{Obj}}(f) = \\mathrm{id}_f$$$

Lean4

@[reassoc (attr := simp)]
theorem ιObj_πObj : ιObj I κ f ≫ πObj I κ f = f := by simp [ιObj, πObj]

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

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

Разделы

Аффилиация

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