hasPullback_biprod_fst_biprod_snd

English

The biproduct square X ⊕ Y with projections yields a pullback with the two zero maps to 0.

Русский

Квадрат биопродукта X ⊕ Y с проекциями образует пуллбак с двумя нулевыми стрелами к 0.

LaTeX

$$$ HasPullback (biprod.inl) (biprod.inr) (0 : X ⟶ 0) (0 : Y ⟶ 0) $$$

Lean4

instance hasPullback_biprod_fst_biprod_snd [HasBinaryBiproduct X Y] :
    HasPullback (biprod.inl : X ⟶ _) (biprod.inr : Y ⟶ _) :=
  HasLimit.mk ⟨_, (of_hasBinaryBiproduct X Y).isLimit⟩

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