The category of R-modules has finite biproducts

instance ModuleCat.instHasBinaryBiproducts {R : Type u} [Ring R] : CategoryTheory.Limits.HasBinaryBiproducts (ModuleCat R)

instance ModuleCat.instHasFiniteBiproducts {R : Type u} [Ring R] : CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R)

def ModuleCat.binaryProductLimitCone {R : Type u} [Ring R] (M N : ModuleCat R) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair 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.

@[simp]

theorem ModuleCat.binaryProductLimitCone_isLimit_lift {R : Type u} [Ring R] (M N : ModuleCat R) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)) : (M.binaryProductLimitCone N).isLimit.lift s = ModuleCat.ofHom ((s.π.app { as := CategoryTheory.Limits.WalkingPair.left }).hom.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.right }).hom)

@[simp]

theorem ModuleCat.binaryProductLimitCone_cone_pt {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (↑M × ↑N)

@[simp]

theorem ModuleCat.binaryProductLimitCone_cone_π_app_left {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)

@[simp]

theorem ModuleCat.binaryProductLimitCone_cone_π_app_right {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)

noncomputable def ModuleCat.biprodIsoProd {R : Type u} [Ring R] (M N : ModuleCat R) : 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 = (CategoryTheory.Limits.BinaryBiproduct.isLimit M N).conePointUniqueUpToIso (M.binaryProductLimitCone N).isLimit

@[simp]

theorem ModuleCat.biprodIsoProd_inv_comp_fst {R : Type u} [Ring R] (M N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.fst = ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)

theorem ModuleCat.biprodIsoProd_inv_comp_fst_apply {R : Type u} [Ring R] (M N : ModuleCat R) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R (↑M × ↑N))) : CategoryTheory.Limits.biprod.fst ((M.biprodIsoProd N).inv x) = (ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)) x

@[simp]

theorem ModuleCat.biprodIsoProd_inv_comp_snd {R : Type u} [Ring R] (M N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.snd = ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)

theorem ModuleCat.biprodIsoProd_inv_comp_snd_apply {R : Type u} [Ring R] (M N : ModuleCat R) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R (↑M × ↑N))) : CategoryTheory.Limits.biprod.snd ((M.biprodIsoProd N).inv x) = (ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)) x

def ModuleCat.HasLimit.lift {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) : 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

• ModuleCat.HasLimit.lift f s = ModuleCat.ofHom { toFun := fun (x : ↑s.1) (j : J) => (s.π.app { as := j }).hom x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModuleCat.HasLimit.lift_hom_apply {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J) : (ModuleCat.HasLimit.lift f s).hom x j = (s.π.app { as := j }).hom x

def ModuleCat.HasLimit.productLimitCone {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)

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.

@[simp]

theorem ModuleCat.HasLimit.productLimitCone_cone_pt_isModule {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : (ModuleCat.HasLimit.productLimitCone f).cone.pt.isModule = Pi.module J (fun (j : J) => ↑(f j)) R

@[simp]

theorem ModuleCat.HasLimit.productLimitCone_isLimit_lift {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) (s : CategoryTheory.Limits.Fan f) : (ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s

@[simp]

theorem ModuleCat.HasLimit.productLimitCone_cone_pt_isAddCommGroup {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : (ModuleCat.HasLimit.productLimitCone f).cone.pt.isAddCommGroup = Pi.addCommGroup

@[simp]

theorem ModuleCat.HasLimit.productLimitCone_cone_π {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : (ModuleCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun (j : CategoryTheory.Discrete J) => ModuleCat.ofHom (LinearMap.proj j.as)

@[simp]

theorem ModuleCat.HasLimit.productLimitCone_cone_pt_carrier {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : ↑(ModuleCat.HasLimit.productLimitCone f).cone.pt = ((j : J) → ↑(f j))

noncomputable def ModuleCat.biproductIsoPi {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) : ⨁ 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

• ModuleCat.biproductIsoPi f = (CategoryTheory.Limits.biproduct.isLimit f).conePointUniqueUpToIso (ModuleCat.HasLimit.productLimitCone f).isLimit

@[simp]

theorem ModuleCat.biproductIsoPi_inv_comp_π {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) (j : J) : CategoryTheory.CategoryStruct.comp (ModuleCat.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) = ModuleCat.ofHom (LinearMap.proj j)

theorem ModuleCat.biproductIsoPi_inv_comp_π_apply {R : Type u} [Ring R] {J : Type} [Finite J] (f : J → ModuleCat R) (j : J) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R ((j : J) → ↑(f j)))) : (CategoryTheory.Limits.biproduct.π f j) ((ModuleCat.biproductIsoPi f).inv x) = (ModuleCat.ofHom (LinearMap.proj j)) x

noncomputable def lequivProdOfRightSplitExact {R : Type u} {A M B : Type v} [Ring R] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup M] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : Function.Injective ⇑j) (exac : LinearMap.range j = LinearMap.ker g) (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.

noncomputable def lequivProdOfLeftSplitExact {R : Type u} {A M B : Type v} [Ring R] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup M] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : M →ₗ[R] A} (hg : Function.Surjective ⇑g) (exac : LinearMap.range j = LinearMap.ker g) (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.