app_p_comp

Mathlib.CategoryTheory.Idempotents.FunctorCategories

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

English

For any morphism f: P ⟶ Q in Karoubi(Functor J C) and any X, P.p.app X ∘ f.f.app X = f.f.app X.

Русский

Для любого морфизма f: P ⟶ Q в Karoubi(Functor J C) и любого X, P.p.app X ∘ f.f.app X = f.f.app X.

LaTeX

$$P.p.app X \\circ f.f.app X = f.f.app X$$

Lean4

@[reassoc (attr := simp)]
theorem app_p_comp : P.p.app X ≫ f.f.app X = f.f.app X :=
  congr_app (p_comp f) X

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

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

Разделы

Аффилиация

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