mathlib documentation


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

def Module.product_cone {R : Type u} [ring R] {ι : Type v} (Z : ι Module R) :

The product cone induced by the concrete product.


The concrete product cone is limiting.

noncomputable def Module.pi_iso_pi {R : Type u} [ring R] {ι : Type v} (Z : ι Module R) [category_theory.limits.has_product Z] :
Z Module.of R (Π (i : ι), (Z i))

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

theorem Module.pi_iso_pi_inv_kernel_ι_apply {R : Type u} [ring R] {ι : Type v} (Z : ι Module R) [category_theory.limits.has_product Z] (i : ι) (x : (Module.of R (Π (i : ι), (Z i)))) :