Documentation

Mathlib.Algebra.Category.ModuleCat.Biproducts

The category of R-modules has finite biproducts #

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_cone_pt {R : Type u} [Ring R] (M N : ModuleCat R) :
(M.binaryProductLimitCone N).cone.pt = of R (M × N)
noncomputable def ModuleCat.biprodIsoProd {R : Type u} [Ring R] (M N : ModuleCat R) :
M N of R (M × N)

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

Equations
def ModuleCat.HasLimit.lift {R : Type u} [Ring R] {J : Type w} (f : JModuleCat R) (s : CategoryTheory.Limits.Fan f) :
s.pt 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
@[simp]
theorem ModuleCat.HasLimit.lift_hom_apply {R : Type u} [Ring R] {J : Type w} (f : JModuleCat R) (s : CategoryTheory.Limits.Fan f) (x : s.1) (j : J) :
(Hom.hom (lift f s)) x j = (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x

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 : JModuleCat R) :
(productLimitCone f).cone.pt.isModule = Pi.module J (fun (j : J) => (f j)) R
@[simp]
theorem ModuleCat.HasLimit.productLimitCone_cone_pt_carrier {R : Type u} [Ring R] {J : Type w} (f : JModuleCat R) :
(productLimitCone f).cone.pt = ((j : J) → (f j))
noncomputable def ModuleCat.biproductIsoPi {R : Type u} [Ring R] {J : Type} [Finite J] (f : JModuleCat R) :
f 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
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.