piIsoPi — Mathlib

English

Definition of the canonical isomorphism between the categorical product and the direct product inside ModuleCat.

Русский

Определение канонического изоморфизма между категориальным произведением и прямым произведением внутри ModuleCat.

LaTeX

$$$ \text{Definition: } \text{piIsoPi : } ∏^{\mathfrak{c}} Z \cong ModuleCat.of R (∀ i, Z_i) $$$

Lean4

/-- The categorical product of a family of objects in `ModuleCat`
agrees with the usual module-theoretical product.
-/
noncomputable def piIsoPi : ∏ᶜ Z ≅ ModuleCat.of R (∀ i, Z i) :=
  limit.isoLimitCone
    ⟨_, productConeIsLimit Z⟩
      -- We now show this isomorphism commutes with the inclusion of the kernel into the source.

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