English
For a pullback cone c, there is an equivalence between IsLimit of the mapped cone and IsLimit of the constructed mapped PullbackCone, i.e., IsLimit (mapCone G (PullbackCone f g)) ≃ IsLimit (PullbackCone.mk (G.map f) (G.map g) (proof)).
Русский
Для конуса притяжения c существует эквивалентность между IsLimit отображённого конуса и IsLimit построенного отображённого PullbackCone; т.е. IsLimit (mapCone G (PullbackCone f g)) ≃ IsLimit (PullbackCone.mk (G.map f) (G.map g) (доказательство)).
LaTeX
$$$IsLimit(mapCone\\ G\\ (PullbackCone\\ f\\ g)) \\simeq IsLimit(PullbackCone.mk(G.map f)(G.map g)\\alpha)$$$
Lean4
/-- The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a
limit. This essentially lets us commute `PullbackCone.mk` with `Functor.mapCone`. -/
def isLimitMapConePullbackConeEquiv :
IsLimit (mapCone G (PullbackCone.mk h k comm)) ≃
IsLimit
(PullbackCone.mk (G.map h) (G.map k) (by simp only [← G.map_comp, comm]) : PullbackCone (G.map f) (G.map g)) :=
(PullbackCone.mk _ _ comm).isLimitMapConeEquiv G
