unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If a `BinaryFan` in the opposite category is a limit, then its `unop` is a colimit. -/
protected def unop {c : BinaryFan (op X) (op Y)} (hc : IsLimit c) : IsColimit c.unop :=
  BinaryCofan.isColimitMk (fun s ↦ (hc.lift 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 (BinaryFan.IsLimit.hom_ext hc (by simp [← h₁]) (by simp [← h₂])))

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