hasPushout_of_epi_comp — Mathlib

English

If a colimit cocone s over f,g factors through an epi h with x,y, and hhx, hhy hold, then the pushout cocone built from s.inl,s.inr is also a colimit cocone for x,y.

Русский

Если колимитный кокон s над f,g факторизуется через эпиморфизм h с помощью x,y и выполняются hhx, hhy, то полученный кокон PushoutCocone.mk s.inl s.inr образует колимит для x,y.

LaTeX

$$$\\text{isColimitOfFactors}(f,g,h,x,y,hhx,hhy,s,hs)$$$

Lean4

instance hasPushout_of_epi_comp (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X) [Epi h] [HasPushout f g] :
    HasPushout (h ≫ f) (h ≫ g) :=
  ⟨⟨⟨_, pushoutIsPushoutOfEpiComp f g h⟩⟩⟩

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