-
Notifications
You must be signed in to change notification settings - Fork 298
/
biproducts.lean
155 lines (129 loc) · 4.82 KB
/
biproducts.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import algebra.category.Group.basic
import algebra.category.Group.preadditive
import category_theory.limits.shapes.biproducts
import algebra.pi_instances
/-!
# The category of abelian groups has finite biproducts
-/
open category_theory
open category_theory.limits
open_locale big_operators
universe u
namespace AddCommGroup
instance has_limit_pair (G H : AddCommGroup.{u}) : has_limit.{u} (pair G H) :=
{ cone :=
{ X := AddCommGroup.of (G × H),
π := { app := λ j, walking_pair.cases_on j (add_monoid_hom.fst G H) (add_monoid_hom.snd G H) }},
is_limit :=
{ lift := λ s, add_monoid_hom.prod (s.π.app walking_pair.left) (s.π.app walking_pair.right),
fac' := begin rintros s (⟨⟩|⟨⟩); { ext x, dsimp, simp, }, end,
uniq' := λ s m w,
begin
ext; [rw ← w walking_pair.left, rw ← w walking_pair.right]; refl,
end, } }
instance (G H : AddCommGroup.{u}) : has_preadditive_binary_biproduct.{u} G H :=
has_preadditive_binary_biproduct.of_has_limit_pair _ _
-- We verify that the underlying type of the biproduct we've just defined is definitionally
-- the cartesian product of the underlying types:
example (G H : AddCommGroup.{u}) : ((G ⊞ H : AddCommGroup.{u}) : Type u) = (G × H) := rfl
-- Furthermore, our biproduct will automatically function as a coproduct.
example (G H : AddCommGroup.{u}) : has_colimit.{u} (pair G H) := by apply_instance
variables {J : Type u} (F : (discrete J) ⥤ AddCommGroup.{u})
namespace has_limit
/--
The map from an arbitrary cone over a indexed family of abelian groups
to the cartesian product of those groups.
-/
def lift (s : cone F) :
s.X ⟶ AddCommGroup.of (Π j, F.obj j) :=
{ to_fun := λ x j, s.π.app j x,
map_zero' := by { ext, simp },
map_add' := λ x y, by { ext, simp }, }
@[simp] lemma lift_apply (s : cone F) (x : s.X) (j : J) : (lift F s) x j = s.π.app j x := rfl
instance has_limit_discrete : has_limit F :=
{ cone :=
{ X := AddCommGroup.of (Π j, F.obj j),
π := discrete.nat_trans (λ j, add_monoid_hom.apply (λ j, F.obj j) j), },
is_limit :=
{ lift := lift F,
fac' := λ s j, by { ext, dsimp, simp, },
uniq' := λ s m w,
begin
ext x j,
dsimp only [has_limit.lift],
simp only [add_monoid_hom.coe_mk],
exact congr_arg (λ f : s.X ⟶ F.obj j, (f : s.X → F.obj j) x) (w j),
end, }, }
end has_limit
namespace has_colimit
variables [fintype J]
/--
The map from the cartesian product of a finite family of abelian groups
to any cocone over that family.
-/
def desc (s : cocone F) :
AddCommGroup.of (Π j, F.obj j) ⟶ s.X :=
{ to_fun := λ f, ∑ j, s.ι.app j (f j),
map_zero' :=
begin
conv_lhs { apply_congr, skip, simp [@pi.zero_apply _ (λ j, F.obj j) x _], },
simp,
end,
map_add' := λ x y,
begin
conv_lhs { apply_congr, skip, simp [pi.add_apply x y _], },
simp [finset.sum_add_distrib],
end, }
@[simp] lemma desc_apply (s : cocone F) (f : Π j, F.obj j) :
(desc F s) f = ∑ j, s.ι.app j (f j) := rfl
variables [decidable_eq J]
instance has_colimit_discrete : has_colimit F :=
{ cocone :=
{ X := AddCommGroup.of (Π j, F.obj j),
ι := discrete.nat_trans (λ j, add_monoid_hom.single (λ j, F.obj j) j), },
is_colimit :=
{ desc := desc F,
fac' := λ s j,
begin
dsimp, ext,
dsimp [add_monoid_hom.single],
simp only [pi.single, add_monoid_hom.coe_mk, desc_apply, coe_comp],
rw finset.sum_eq_single j,
{ simp, },
{ intros b _ h, simp only [dif_neg h, add_monoid_hom.map_zero], },
{ simp, },
end,
uniq' := λ s m w,
begin
dsimp at *,
convert @add_monoid_hom.functions_ext
(discrete J) _ (λ j, F.obj j) _ _ s.X _ m (eq_to_hom rfl ≫ desc F s) _,
intros j x,
dsimp [desc],
simp,
rw finset.sum_eq_single j,
{ -- FIXME what prevents either of these `erw`s working by `simp`?
erw [pi.single_eq_same], rw ←w, simp,
erw add_monoid_hom.single_apply, },
{ intros j' _ h, simp only [pi.single_eq_of_ne h, add_monoid_hom.map_zero], },
{ intros h, exfalso, simpa using h, },
end, }, }.
end has_colimit
open has_limit has_colimit
variables [decidable_eq J] [fintype J]
instance : has_bilimit F :=
{ bicone :=
{ X := AddCommGroup.of (Π j, F.obj j),
ι := discrete.nat_trans (λ j, add_monoid_hom.single (λ j, F.obj j) j),
π := discrete.nat_trans (λ j, add_monoid_hom.apply (λ j, F.obj j) j), },
is_limit := limit.is_limit F,
is_colimit := colimit.is_colimit F, }.
-- We verify that the underlying type of the biproduct we've just defined is definitionally
-- the dependent function type:
example (f : J → AddCommGroup.{u}) : ((⨁ f : AddCommGroup.{u}) : Type u) = (Π j, f j) := rfl
end AddCommGroup