English
There is a natural equivalence between the property that the mapped binary fan is a limit and the property that the mapped pair is a limit; equivalently, the limit-ness is preserved by mapping along the functor.
Русский
Существует естественное эквивалентное соответствие между тем, что отображённый двоичный конус является пределом, и тем, что отображённая пара является пределом; предел сохраняется функтором.
LaTeX
$$$\text{IsLimit}(G.mapCone(\text{BinaryFan.mk } f g)) \;\simeq\; \text{IsLimit}(\text{BinaryFan.mk} (G.map f) (G.map g))$$$
Lean4
/-- The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `BinaryFan.mk` with `Functor.mapCone`.
-/
def isLimitMapConeBinaryFanEquiv :
IsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
(IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm.trans
(IsLimit.equivIsoLimit (Cones.ext (Iso.refl _) (by rintro (_ | _) <;> simp)))
