instHasPushoutsType — Mathlib

English

The category of Type u has all pushouts. For f: S → X1 and g: S → X2, the pushout is constructed as the quotient of the disjoint sum X1 ⊕ X2 by identifying f(s) with g(s) for all s ∈ S.

Русский

Категория Type u имеет все пушауты. Пусть f: S → X1 и g: S → X2; пушаут строится как фактор-пространство суммы X1 ⊔ X2, идентифицируя f(s) и g(s) для всех s ∈ S.

LaTeX

$$$\\mathrm{Pushout}(f,g) = (X_1 \\amalg X_2)/\\sim$, где $f(s) \\sim g(s)$ для всех $s \\in S$$$

Lean4

instance : HasPushouts.{u} (Type u) :=
  hasPushouts_of_hasWidePushouts.{u} (Type u)

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