From 4e50b688d7914d0d0b3a92027eab20af6f76d71a Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 25 Apr 2022 17:22:45 +0000 Subject: [PATCH] =?UTF-8?q?feat(category=5Ftheory/abelian):=20if=20D=20is?= =?UTF-8?q?=20abelian=20so=20is=20C=20=E2=A5=A4=20D=20(#13686)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Needed for LTE, and also useful to show `Rep k G` is abelian. Co-authored-by: Scott Morrison --- .../abelian/functor_category.lean | 92 +++++++++++++++++++ .../limits/preserves/shapes/kernels.lean | 4 +- .../limits/shapes/functor_category.lean | 31 +++++++ .../limits/shapes/kernels.lean | 14 +++ 4 files changed, 139 insertions(+), 2 deletions(-) create mode 100644 src/category_theory/abelian/functor_category.lean create mode 100644 src/category_theory/limits/shapes/functor_category.lean diff --git a/src/category_theory/abelian/functor_category.lean b/src/category_theory/abelian/functor_category.lean new file mode 100644 index 0000000000000..5ec19afb4b070 --- /dev/null +++ b/src/category_theory/abelian/functor_category.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2022 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import category_theory.abelian.basic +import category_theory.preadditive.functor_category +import category_theory.limits.shapes.functor_category +import category_theory.limits.preserves.shapes.kernels + +/-! +# If `D` is abelian, then the functor category `C ⥤ D` is also abelian. + +-/ + +noncomputable theory + +namespace category_theory +open category_theory.limits + +universes w v u +variables {C : Type (max v u)} [category.{v} C] +variables {D : Type w} [category.{max v u} D] [abelian D] + +namespace abelian + +namespace functor_category +variables {F G : C ⥤ D} (α : F ⟶ G) (X : C) + +/-- The evaluation of the abelian coimage in a functor category is +the abelian coimage of the corresponding component. -/ +@[simps] +def coimage_obj_iso : (abelian.coimage α).obj X ≅ abelian.coimage (α.app X) := +preserves_cokernel.iso ((evaluation C D).obj X) _ ≪≫ + cokernel.map_iso _ _ (preserves_kernel.iso ((evaluation C D).obj X) _) (iso.refl _) + begin + dsimp, + simp only [category.comp_id], + exact (kernel_comparison_comp_ι _ ((evaluation C D).obj X)).symm, + end + +/-- The evaluation of the abelian image in a functor category is +the abelian image of the corresponding component. -/ +@[simps] +def image_obj_iso : (abelian.image α).obj X ≅ abelian.image (α.app X) := +preserves_kernel.iso ((evaluation C D).obj X) _ ≪≫ + kernel.map_iso _ _ (iso.refl _) (preserves_cokernel.iso ((evaluation C D).obj X) _) + begin + apply (cancel_mono (preserves_cokernel.iso ((evaluation C D).obj X) α).inv).1, + simp only [category.assoc, iso.hom_inv_id], + dsimp, + simp only [category.id_comp, category.comp_id], + exact (π_comp_cokernel_comparison _ ((evaluation C D).obj X)).symm, + end + +lemma coimage_image_comparison_app : + coimage_image_comparison (α.app X) = + (coimage_obj_iso α X).inv ≫ (coimage_image_comparison α).app X ≫ (image_obj_iso α X).hom := +begin + ext, + dsimp, + simp only [category.comp_id, category.id_comp, category.assoc, + coimage_image_factorisation, limits.cokernel.π_desc_assoc, limits.kernel.lift_ι], + simp only [←evaluation_obj_map C D X], + erw kernel_comparison_comp_ι _ ((evaluation C D).obj X), + erw π_comp_cokernel_comparison_assoc _ ((evaluation C D).obj X), + simp only [←functor.map_comp], + simp only [coimage_image_factorisation, evaluation_obj_map], +end + +lemma coimage_image_comparison_app' : + (coimage_image_comparison α).app X = + (coimage_obj_iso α X).hom ≫ coimage_image_comparison (α.app X) ≫ (image_obj_iso α X).inv := +by simp only [coimage_image_comparison_app, iso.hom_inv_id_assoc, iso.hom_inv_id, category.assoc, + category.comp_id] + +instance functor_category_is_iso_coimage_image_comparison : + is_iso (abelian.coimage_image_comparison α) := +begin + haveI : ∀ X : C, is_iso ((abelian.coimage_image_comparison α).app X), + { intros, rw coimage_image_comparison_app', apply_instance, }, + apply nat_iso.is_iso_of_is_iso_app, +end + +end functor_category + +noncomputable instance : abelian (C ⥤ D) := +abelian.of_coimage_image_comparison_is_iso + +end abelian + +end category_theory diff --git a/src/category_theory/limits/preserves/shapes/kernels.lean b/src/category_theory/limits/preserves/shapes/kernels.lean index 21448cec3dca3..0662414ba6c4e 100644 --- a/src/category_theory/limits/preserves/shapes/kernels.lean +++ b/src/category_theory/limits/preserves/shapes/kernels.lean @@ -197,13 +197,13 @@ is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) @[simp] -lemma preserves_cokernel.iso_hom : +lemma preserves_cokernel.iso_inv : (preserves_cokernel.iso G f).inv = cokernel_comparison f G := rfl instance : is_iso (cokernel_comparison f G) := begin - rw ← preserves_cokernel.iso_hom, + rw ← preserves_cokernel.iso_inv, apply_instance end diff --git a/src/category_theory/limits/shapes/functor_category.lean b/src/category_theory/limits/shapes/functor_category.lean new file mode 100644 index 0000000000000..46fcedd223700 --- /dev/null +++ b/src/category_theory/limits/shapes/functor_category.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2022 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import category_theory.limits.shapes.finite_limits +import category_theory.limits.functor_category + +/-! +# If `D` has finite (co)limits, so do the functor categories `C ⥤ D`. + +These are boiler-plate instances, in their own file as neither import otherwise needs the other. +-/ + +open category_theory + +namespace category_theory.limits + +universes w v u +variables {C : Type (max v u)} [category.{v} C] +variables {D : Type w} [category.{max v u} D] + +instance functor_category_has_finite_limits [has_finite_limits D] : + has_finite_limits (C ⥤ D) := +{ out := λ J _ _, by exactI infer_instance, } + +instance functor_category_has_finite_colimits [has_finite_colimits D] : + has_finite_colimits (C ⥤ D) := +{ out := λ J _ _, by exactI infer_instance, } + +end category_theory.limits diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean index bddff1b2357ec..3a244f923f03c 100644 --- a/src/category_theory/limits/shapes/kernels.lean +++ b/src/category_theory/limits/shapes/kernels.lean @@ -225,6 +225,13 @@ lemma kernel.lift_map {X Y Z X' Y' Z' : C} kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w' := by { ext, simp [h₁], } +/-- A commuting square of isomorphisms induces an isomorphism of kernels. -/ +@[simps] +def kernel.map_iso {X' Y' : C} (f' : X' ⟶ Y') [has_kernel f'] + (p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') : kernel f ≅ kernel f' := +{ hom := kernel.map f f' p.hom q.hom w, + inv := kernel.map f' f p.inv q.inv (by { refine (cancel_mono q.hom).1 _, simp [w], }), } + /-- Every kernel of the zero morphism is an isomorphism -/ instance kernel.ι_zero_is_iso : is_iso (kernel.ι (0 : X ⟶ Y)) := equalizer.ι_of_self _ @@ -553,6 +560,13 @@ lemma cokernel.map_desc {X Y Z X' Y' Z' : C} cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r := by { ext, simp [h₂], } +/-- A commuting square of isomorphisms induces an isomorphism of cokernels. -/ +@[simps] +def cokernel.map_iso {X' Y' : C} (f' : X' ⟶ Y') [has_cokernel f'] + (p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') : cokernel f ≅ cokernel f' := +{ hom := cokernel.map f f' p.hom q.hom w, + inv := cokernel.map f' f p.inv q.inv (by { refine (cancel_mono q.hom).1 _, simp [w], }), } + /-- The cokernel of the zero morphism is an isomorphism -/ instance cokernel.π_zero_is_iso : is_iso (cokernel.π (0 : X ⟶ Y)) :=