mathlib documentation

algebra.category.Module.products

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.

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

The concrete product cone is limiting.

Equations
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.

Equations
@[simp]
@[simp]
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)))) :
@[simp]
@[simp]
theorem Module.pi_iso_pi_hom_ker_subtype_apply {R : Type u} [ring R] {ι : Type v} (Z : ι → Module R) [category_theory.limits.has_product Z] (i : ι) (x : Z) :