of_map — Mathlib

English

If sq.map F is a pushout and F reflects colimits for the span, then sq is a pushout.

Русский

Если sq.map F является pushout, и F отражает колимиты для соответствующего span, то sq — pushout.

LaTeX

$$$[\\text{ReflectsColimit}(\\operatorname{span} sq.f_{12} sq.f_{13}, F)] \\Rightarrow ( (sq.map F).IsPushout ) \\Rightarrow ( sq.IsPushout ).$$$

Lean4

theorem of_map (F : C ⥤ D) [ReflectsColimit (span sq.f₁₂ sq.f₁₃) F] (h : (sq.map F).IsPushout) : sq.IsPushout :=
  CategoryTheory.IsPushout.of_map F sq.fac h

Похожие утверждения