hasPullback_over_zero — Mathlib

English

If X and Y are objects with a binary product, then the pullback of the two zero morphisms 0 → X and 0 → Y exists.

Русский

Если имеются X, Y с бинарным произведением, то существует пуллбэк нулевых морфизмов 0 → X и 0 → Y.

LaTeX

$$$$\text{HasPullback}(0 \to X,\; 0 \to Y).$$$$

Lean4

instance hasPullback_over_zero (X Y : C) [HasBinaryProduct X Y] : HasPullback (0 : X ⟶ 0) (0 : Y ⟶ 0) :=
  HasLimit.mk ⟨_, isPullbackOfIsTerminalIsProduct _ _ _ _ HasZeroObject.zeroIsTerminal (prodIsProd X Y)⟩

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