propArrow

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.propArrow

Lean4

/-- The class of morphisms in `Arrow C` which on the left side are
pushouts of coproducts of morphisms in `I`, and which are
isomorphisms on the right side. -/
def propArrow : MorphismProperty (Arrow C) := fun _ _ f ↦ (coproducts.{w} I).pushouts f.left ∧ (isomorphisms C) f.right

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

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

Разделы

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

Аффилиация

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