unop — Mathlib

English

If a binary cofan in the opposite category is a colimit, then its unop is a limit.

Русский

Если бинарный кофан в противоположной категории является колимитом, то его обратное является пределом.

LaTeX

$$$$\\text{If } hc: IsColimit(c)\\text{ for } c : BinaryCofan(op X)(op Y),\\ \\text{then } IsLimit(c.unop).$$$$

Lean4

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

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