English
Let R_i be a family of rings. There is a canonical ring isomorphism between the categorical product of the rings and the function ring i ↦ R_i, with pointwise operations.
Русский
Пусть R_i — семейство колец. Существует каноническое кольцевое изоморфирование между категориальным произведением колец и кольцом функций i ↦ R_i, с покоординатными операциями.
LaTeX
$$$\\left(\\prod^{\\mathrm{CommRingCat}}_{i} R_i\\right) \\cong_*\\; \\prod_{i} R_i \\quad (\\cong_{\\text{ring}} \\; (i \\mapsto R_i))$$$
Lean4
/-- The categorical product and the usual product agree
-/
noncomputable def _root_.RingEquiv.piEquivPi (R : ι → Type u) [∀ i, CommRing (R i)] :
(∏ᶜ (fun i : ι ↦ CommRingCat.of (R i)) : CommRingCat.{u}) ≃+* ((i : ι) → R i) :=
(piIsoPi (CommRingCat.of <| R ·)).commRingCatIsoToRingEquiv
