# mathlibdocumentation

algebra.category.Module.biproducts

# The category of R-modules has finite biproducts #

@[protected, instance]
@[protected, instance]
@[simp]
theorem Module.binary_product_limit_cone_cone_X {R : Type u} [ring R] (M N : Module R) :
.X = (M × N)
@[simp]
theorem Module.binary_product_limit_cone_is_limit_lift {R : Type u} [ring R] (M N : Module R)  :
def Module.binary_product_limit_cone {R : Type u} [ring R] (M N : Module R) :

Construct limit data for a binary product in Module R, using Module.of R (M × N).

Equations
@[simp]
theorem Module.binary_product_limit_cone_cone_π_app_left {R : Type u} [ring R] (M N : Module R) :
@[simp]
theorem Module.binary_product_limit_cone_cone_π_app_right {R : Type u} [ring R] (M N : Module R) :
noncomputable def Module.biprod_iso_prod {R : Type u} [ring R] (M N : Module R) :
M N (M × N)

We verify that the biproduct in Module R is isomorphic to the cartesian product of the underlying types:

Equations
@[simp]
theorem Module.biprod_iso_prod_hom_apply {R : Type u} [ring R] (M N : Module R) (i : ) :
@[simp]
theorem Module.biprod_iso_prod_inv_comp_fst {R : Type u} [ring R] (M N : Module R) :
@[simp]
theorem Module.biprod_iso_prod_inv_comp_fst_apply {R : Type u} [ring R] (M N : Module R) (x : (M × N))) :
= M N) x
@[simp]
theorem Module.biprod_iso_prod_inv_comp_snd {R : Type u} [ring R] (M N : Module R) :
@[simp]
theorem Module.biprod_iso_prod_inv_comp_snd_apply {R : Type u} [ring R] (M N : Module R) (x : (M × N))) :
= M N) x
def Module.has_limit.lift {R : Type u} [ring R] {J : Type w} (f : J → )  :
s.X (Π (j : J), (f j))

The map from an arbitrary cone over a indexed family of abelian groups to the cartesian product of those groups.

Equations
@[simp]
theorem Module.has_limit.lift_apply {R : Type u} [ring R] {J : Type w} (f : J → ) (x : (s.X)) (j : J) :
x j = (s.π.app {as := j}) x
@[simp]
theorem Module.has_limit.product_limit_cone_is_limit_lift {R : Type u} [ring R] {J : Type w} (f : J → )  :
@[simp]
theorem Module.has_limit.product_limit_cone_cone_π {R : Type u} [ring R] {J : Type w} (f : J → ) :
def Module.has_limit.product_limit_cone {R : Type u} [ring R] {J : Type w} (f : J → ) :

Construct limit data for a product in Module R, using Module.of R (Π j, F.obj j).

Equations
@[simp]
theorem Module.has_limit.product_limit_cone_cone_X {R : Type u} [ring R] {J : Type w} (f : J → ) :
= (Π (j : J), (f j))
@[simp]
theorem Module.biproduct_iso_pi_hom_apply {R : Type u} [ring R] {J : Type} [fintype J] (f : J → ) (x : ) (j : J) :
.hom) x j =
noncomputable def Module.biproduct_iso_pi {R : Type u} [ring R] {J : Type} [fintype J] (f : J → ) :
f (Π (j : J), (f j))

We verify that the biproduct we've just defined is isomorphic to the Module R structure on the dependent function type

Equations
@[simp]
theorem Module.biproduct_iso_pi_inv_comp_π_apply {R : Type u} [ring R] {J : Type} [fintype J] (f : J → ) (j : J) (x : (Π (j : J), (f j)))) :
(.inv) x) = x
@[simp]
theorem Module.biproduct_iso_pi_inv_comp_π {R : Type u} [ring R] {J : Type} [fintype J] (f : J → ) (j : J) :
noncomputable def lequiv_prod_of_right_split_exact {R : Type u} {A M B : Type v} [ring R] [ A] [ B] [ M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : function.injective j) (exac : = ) (h : g.comp f = linear_map.id) :
(A × B) ≃ₗ[R] M

The isomorphism A × B ≃ₗ[R] M coming from a right split exact sequence 0 ⟶ A ⟶ M ⟶ B ⟶ 0 of modules.

Equations
noncomputable def lequiv_prod_of_left_split_exact {R : Type u} {A M B : Type v} [ring R] [ A] [ B] [ M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : M →ₗ[R] A} (hg : function.surjective g) (exac : = ) (h : f.comp j = linear_map.id) :
(A × B) ≃ₗ[R] M

The isomorphism A × B ≃ₗ[R] M coming from a left split exact sequence 0 ⟶ A ⟶ M ⟶ B ⟶ 0 of modules.

Equations