mathlib3 documentation

algebra.category.Group.biproducts

The category of abelian groups has finite biproducts #

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

source
@[protected, instance]
def AddCommGroup.category_theory.limits.has_binary_biproducts  :
category_theory.limits.has_binary_biproducts AddCommGroup
source
@[protected, instance]
def AddCommGroup.category_theory.limits.has_finite_biproducts  :
category_theory.limits.has_finite_biproducts AddCommGroup
source
@[simp]
theorem AddCommGroup.binary_product_limit_cone_cone_X (G H : AddCommGroup) :
(G.binary_product_limit_cone H).cone.X = AddCommGroup.of (↥G × ↥H)
source
def AddCommGroup.binary_product_limit_cone (G H : AddCommGroup) :
category_theory.limits.limit_cone (category_theory.limits.pair G H)

Construct limit data for a binary product in AddCommGroup, using AddCommGroup.of (G × H).

Equations
source
@[simp]
theorem AddCommGroup.binary_product_limit_cone_is_limit_lift (G H : AddCommGroup) (s : category_theory.limits.cone (category_theory.limits.pair G H)) :
(G.binary_product_limit_cone H).is_limit.lift s = add_monoid_hom.prod (s.π.app {as := category_theory.limits.walking_pair.left}) (s.π.app {as := category_theory.limits.walking_pair.right})
source
@[simp]
theorem AddCommGroup.binary_product_limit_cone_cone_π_app_left (G H : AddCommGroup) :
(G.binary_product_limit_cone H).cone.π.app {as := category_theory.limits.walking_pair.left} = add_monoid_hom.fst ↥G ↥H
source
@[simp]
theorem AddCommGroup.binary_product_limit_cone_cone_π_app_right (G H : AddCommGroup) :
(G.binary_product_limit_cone H).cone.π.app {as := category_theory.limits.walking_pair.right} = add_monoid_hom.snd ↥G ↥H
source
noncomputable def AddCommGroup.biprod_iso_prod (G H : AddCommGroup) :
G ⊞ H ≅ AddCommGroup.of (↥G × ↥H)

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

Equations
source
@[simp]
theorem AddCommGroup.biprod_iso_prod_hom_apply (G H : AddCommGroup) (i : ↥((category_theory.limits.binary_biproduct.bicone G H).to_cone.X)) :
⇑((G.biprod_iso_prod H).hom) i = (⇑category_theory.limits.biprod.fst i, ⇑category_theory.limits.biprod.snd i)
source
@[simp]
theorem AddCommGroup.biprod_iso_prod_inv_comp_fst_apply (G H : AddCommGroup) (x : ↥(AddCommGroup.of (↥G × ↥H))) :
⇑category_theory.limits.biprod.fst (⇑((G.biprod_iso_prod H).inv) x) = ⇑(add_monoid_hom.fst ↥G ↥H) x
source
@[simp]
theorem AddCommGroup.biprod_iso_prod_inv_comp_fst (G H : AddCommGroup) :
(G.biprod_iso_prod H).inv ≫ category_theory.limits.biprod.fst = add_monoid_hom.fst ↥G ↥H
source
@[simp]
theorem AddCommGroup.biprod_iso_prod_inv_comp_snd_apply (G H : AddCommGroup) (x : ↥(AddCommGroup.of (↥G × ↥H))) :
⇑category_theory.limits.biprod.snd (⇑((G.biprod_iso_prod H).inv) x) = ⇑(add_monoid_hom.snd ↥G ↥H) x
source
@[simp]
theorem AddCommGroup.biprod_iso_prod_inv_comp_snd (G H : AddCommGroup) :
(G.biprod_iso_prod H).inv ≫ category_theory.limits.biprod.snd = add_monoid_hom.snd ↥G ↥H
source
@[simp]
theorem AddCommGroup.has_limit.lift_apply {J : Type w} (f : J → AddCommGroup) (s : category_theory.limits.fan f) (x : ↥(s.X)) (j : J) :
⇑(AddCommGroup.has_limit.lift f s) x j = ⇑(s.π.app {as := j}) x
source
def AddCommGroup.has_limit.lift {J : Type w} (f : J → AddCommGroup) (s : category_theory.limits.fan f) :
s.X ⟶ AddCommGroup.of (Π (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
def AddCommGroup.has_limit.product_limit_cone {J : Type w} (f : J → AddCommGroup) :
category_theory.limits.limit_cone (category_theory.discrete.functor f)

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

Equations
source
@[simp]
theorem AddCommGroup.has_limit.product_limit_cone_cone_π {J : Type w} (f : J → AddCommGroup) :
(AddCommGroup.has_limit.product_limit_cone f).cone.π = category_theory.discrete.nat_trans (λ (j : category_theory.discrete J), pi.eval_add_monoid_hom (λ (j : J), ↥(f j)) j.as)
source
@[simp]
theorem AddCommGroup.has_limit.product_limit_cone_cone_X {J : Type w} (f : J → AddCommGroup) :
(AddCommGroup.has_limit.product_limit_cone f).cone.X = AddCommGroup.of (Π (j : J), ↥(f j))
source
@[simp]
theorem AddCommGroup.has_limit.product_limit_cone_is_limit_lift {J : Type w} (f : J → AddCommGroup) (s : category_theory.limits.fan f) :
(AddCommGroup.has_limit.product_limit_cone f).is_limit.lift s = AddCommGroup.has_limit.lift f s
source
@[simp]
theorem AddCommGroup.biproduct_iso_pi_hom_apply {J : Type} [fintype J] (f : J → AddCommGroup) (x : ↥((category_theory.limits.biproduct.bicone f).to_cone.X)) (j : J) :
⇑((AddCommGroup.biproduct_iso_pi f).hom) x j = ⇑(category_theory.limits.biproduct.π f j) x
source
noncomputable def AddCommGroup.biproduct_iso_pi {J : Type} [fintype J] (f : J → AddCommGroup) :
⨁ f ≅ AddCommGroup.of (Π (j : J), ↥(f j))

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

Equations
source
@[simp]
theorem AddCommGroup.biproduct_iso_pi_inv_comp_π_apply {J : Type} [fintype J] (f : J → AddCommGroup) (j : J) (x : ↥(AddCommGroup.of (Π (j : J), ↥(f j)))) :
⇑(category_theory.limits.biproduct.π f j) (⇑((AddCommGroup.biproduct_iso_pi f).inv) x) = ⇑(pi.eval_add_monoid_hom (λ (j : J), ↥(f j)) j) x
source
@[simp]
theorem AddCommGroup.biproduct_iso_pi_inv_comp_π {J : Type} [fintype J] (f : J → AddCommGroup) (j : J) :
(AddCommGroup.biproduct_iso_pi f).inv ≫ category_theory.limits.biproduct.π f j = pi.eval_add_monoid_hom (λ (j : J), ↥(f j)) j