of_createsColimit — Mathlib

English

If F creates the colimit of the span f -> S <- g and F.map f, F.map g have a pushout, then f and g form a pushout.

Русский

Если F создает колимит для касательной (span) f → S ← g и имеются pushout для F.map f и F.map g, то f и g образуют pushout.

LaTeX

$$$HasPushout f g$ given $CreatesColimit (span f g) F$ and $HasPushout (F.map f) (F.map g)$$$

Lean4

theorem of_createsColimit (F : C ⥤ D) {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [CreatesColimit (span f g) F]
    [HasPushout (F.map f) (F.map g)] : HasPushout f g :=
  have : HasColimit (span f g ⋙ F) := hasColimit_of_iso (spanCompIso F f g)
  hasColimit_of_created _ F

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