colimit_eq_iff_aux

Mathlib.CategoryTheory.Limits.Types.Filtered

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux

Lean4

theorem colimit_eq_iff_aux [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
    (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔ FilteredColimit.Rel.{v, u} F ⟨i, xi⟩ ⟨j, xj⟩ :=
  by
  dsimp
  rw [← (equivShrink _).symm.injective.eq_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply,
    Functor.ιColimitType_eq_iff, FilteredColimit.rel_eq_eqvGen_colimitTypeRel]

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

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

Разделы

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

Аффилиация

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