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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

theorem Module.pi_iso_pi_inv_kernel_ι {R : Type u} [ring R] {ι : Type v} (Z : ι → Module R) [category_theory.limits.has_product Z] (i : ι) :

@[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]

theorem Module.pi_iso_pi_hom_ker_subtype {R : Type u} [ring R] {ι : Type v} (Z : ι → Module R) [category_theory.limits.has_product Z] (i : ι) :

@[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) :