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