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.

Equations
Instances For

    The concrete product cone is limiting.

    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For
        theorem ModuleCat.piIsoPi_inv_kernel_ι_apply {R : Type u} [Ring R] {ι : Type v} (Z : ιModuleCatMax R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : (CategoryTheory.forget (ModuleCatMax R)).obj (ModuleCat.of R ((i : ι) → (Z i)))) :