biproductIsoPi — Mathlib

English

The biproduct of a family of ModuleCat objects is isomorphic to the module category structure on the dependent function type.

Русский

Бипродукт семейства объектов ModuleCat изоморфен структуре модуля над зависимым типом функций.

LaTeX

$$$\mathrm{biproduct}(f) \cong \mathrm{ModuleCat.of}(R, (\forall j, f_j))$$$

Lean4

/-- We verify that the biproduct we've just defined is isomorphic to the `ModuleCat R` structure
on the dependent function type.
-/
noncomputable def biproductIsoPi [Finite J] (f : J → ModuleCat.{v} R) :
    ((⨁ f) : ModuleCat.{v} R) ≅ ModuleCat.of R (∀ j, f j) :=
  IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit

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