toCoeq

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

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

Lean4

/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, this is a morphism `j ⟶ coeq f hK` which is equal
to all compositions `f k ≫ coeqHom f hK` for `k : K`. -/
noncomputable def toCoeq : j ⟶ coeq f hK :=
  (cocone (parallelFamily f) (hasCardinalLT_arrow_walkingParallelFamily hK hκ.out.aleph0_le)).ι.app .zero

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

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

Разделы

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

Аффилиация

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