The category of abelian groups has finite biproducts
@[instance]
Equations
- G.has_binary_product H = {cone := {X := AddCommGroup.of (↥G × ↥H) prod.add_comm_group, π := {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j (add_monoid_hom.fst ↥G ↥H) (add_monoid_hom.snd ↥G ↥H), naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair G H)), add_monoid_hom.prod (s.π.app category_theory.limits.walking_pair.left) (s.π.app category_theory.limits.walking_pair.right), fac' := _, uniq' := _}}
def
AddCommGroup.has_limit.lift
{J : Type u}
(F : category_theory.discrete J ⥤ AddCommGroup)
(s : category_theory.limits.cone F) :
s.X ⟶ AddCommGroup.of (Π (j : category_theory.discrete J), ↥(F.obj j))
The map from an arbitrary cone over a indexed family of abelian groups to the cartesian product of those groups.
@[simp]
theorem
AddCommGroup.has_limit.lift_apply
{J : Type u}
(F : category_theory.discrete J ⥤ AddCommGroup)
(s : category_theory.limits.cone F)
(x : ↥(s.X))
(j : J) :
@[instance]
def
AddCommGroup.has_limit.has_limit_discrete
{J : Type u}
(F : category_theory.discrete J ⥤ AddCommGroup) :
Equations
- AddCommGroup.has_limit.has_limit_discrete F = {cone := {X := AddCommGroup.of (Π (j : category_theory.discrete J), ↥(F.obj j)) pi.add_comm_group, π := category_theory.discrete.nat_trans (λ (j : category_theory.discrete J), add_monoid_hom.apply (λ (j : category_theory.discrete J), ↥(F.obj j)) j)}, is_limit := {lift := AddCommGroup.has_limit.lift F, fac' := _, uniq' := _}}
@[instance]
def
AddCommGroup.category_theory.limits.has_biproduct
{J : Type u}
[decidable_eq J]
[fintype J]
(f : J → AddCommGroup) :
@[instance]
Equations
- AddCommGroup.category_theory.limits.has_finite_biproducts = {has_biproducts_of_shape := λ (J : Type u_1) (_x : decidable_eq J) (_x_1 : fintype J), {has_biproduct := λ (f : J → AddCommGroup), infer_instance}}