hasPushouts_of_hasWidePushouts — Mathlib

English

Having wide pushouts in a category implies having ordinary binary pushouts; the construction shrinks to binary case.

Русский

Наличие широких пушпойнтов в категории означает существование двоичных пушпойнтов; конструкция сводится к двоичному случаю.

LaTeX

$$$\text{HasWidePushouts } D \implies \text{HasPushouts } D.$$$

Lean4

/-- Having wide pushout at any universe level implies having binary pushouts. -/
instance (priority := 100) hasPushouts_of_hasWidePushouts (D : Type u) [Category.{v} D] [HasWidePushouts.{w} D] :
    HasPushouts.{v, u} D :=
  hasWidePushouts_shrink WalkingPair

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