biprodIsoProd — Mathlib

English

The biproduct of M and N in ModuleCat R is isomorphic to the product module M × N, via an explicit isomorphism constructed from the universal property of biproducts.

Русский

Бипродукт M ⊞ N в ModuleCat R изоморфен произведению M × N над R.

LaTeX

$$$(M \biprod N) \cong_R \mathrm{ModuleCat.of}(R, M \times N)$$$

Lean4

/-- We verify that the biproduct in `ModuleCat R` is isomorphic to
the Cartesian product of the underlying types:
-/
noncomputable def biprodIsoProd (M N : ModuleCat.{v} R) : (M ⊞ N : ModuleCat.{v} R) ≅ ModuleCat.of R (M × N) :=
  IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit M N) (binaryProductLimitCone M N).isLimit

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