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

The concrete product cone is limiting.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def ModuleCat.piIsoPi {R : Type u} [Ring R] {ι : Type v} (Z : ιModuleCatMax R) [CategoryTheory.Limits.HasProduct Z] :
∏ᶜ Z of R ((i : ι) → (Z i))

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

Equations

The coproduct cone induced by the concrete product.

Equations

The concrete coproduct cone is limiting.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def ModuleCat.coprodIsoDirectSum {R : Type u} [Ring R] {ι : Type v} (Z : ιModuleCatMax R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] :
Z of R (DirectSum ι fun (i : ι) => (Z i))

The categorical coproduct of a family of objects in ModuleCat agrees with direct sum.

Equations