coeqHom

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

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

Lean4

/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, and `k : K`, this is a choice of morphism `j' ⟶ coeq f hK`. -/
noncomputable def coeqHom : j' ⟶ coeq f hK :=
  (cocone (parallelFamily f) (hasCardinalLT_arrow_walkingParallelFamily hK hκ.out.aleph0_le)).ι.app .one

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

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

Разделы

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

Аффилиация

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