feat(representation_theory/Rep): Rep k G is abelian (#13689)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/abelian/functor_category.lean

@@ -18,17 +18,17 @@ 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
 
+section
+universes z w v u
+variables {C : Type (max v u)} [category.{v} C]
+variables {D : Type w} [category.{max z v u} D] [abelian D]
+
 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. -/
+/-- The abelian coimage in a functor category can be calculated componentwise. -/
 @[simps]
 def coimage_obj_iso : (abelian.coimage α).obj X ≅ abelian.coimage (α.app X) :=
 preserves_cokernel.iso ((evaluation C D).obj X) _ ≪≫
@@ -39,8 +39,7 @@ preserves_cokernel.iso ((evaluation C D).obj X) _ ≪≫
     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. -/
+/-- The abelian image in a functor category can be calculated componentwise. -/
 @[simps]
 def image_obj_iso : (abelian.image α).obj X ≅ abelian.image (α.app X) :=
 preserves_kernel.iso ((evaluation C D).obj X) _ ≪≫
@@ -84,9 +83,23 @@ end
 
 end functor_category
 
-noncomputable instance : abelian (C ⥤ D) :=
+noncomputable instance functor_category_abelian : abelian (C ⥤ D) :=
 abelian.of_coimage_image_comparison_is_iso
 
+end
+
+section
+
+universes u
+variables {C : Type u} [small_category C]
+variables {D : Type (u+1)} [large_category D] [abelian D]
+
+/-- A variant with specialized universes for a common case. -/
+noncomputable instance functor_category_abelian' : abelian (C ⥤ D) :=
+abelian.functor_category_abelian.{u u+1 u u}
+
+end
+
 end abelian
 
 end category_theory

src/category_theory/abelian/transfer.lean

@@ -168,4 +168,15 @@ begin
   apply abelian.of_coimage_image_comparison_is_iso,
 end
 
+/--
+If `C` is an additive category equivalent to an abelian category `D`
+via a functor that preserves zero morphisms,
+then `C` is also abelian.
+-/
+def abelian_of_equivalence
+  {C : Type u₁} [category.{v} C] [preadditive C] [has_finite_products C]
+  {D : Type u₂} [category.{v} D] [abelian D]
+  (F : C ⥤ D) [functor.preserves_zero_morphisms F] [is_equivalence F] : abelian C :=
+abelian_of_adjunction F F.inv F.as_equivalence.unit_iso.symm F.as_equivalence.symm.to_adjunction
+
 end category_theory

src/category_theory/limits/shapes/functor_category.lean

@@ -16,9 +16,9 @@ open category_theory
 
 namespace category_theory.limits
 
-universes w v u
+universes z w v u
 variables {C : Type (max v u)} [category.{v} C]
-variables {D : Type w} [category.{max v u} D]
+variables {D : Type w} [category.{max z v u} D]
 
 instance functor_category_has_finite_limits [has_finite_limits D] :
   has_finite_limits (C ⥤ D) :=

src/representation_theory/Action.lean

@@ -10,6 +10,8 @@ import category_theory.limits.preserves.basic
 import category_theory.adjunction.limits
 import category_theory.monoidal.functor_category
 import category_theory.monoidal.transport
+import category_theory.abelian.functor_category
+import category_theory.abelian.transfer
 
 /-!
 # `Action V G`, the category of actions of a monoid `G` inside some category `V`.
@@ -20,7 +22,9 @@ where `Action (Module R) G` is the category of `R`-linear representations of `G`
 We check `Action V G ≌ (single_obj G ⥤ V)`,
 and construct the restriction functors `res {G H : Mon} (f : G ⟶ H) : Action V H ⥤ Action V G`.
 
-When `V` has (co)limits so does `Action V G`. When `V` is monoidal so is `Action V G`.
+* When `V` has (co)limits so does `Action V G`.
+* When `V` is monoidal so is `Action V G`.
+* When `V` is preadditive or abelian so is `Action V G`.
 -/
 
 universes u
@@ -186,6 +190,10 @@ def functor_category_equivalence : Action V G ≌ (single_obj G ⥤ V) :=
 
 attribute [simps] functor_category_equivalence
 
+instance [has_finite_products V] : has_finite_products (Action V G) :=
+{ out := λ J _ _, by exactI
+  adjunction.has_limits_of_shape_of_equivalence (Action.functor_category_equivalence _ _).functor }
+
 instance [has_limits V] : has_limits (Action V G) :=
 adjunction.has_limits_of_equivalence (Action.functor_category_equivalence _ _).functor
 
@@ -235,6 +243,46 @@ preserves_colimits_of_nat_iso
 
 end forget
 
+section has_zero_morphisms
+variables [has_zero_morphisms V]
+
+instance : has_zero_morphisms (Action V G) :=
+{ has_zero := λ X Y, ⟨⟨0, by tidy⟩⟩, }
+
+instance : functor.preserves_zero_morphisms (functor_category_equivalence V G).functor := {}
+
+end has_zero_morphisms
+
+section preadditive
+variables [preadditive V]
+
+instance : preadditive (Action V G) :=
+{ hom_group := λ X Y,
+  { zero := ⟨0, by simp⟩,
+    add := λ f g, ⟨f.hom + g.hom, by simp [f.comm, g.comm]⟩,
+    neg := λ f, ⟨-f.hom, by simp [f.comm]⟩,
+    zero_add := by { intros, ext, exact zero_add _, },
+    add_zero := by { intros, ext, exact add_zero _, },
+    add_assoc := by { intros, ext, exact add_assoc _ _ _, },
+    add_left_neg := by { intros, ext, exact add_left_neg _, },
+    add_comm := by { intros, ext, exact add_comm _ _, }, },
+  add_comp' := by { intros, ext, exact preadditive.add_comp _ _ _ _ _ _, },
+  comp_add' := by { intros, ext, exact preadditive.comp_add _ _ _ _ _ _, }, }
+
+instance : functor.additive (functor_category_equivalence V G).functor := {}
+
+end preadditive
+
+section abelian
+/-- Auxilliary construction for the `abelian (Action V G)` instance. -/
+def abelian_aux : Action V G ≌ (ulift.{u} (single_obj G) ⥤ V) :=
+(functor_category_equivalence V G).trans (equivalence.congr_left ulift.equivalence)
+
+noncomputable instance [abelian V] : abelian (Action V G) :=
+abelian_of_equivalence abelian_aux.functor
+
+end abelian
+
 section monoidal
 
 instance [monoidal_category V] : monoidal_category (Action V G) :=

src/representation_theory/Rep.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import representation_theory.Action
-import algebra.category.Module.limits
+import algebra.category.Module.abelian
 import algebra.category.Module.colimits
 import algebra.category.Module.monoidal
 
@@ -18,7 +18,7 @@ Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`.
 Conversely, given a homomorphism `ρ : G →* (V →ₗ[k] V)`,
 you can construct the bundled representation as `Rep.of ρ`.
 
-We verify that `Rep k G` has all limits and colimits, and is a monoidal category.
+We verify that `Rep k G` is an abelian monoidal category with all (co)limits.
 -/
 
 universes u
@@ -27,7 +27,7 @@ open category_theory
 open category_theory.limits
 
 /-- The category of `k`-linear representations of a monoid `G`. -/
-@[derive [large_category, concrete_category, has_limits, has_colimits]]
+@[derive [large_category, concrete_category, has_limits, has_colimits, abelian]]
 abbreviation Rep (k G : Type u) [ring k] [monoid G] :=
 Action (Module.{u} k) (Mon.of G)