of_hasBinaryProduct — Mathlib

English

If X and Y have a binary product and the category has a zero object and zero morphisms, then the square with X×Y mapping to X via fst and to Y via snd, and the arrows X→0 and Y→0, forms a pullback square for the arrows 0: X→0 and 0: Y→0.

Русский

Пусть в категории существуют бинарный произведение X×Y, нулевой объект и нулевые морфизмы. Тогда квадрат X×Y ⇢ X и X×Y ⇢ Y вместе с нулевыми стрелками X→0 и Y→0 образует пулбаков квадрат для стрелок 0: X→0 и 0: Y→0.

LaTeX

$$$\mathrm{IsPullback}(\mathrm{Limits.prod.fst},\mathrm{Limits.prod.snd},0: X\to 0,0: Y\to 0).$$$

Lean4

theorem of_hasBinaryProduct [HasBinaryProduct X Y] [HasZeroObject C] [HasZeroMorphisms C] :
    IsPullback Limits.prod.fst Limits.prod.snd (0 : X ⟶ 0) (0 : Y ⟶ 0) := by
  convert @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal <;> subsingleton

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