coeq

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCardinalFiltered.coeq

Lean4

/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, this is an object of `J` where these morphisms
shall be equalized. -/
noncomputable def coeq : J :=
  (cocone (parallelFamily f) (hasCardinalLT_arrow_walkingParallelFamily hK hκ.out.aleph0_le)).pt

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

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

Разделы

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

Аффилиация

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