English
If F preserves colimits of spans and preserves limits under span f g, then an IsPushout statement is equivalent after applying F: IsPushout (F.map f) ... ↔ IsPushout f g h i.
Русский
Если F сохраняет колимиты для спанов и сохраняет пределы под Span f g, то условие IsPushout сохраняется после применения F: IsPushout(F.map f,...) ↔ IsPushout f g h i.
LaTeX
$$$ \\operatorname{IsPushout}(F.map f,F.map g,F.map h,F.map i) \\;\\Leftrightarrow\\; \\operatorname{IsPushout}(f,g,h,i) $$$
Lean4
theorem map_isPushout [PreservesColimit (span f g) F] (s : IsPushout f g h i) :
IsPushout (F.map f) (F.map g) (F.map h) (F.map i) :=
by
refine
IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
(IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
(isColimitOfPreserves F s.isColimit))
· rfl
· simp
· simp
