# mathlibdocumentation

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 : ι → ) :

The product cone induced by the concrete product.

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

The concrete product cone is limiting.

Equations
noncomputable def Module.pi_iso_pi {R : Type u} [ring R] {ι : Type v} (Z : ι → )  :
Z (Π (i : ι), (Z i))

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

Equations
@[simp]
theorem Module.pi_iso_pi_inv_kernel_ι {R : Type u} [ring R] {ι : Type v} (Z : ι → ) (i : ι) :
@[simp]
theorem Module.pi_iso_pi_inv_kernel_ι_apply {R : Type u} [ring R] {ι : Type v} (Z : ι → ) (i : ι) (x : (Π (i : ι), (Z i)))) :
@[simp]
theorem Module.pi_iso_pi_hom_ker_subtype {R : Type u} [ring R] {ι : Type v} (Z : ι → ) (i : ι) :
@[simp]
theorem Module.pi_iso_pi_hom_ker_subtype_apply {R : Type u} [ring R] {ι : Type v} (Z : ι → ) (i : ι) (x : Z) :