instFiniteCarrierPiObjModuleCatOfFinite

English

If J is finite and Z: J → ModuleCat(k) with each Z(j) finite, then the product piObj has finite carrier.

Русский

Пусть J конечна, Z: J → ModuleCat(k) и каждый Z(j) конечно по Carrier; тогда произведение имеет конечный носитель.

LaTeX

$$$\forall {k} [Ring k] [Finite J] (Z: J \to ModuleCat(k))\; [\forall j, Module.Finite(k, (Z j).carrier)]\; \operatorname{Module.Finite}_k\left(\operatorname{CategoryTheory.Limits.piObj( Z )}.carrier\right)$$$

Lean4

instance {J : Type} [Finite J] (Z : J → ModuleCat.{v} k) [∀ j, Module.Finite k (Z j)] :
    Module.Finite k (∏ᶜ fun j => Z j : ModuleCat.{v} k) :=
  haveI : Module.Finite k (ModuleCat.of k (∀ j, Z j)) := by unfold ModuleCat.of; infer_instance
  (Module.Finite.equiv_iff (ModuleCat.piIsoPi Z).toLinearEquiv).mpr inferInstance

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