mathlib3 documentation

algebra.category.Module.biproducts

The category of R-modules has finite biproducts #

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

source
@[protected, instance]
def Module.category_theory.limits.has_binary_biproducts {R : Type u} [ring R] :
category_theory.limits.has_binary_biproducts (Module R)
source
@[protected, instance]
def Module.category_theory.limits.has_finite_biproducts {R : Type u} [ring R] :
category_theory.limits.has_finite_biproducts (Module R)
source
@[simp]
theorem Module.binary_product_limit_cone_cone_X {R : Type u} [ring R] (M N : Module R) :
(M.binary_product_limit_cone N).cone.X = Module.of R (↥M × ↥N)
source
@[simp]
theorem Module.binary_product_limit_cone_is_limit_lift {R : Type u} [ring R] (M N : Module R) (s : category_theory.limits.cone (category_theory.limits.pair M N)) :
(M.binary_product_limit_cone N).is_limit.lift s = linear_map.prod (s.π.app {as := category_theory.limits.walking_pair.left}) (s.π.app {as := category_theory.limits.walking_pair.right})
source
def Module.binary_product_limit_cone {R : Type u} [ring R] (M N : Module R) :
category_theory.limits.limit_cone (category_theory.limits.pair M N)

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

Equations
source
@[simp]
theorem Module.binary_product_limit_cone_cone_π_app_left {R : Type u} [ring R] (M N : Module R) :
(M.binary_product_limit_cone N).cone.π.app {as := category_theory.limits.walking_pair.left} = linear_map.fst R ↥M ↥N
source
@[simp]
theorem Module.binary_product_limit_cone_cone_π_app_right {R : Type u} [ring R] (M N : Module R) :
(M.binary_product_limit_cone N).cone.π.app {as := category_theory.limits.walking_pair.right} = linear_map.snd R ↥M ↥N
source
noncomputable def Module.biprod_iso_prod {R : Type u} [ring R] (M N : Module R) :
M ⊞ N ≅ Module.of R (↥M × ↥N)

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

Equations
source
@[simp]
theorem Module.biprod_iso_prod_hom_apply {R : Type u} [ring R] (M N : Module R) (i : ↥((category_theory.limits.binary_biproduct.bicone M N).to_cone.X)) :
⇑((M.biprod_iso_prod N).hom) i = (⇑category_theory.limits.biprod.fst i, ⇑category_theory.limits.biprod.snd i)
source
@[simp]
theorem Module.biprod_iso_prod_inv_comp_fst {R : Type u} [ring R] (M N : Module R) :
(M.biprod_iso_prod N).inv ≫ category_theory.limits.biprod.fst = linear_map.fst R ↥M ↥N
source
@[simp]
theorem Module.biprod_iso_prod_inv_comp_fst_apply {R : Type u} [ring R] (M N : Module R) (x : ↥(Module.of R (↥M × ↥N))) :
⇑category_theory.limits.biprod.fst (⇑((M.biprod_iso_prod N).inv) x) = ⇑(linear_map.fst R ↥M ↥N) x
source
@[simp]
theorem Module.biprod_iso_prod_inv_comp_snd {R : Type u} [ring R] (M N : Module R) :
(M.biprod_iso_prod N).inv ≫ category_theory.limits.biprod.snd = linear_map.snd R ↥M ↥N
source
@[simp]
theorem Module.biprod_iso_prod_inv_comp_snd_apply {R : Type u} [ring R] (M N : Module R) (x : ↥(Module.of R (↥M × ↥N))) :
⇑category_theory.limits.biprod.snd (⇑((M.biprod_iso_prod N).inv) x) = ⇑(linear_map.snd R ↥M ↥N) x
source
def Module.has_limit.lift {R : Type u} [ring R] {J : Type w} (f : J → Module R) (s : category_theory.limits.fan f) :
s.X ⟶ Module.of R (Π (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
source
@[simp]
theorem Module.has_limit.lift_apply {R : Type u} [ring R] {J : Type w} (f : J → Module R) (s : category_theory.limits.fan f) (x : ↥(s.X)) (j : J) :
⇑(Module.has_limit.lift f s) x j = ⇑(s.π.app {as := j}) x
source
@[simp]
theorem Module.has_limit.product_limit_cone_is_limit_lift {R : Type u} [ring R] {J : Type w} (f : J → Module R) (s : category_theory.limits.fan f) :
(Module.has_limit.product_limit_cone f).is_limit.lift s = Module.has_limit.lift f s
source
@[simp]
theorem Module.has_limit.product_limit_cone_cone_π {R : Type u} [ring R] {J : Type w} (f : J → Module R) :
(Module.has_limit.product_limit_cone f).cone.π = category_theory.discrete.nat_trans (λ (j : category_theory.discrete J), linear_map.proj j.as)
source
def Module.has_limit.product_limit_cone {R : Type u} [ring R] {J : Type w} (f : J → Module R) :
category_theory.limits.limit_cone (category_theory.discrete.functor f)

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

Equations
source
@[simp]
theorem Module.has_limit.product_limit_cone_cone_X {R : Type u} [ring R] {J : Type w} (f : J → Module R) :
(Module.has_limit.product_limit_cone f).cone.X = Module.of R (Π (j : J), ↥(f j))
source
@[simp]
theorem Module.biproduct_iso_pi_hom_apply {R : Type u} [ring R] {J : Type} [fintype J] (f : J → Module R) (x : ↥((category_theory.limits.biproduct.bicone f).to_cone.X)) (j : J) :
⇑((Module.biproduct_iso_pi f).hom) x j = ⇑(category_theory.limits.biproduct.π f j) x
source
noncomputable def Module.biproduct_iso_pi {R : Type u} [ring R] {J : Type} [fintype J] (f : J → Module R) :
⨁ f ≅ Module.of R (Π (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
source
@[simp]
theorem Module.biproduct_iso_pi_inv_comp_π_apply {R : Type u} [ring R] {J : Type} [fintype J] (f : J → Module R) (j : J) (x : ↥(Module.of R (Π (j : J), ↥(f j)))) :
⇑(category_theory.limits.biproduct.π f j) (⇑((Module.biproduct_iso_pi f).inv) x) = ⇑(linear_map.proj j) x
source
@[simp]
theorem Module.biproduct_iso_pi_inv_comp_π {R : Type u} [ring R] {J : Type} [fintype J] (f : J → Module R) (j : J) :
(Module.biproduct_iso_pi f).inv ≫ category_theory.limits.biproduct.π f j = linear_map.proj j
source
noncomputable def lequiv_prod_of_right_split_exact {R : Type u} {A M B : Type v} [ring R] [add_comm_group A] [module R A] [add_comm_group B] [module R B] [add_comm_group M] [module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : function.injective ⇑j) (exac : linear_map.range j = linear_map.ker g) (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
source
noncomputable def lequiv_prod_of_left_split_exact {R : Type u} {A M B : Type v} [ring R] [add_comm_group A] [module R A] [add_comm_group B] [module R B] [add_comm_group M] [module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : M →ₗ[R] A} (hg : function.surjective ⇑g) (exac : linear_map.range j = linear_map.ker g) (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