Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 4e50b68

Browse files
committed
feat(category_theory/abelian): if D is abelian so is C ⥤ D (#13686)
Needed for LTE, and also useful to show `Rep k G` is abelian. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 43e84cd commit 4e50b68

File tree

4 files changed

+139
-2
lines changed

4 files changed

+139
-2
lines changed
Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
/-
2+
Copyright (c) 2022 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 category_theory.abelian.basic
7+
import category_theory.preadditive.functor_category
8+
import category_theory.limits.shapes.functor_category
9+
import category_theory.limits.preserves.shapes.kernels
10+
11+
/-!
12+
# If `D` is abelian, then the functor category `C ⥤ D` is also abelian.
13+
14+
-/
15+
16+
noncomputable theory
17+
18+
namespace category_theory
19+
open category_theory.limits
20+
21+
universes w v u
22+
variables {C : Type (max v u)} [category.{v} C]
23+
variables {D : Type w} [category.{max v u} D] [abelian D]
24+
25+
namespace abelian
26+
27+
namespace functor_category
28+
variables {F G : C ⥤ D} (α : F ⟶ G) (X : C)
29+
30+
/-- The evaluation of the abelian coimage in a functor category is
31+
the abelian coimage of the corresponding component. -/
32+
@[simps]
33+
def coimage_obj_iso : (abelian.coimage α).obj X ≅ abelian.coimage (α.app X) :=
34+
preserves_cokernel.iso ((evaluation C D).obj X) _ ≪≫
35+
cokernel.map_iso _ _ (preserves_kernel.iso ((evaluation C D).obj X) _) (iso.refl _)
36+
begin
37+
dsimp,
38+
simp only [category.comp_id],
39+
exact (kernel_comparison_comp_ι _ ((evaluation C D).obj X)).symm,
40+
end
41+
42+
/-- The evaluation of the abelian image in a functor category is
43+
the abelian image of the corresponding component. -/
44+
@[simps]
45+
def image_obj_iso : (abelian.image α).obj X ≅ abelian.image (α.app X) :=
46+
preserves_kernel.iso ((evaluation C D).obj X) _ ≪≫
47+
kernel.map_iso _ _ (iso.refl _) (preserves_cokernel.iso ((evaluation C D).obj X) _)
48+
begin
49+
apply (cancel_mono (preserves_cokernel.iso ((evaluation C D).obj X) α).inv).1,
50+
simp only [category.assoc, iso.hom_inv_id],
51+
dsimp,
52+
simp only [category.id_comp, category.comp_id],
53+
exact (π_comp_cokernel_comparison _ ((evaluation C D).obj X)).symm,
54+
end
55+
56+
lemma coimage_image_comparison_app :
57+
coimage_image_comparison (α.app X) =
58+
(coimage_obj_iso α X).inv ≫ (coimage_image_comparison α).app X ≫ (image_obj_iso α X).hom :=
59+
begin
60+
ext,
61+
dsimp,
62+
simp only [category.comp_id, category.id_comp, category.assoc,
63+
coimage_image_factorisation, limits.cokernel.π_desc_assoc, limits.kernel.lift_ι],
64+
simp only [←evaluation_obj_map C D X],
65+
erw kernel_comparison_comp_ι _ ((evaluation C D).obj X),
66+
erw π_comp_cokernel_comparison_assoc _ ((evaluation C D).obj X),
67+
simp only [←functor.map_comp],
68+
simp only [coimage_image_factorisation, evaluation_obj_map],
69+
end
70+
71+
lemma coimage_image_comparison_app' :
72+
(coimage_image_comparison α).app X =
73+
(coimage_obj_iso α X).hom ≫ coimage_image_comparison (α.app X) ≫ (image_obj_iso α X).inv :=
74+
by simp only [coimage_image_comparison_app, iso.hom_inv_id_assoc, iso.hom_inv_id, category.assoc,
75+
category.comp_id]
76+
77+
instance functor_category_is_iso_coimage_image_comparison :
78+
is_iso (abelian.coimage_image_comparison α) :=
79+
begin
80+
haveI : ∀ X : C, is_iso ((abelian.coimage_image_comparison α).app X),
81+
{ intros, rw coimage_image_comparison_app', apply_instance, },
82+
apply nat_iso.is_iso_of_is_iso_app,
83+
end
84+
85+
end functor_category
86+
87+
noncomputable instance : abelian (C ⥤ D) :=
88+
abelian.of_coimage_image_comparison_is_iso
89+
90+
end abelian
91+
92+
end category_theory

src/category_theory/limits/preserves/shapes/kernels.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -197,13 +197,13 @@ is_colimit.cocone_point_unique_up_to_iso
197197
(colimit.is_colimit _)
198198

199199
@[simp]
200-
lemma preserves_cokernel.iso_hom :
200+
lemma preserves_cokernel.iso_inv :
201201
(preserves_cokernel.iso G f).inv = cokernel_comparison f G :=
202202
rfl
203203

204204
instance : is_iso (cokernel_comparison f G) :=
205205
begin
206-
rw ← preserves_cokernel.iso_hom,
206+
rw ← preserves_cokernel.iso_inv,
207207
apply_instance
208208
end
209209

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
/-
2+
Copyright (c) 2022 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 category_theory.limits.shapes.finite_limits
7+
import category_theory.limits.functor_category
8+
9+
/-!
10+
# If `D` has finite (co)limits, so do the functor categories `C ⥤ D`.
11+
12+
These are boiler-plate instances, in their own file as neither import otherwise needs the other.
13+
-/
14+
15+
open category_theory
16+
17+
namespace category_theory.limits
18+
19+
universes w v u
20+
variables {C : Type (max v u)} [category.{v} C]
21+
variables {D : Type w} [category.{max v u} D]
22+
23+
instance functor_category_has_finite_limits [has_finite_limits D] :
24+
has_finite_limits (C ⥤ D) :=
25+
{ out := λ J _ _, by exactI infer_instance, }
26+
27+
instance functor_category_has_finite_colimits [has_finite_colimits D] :
28+
has_finite_colimits (C ⥤ D) :=
29+
{ out := λ J _ _, by exactI infer_instance, }
30+
31+
end category_theory.limits

src/category_theory/limits/shapes/kernels.lean

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,13 @@ lemma kernel.lift_map {X Y Z X' Y' Z' : C}
225225
kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w' :=
226226
by { ext, simp [h₁], }
227227

228+
/-- A commuting square of isomorphisms induces an isomorphism of kernels. -/
229+
@[simps]
230+
def kernel.map_iso {X' Y' : C} (f' : X' ⟶ Y') [has_kernel f']
231+
(p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') : kernel f ≅ kernel f' :=
232+
{ hom := kernel.map f f' p.hom q.hom w,
233+
inv := kernel.map f' f p.inv q.inv (by { refine (cancel_mono q.hom).1 _, simp [w], }), }
234+
228235
/-- Every kernel of the zero morphism is an isomorphism -/
229236
instance kernel.ι_zero_is_iso : is_iso (kernel.ι (0 : X ⟶ Y)) :=
230237
equalizer.ι_of_self _
@@ -553,6 +560,13 @@ lemma cokernel.map_desc {X Y Z X' Y' Z' : C}
553560
cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r :=
554561
by { ext, simp [h₂], }
555562

563+
/-- A commuting square of isomorphisms induces an isomorphism of cokernels. -/
564+
@[simps]
565+
def cokernel.map_iso {X' Y' : C} (f' : X' ⟶ Y') [has_cokernel f']
566+
(p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') : cokernel f ≅ cokernel f' :=
567+
{ hom := cokernel.map f f' p.hom q.hom w,
568+
inv := cokernel.map f' f p.inv q.inv (by { refine (cancel_mono q.hom).1 _, simp [w], }), }
569+
556570
/-- The cokernel of the zero morphism is an isomorphism -/
557571
instance cokernel.π_zero_is_iso :
558572
is_iso (cokernel.π (0 : X ⟶ Y)) :=

0 commit comments

Comments
 (0)