hom_ext

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

If two Karoubi morphisms have the same underlying map, they are equal.

Русский

Если две гомоморфизмы Каруоби имеют одинаковое базовое отображение, они равны.

LaTeX

$$$f.f = g.f \Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g := by simpa [hom_ext_iff] using h

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

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

Разделы

Аффилиация

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