instHasFiniteProducts — Mathlib

English

For a cartesian monoidal category C, C has finite products; in particular for every pair X,Y there exists a product X × Y with projections and a universal property.

Русский

У картинианской моноидальной категории C существуют конечные произведения; для любой пары объектов X,Y существует произведение X × Y с проекциям и универсальным свойством.

LaTeX

$$$\text{HasFiniteProducts}(C)$$$

Lean4

instance (priority := 100) : Limits.HasFiniteProducts C :=
  letI : ∀ (X Y : C), Limits.HasLimit (Limits.pair X Y) := fun _ _ => .mk ⟨_, tensorProductIsBinaryProduct _ _⟩
  letI : Limits.HasBinaryProducts C := Limits.hasBinaryProducts_of_hasLimit_pair _
  letI : Limits.HasTerminal C := Limits.hasTerminal_of_unique (𝟙_ C)
  hasFiniteProducts_of_has_binary_and_terminal

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