op

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryFan.IsLimit.op

Lean4

/-- If a `BinaryFan` is a limit, then its opposite is a colimit. -/
protected def op {c : BinaryFan X Y} (hc : IsLimit c) : IsColimit c.op :=
  BinaryCofan.isColimitMk (fun s ↦ (hc.lift s.unop).op) (fun _ ↦ Quiver.Hom.unop_inj (by simp))
    (fun _ ↦ Quiver.Hom.unop_inj (by simp))
    (fun s m h₁ h₂ ↦ Quiver.Hom.unop_inj (BinaryFan.IsLimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

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

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

Разделы

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

Аффилиация

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