app_idem

Mathlib.CategoryTheory.Idempotents.FunctorCategories

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.app_idem

English

In the functor category Karoubi(C) ⥤ D, for every X, the component P.p.app X is idempotent.

Русский

В категорийной категории Кароуби(C) ⥤ D компонент P.p.app X является идемпотентом для каждого X.

LaTeX

$$(P.p.app X) \\circ (P.p.app X) = P.p.app X$$

Lean4

@[reassoc (attr := simp)]
theorem app_idem : P.p.app X ≫ P.p.app X = P.p.app X :=
  congr_app P.idem X

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

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

Разделы

Аффилиация

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