Documentation

Mathlib.Algebra.Category.ModuleCat.Products

The concrete products in the category of modules are products in the categorical sense. #

def ModuleCat.productCone {R : Type u} [Ring R] {ι : Type v} (Z : ιModuleCatMax R) :

The product cone induced by the concrete product.

Instances For

    The concrete product cone is limiting.

    Instances For
      noncomputable def ModuleCat.piIsoPi {R : Type u} [Ring R] {ι : Type v} (Z : ιModuleCatMax R) [CategoryTheory.Limits.HasProduct Z] :
      Z ModuleCat.of R ((i : ι) → ↑(Z i))

      The categorical product of a family of objects in ModuleCat agrees with the usual module-theoretical product.

      Instances For