app

Mathlib.CategoryTheory.Abelian.Pseudoelements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.app

Lean4

/-- This is just composition of morphisms in `C`. Another way to express this would be
`(Over.map f).obj a`, but our definition has nicer definitional properties. -/
def app {P Q : C} (f : P ⟶ Q) (a : Over P) : Over Q :=
  a.hom ≫ f

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

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

Разделы

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

Аффилиация

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