piIsoPi — Mathlib

English

For a family of commutative rings R_i, the categorical product in CommRingCat is canonically isomorphic to the usual product ring formed by the family, i.e., the ring of functions i ↦ R_i with pointwise operations.

Русский

Для семейства коммутативных колец R_i категориальное произведение в CommRingCat канонически изоморфно обычному произведению этой семьи, то есть кольцу функций i ↦ R_i с покоординатными операциями.

LaTeX

$$$\\prod^{\\mathrm{C}}_{i:\\,\\iota} R(i) \\cong CommRingCat.of\\big(\\iota \\to R(i)\\big)$$$

Lean4

/-- The categorical product and the usual product agree
-/
noncomputable def piIsoPi : ∏ᶜ R ≅ CommRingCat.of ((i : ι) → R i) :=
  limit.isoLimitCone ⟨_, piFanIsLimit R⟩

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