prod — Mathlib

English

In the product category, two morphisms are equal if and only if their components are equal.

Русский

В произведении категорий две морфизмы равны тогда и только тогда, когда их компоненты равны.

LaTeX

$$$\forall X,Y:\, \text{Hom}_{\mathrm{Prod}}(X,Y),\ f=g \iff f.1=g.1 \land f.2=g.2$$$

Lean4

/-- `prod C D` gives the Cartesian product of two categories. -/
@[simps (notRecursive := []) Hom id_fst id_snd comp_fst comp_snd, stacks 001K]
instance prod : Category.{max v₁ v₂} (C × D)
    where
  Hom X Y := (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)
  id X := ⟨𝟙 X.1, 𝟙 X.2⟩
  comp f g := (f.1 ≫ g.1, f.2 ≫ g.2)

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