# The category of R-modules has finite biproducts #

Equations
• =
Equations
• =
@[simp]
theorem ModuleCat.binaryProductLimitCone_isLimit_lift {R : Type u} [Ring R] (M : ) (N : ) :
(M.binaryProductLimitCone N).isLimit.lift s = LinearMap.prod (s.app ) (s.app )
@[simp]
theorem ModuleCat.binaryProductLimitCone_cone_pt {R : Type u} [Ring R] (M : ) (N : ) :
(M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (M × N)
def ModuleCat.binaryProductLimitCone {R : Type u} [Ring R] (M : ) (N : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ModuleCat.binaryProductLimitCone_cone_π_app_left {R : Type u} [Ring R] (M : ) (N : ) :
(M.binaryProductLimitCone N).cone.app = LinearMap.fst R M N
@[simp]
theorem ModuleCat.binaryProductLimitCone_cone_π_app_right {R : Type u} [Ring R] (M : ) (N : ) :
(M.binaryProductLimitCone N).cone.app = LinearMap.snd R M N
@[simp]
theorem ModuleCat.biprodIsoProd_hom_apply {R : Type u} [Ring R] (M : ) (N : ) (i : .toCone.pt) :
(M.biprodIsoProd N).hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)
noncomputable def ModuleCat.biprodIsoProd {R : Type u} [Ring R] (M : ) (N : ) :
M N ModuleCat.of R (M × N)

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

Equations
• M.biprodIsoProd N = .conePointUniqueUpToIso (M.binaryProductLimitCone N).isLimit
Instances For
theorem ModuleCat.biprodIsoProd_inv_comp_fst_apply {R : Type u} [Ring R] (M : ) (N : ) (x : .obj (ModuleCat.of R (M × N))) :
CategoryTheory.Limits.biprod.fst ((M.biprodIsoProd N).inv x) = (LinearMap.fst R M N) x
@[simp]
theorem ModuleCat.biprodIsoProd_inv_comp_fst {R : Type u} [Ring R] (M : ) (N : ) :
CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.fst = LinearMap.fst R M N
theorem ModuleCat.biprodIsoProd_inv_comp_snd_apply {R : Type u} [Ring R] (M : ) (N : ) (x : .obj (ModuleCat.of R (M × N))) :
CategoryTheory.Limits.biprod.snd ((M.biprodIsoProd N).inv x) = (LinearMap.snd R M N) x
@[simp]
theorem ModuleCat.biprodIsoProd_inv_comp_snd {R : Type u} [Ring R] (M : ) (N : ) :
CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.snd = LinearMap.snd R M N
@[simp]
theorem ModuleCat.HasLimit.lift_apply {R : Type u} [Ring R] {J : Type w} (f : J) (s : ) (x : s.pt) (j : J) :
() x j = (s.app { as := j }) x
def ModuleCat.HasLimit.lift {R : Type u} [Ring R] {J : Type w} (f : J) (s : ) :
s.pt ModuleCat.of R ((j : J) → (f j))

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

Equations
• = { toFun := fun (x : s.pt) (j : J) => (s.app { as := j }) x, map_add' := , map_smul' := }
Instances For
@[simp]
theorem ModuleCat.HasLimit.productLimitCone_cone_π {R : Type u} [Ring R] {J : Type w} (f : J) :
@[simp]
theorem ModuleCat.HasLimit.productLimitCone_cone_pt {R : Type u} [Ring R] {J : Type w} (f : J) :
.cone.pt = ModuleCat.of R ((j : J) → (f j))
@[simp]
theorem ModuleCat.HasLimit.productLimitCone_isLimit_lift {R : Type u} [Ring R] {J : Type w} (f : J) (s : ) :
.isLimit.lift s =
def ModuleCat.HasLimit.productLimitCone {R : Type u} [Ring R] {J : Type w} (f : J) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ModuleCat.biproductIsoPi_hom_apply {R : Type u} [Ring R] {J : Type} [] (f : J) (x : .toCone.pt) (j : J) :
.hom x j =
noncomputable def ModuleCat.biproductIsoPi {R : Type u} [Ring R] {J : Type} [] (f : J) :
f ModuleCat.of R ((j : J) → (f j))

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

Equations
• = .conePointUniqueUpToIso .isLimit
Instances For
theorem ModuleCat.biproductIsoPi_inv_comp_π_apply {R : Type u} [Ring R] {J : Type} [] (f : J) (j : J) (x : .obj (ModuleCat.of R ((j : J) → (f j)))) :
(.inv x) = () x
@[simp]
theorem ModuleCat.biproductIsoPi_inv_comp_π {R : Type u} [Ring R] {J : Type} [] (f : J) (j : J) :
noncomputable def lequivProdOfRightSplitExact {R : Type u} {A : Type v} {M : Type v} {B : Type v} [Ring R] [] [Module R A] [] [Module R B] [] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : ) (exac : ) (h : g ∘ₗ f = LinearMap.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
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def lequivProdOfLeftSplitExact {R : Type u} {A : Type v} {M : Type v} {B : Type v} [Ring R] [] [Module R A] [] [Module R B] [] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : M →ₗ[R] A} (hg : ) (exac : ) (h : f ∘ₗ j = LinearMap.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
• One or more equations did not get rendered due to their size.
Instances For