English
If F preserves limits of cospans, then a pullback is preserved under F: IsPullback (F.map f) (F.map g) (F.map h) (F.map i) whenever IsPullback f g h i.
Русский
Если F сохраняет пределы для диаграмм cospan, то предельная конфигурация сохраняется под F: IsPullback(F.map f, F.map g, F.map h, F.map i) при IsPullback(f,g,h,i).
LaTeX
$$$ [\\operatorname{PreservesLimit}(\\mathrm{cospan}(h,i)) F] \\left( \\operatorname{IsPullback}(f,g,h,i) \\rightarrow \\operatorname{IsPullback}(F.map f,F.map g,F.map h,F.map i) \\right) $$$
Lean4
theorem map_isPullback [PreservesLimit (cospan h i) F] (s : IsPullback f g h i) :
IsPullback (F.map f) (F.map g) (F.map h) (F.map i) := by
-- This is made slightly awkward because `C` and `D` have different universes,
-- and so the relevant `WalkingCospan` diagrams live in different universes too!
refine
IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
(IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
(isLimitOfPreserves F s.isLimit))
· rfl
· simp
· simp
