English
If equalizer preservation holds, then the inverse of PreservesEqualizer.iso composed with G.map equalizer.ι equals the equalizer.ι of the mapped morphisms.
Русский
Если равнопроизводитель сохраняется, то обратное к PreservesEqualizer.iso, композиция с G.map equalizer.ι равна равнопроизводителю на отображениях, полученных из G.map f и G.map g.
LaTeX
$$$(\\text{PreservesEqualizer.iso } G f g)^{-1} \\circ G(\\text{equalizer.ι } f g) = \\text{equalizer.ι}(G.map f)(G.map g)$$$
Lean4
/-- The map of a fork is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `Fork.ofι` with `Functor.mapCone`.
-/
def isLimitMapConeForkEquiv :
IsLimit (G.mapCone (Fork.ofι h w)) ≃
IsLimit (Fork.ofι (G.map h) (by simp only [← G.map_comp, w]) : Fork (G.map f) (G.map g)) :=
(IsLimit.postcomposeHomEquiv (diagramIsoParallelPair _) _).symm.trans
(IsLimit.equivIsoLimit (Fork.ext (Iso.refl _) (by simp [Fork.ι])))
