p_comm_f

Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

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

← MathLib Explorer

English

In Karoubi(Karoubi C), for morphism f, the composition with P.p.f commutes with f.f.f.

Русский

В Karoubi(Karoubi C) композиция с P.p.f коммутирует с f.f.f для морфизма f.

LaTeX

$$P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f$$

Lean4

@[reassoc]
theorem p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f := by
  simpa only [hom_ext_iff, comp_f] using p_comm f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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