feat(representation/Rep): linear structures (#13782)

Make `Rep k G` a `k`-linear (and `k`-linear monoidal) category.



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

Author: kim-em

src/algebra/category/Module/monoidal.lean

@@ -8,7 +8,7 @@ import category_theory.closed.monoidal
 import algebra.category.Module.basic
 import linear_algebra.tensor_product
 import category_theory.linear.yoneda
-import category_theory.monoidal.preadditive
+import category_theory.monoidal.linear
 
 /-!
 # The symmetric monoidal category structure on R-modules
@@ -273,6 +273,10 @@ instance : monoidal_preadditive (Module.{u} R) :=
   tensor_add' := by { intros, ext, simp [tensor_product.tmul_add], },
   add_tensor' := by { intros, ext, simp [tensor_product.add_tmul], }, }
 
+instance : monoidal_linear R (Module.{u} R) :=
+{ tensor_smul' := by { intros, ext, simp, },
+  smul_tensor' := by { intros, ext, simp [tensor_product.smul_tmul], }, }
+
 /--
 Auxiliary definition for the `monoidal_closed` instance on `Module R`.
 (This is only a separate definition in order to speed up typechecking. )

src/category_theory/linear/default.lean

@@ -15,6 +15,8 @@ import algebra.algebra.basic
 An `R`-linear category is a category in which `X ⟶ Y` is an `R`-module in such a way that
 composition of morphisms is `R`-linear in both variables.
 
+Note that sometimes in the literature a "linear category" is further required to be abelian.
+
 ## Implementation
 
 Corresponding to the fact that we need to have an `add_comm_group X` structure in place

src/category_theory/linear/functor_category.lean

@@ -0,0 +1,54 @@
+/-
+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.preadditive.functor_category
+import category_theory.linear.default
+
+/-!
+# Linear structure on functor categories
+
+If `C` and `D` are categories and `D` is `R`-linear,
+then `C ⥤ D` is also `R`-linear.
+
+-/
+
+open_locale big_operators
+
+namespace category_theory
+open category_theory.limits linear
+
+variables {R : Type*} [semiring R]
+variables {C D : Type*} [category C] [category D] [preadditive D] [linear R D]
+
+instance functor_category_linear : linear R (C ⥤ D) :=
+{ hom_module := λ F G,
+  { smul := λ r α,
+    { app := λ X, r • α.app X,
+      naturality' := by { intros, rw [comp_smul, smul_comp, α.naturality] } },
+    one_smul := by { intros, ext, apply one_smul },
+    zero_smul := by { intros, ext, apply zero_smul },
+    smul_zero := by { intros, ext, apply smul_zero },
+    add_smul := by { intros, ext, apply add_smul },
+    smul_add := by { intros, ext, apply smul_add },
+    mul_smul := by { intros, ext, apply mul_smul } },
+  smul_comp' := by { intros, ext, apply smul_comp },
+  comp_smul' := by { intros, ext, apply comp_smul } }
+
+namespace nat_trans
+
+variables {F G : C ⥤ D}
+
+/-- Application of a natural transformation at a fixed object,
+as group homomorphism -/
+@[simps] def app_linear_map (X : C) : (F ⟶ G) →ₗ[R] (F.obj X ⟶ G.obj X) :=
+{ to_fun := λ α, α.app X,
+  map_add' := λ _ _, rfl,
+  map_smul' := λ _ _, rfl, }
+
+@[simp] lemma app_smul (X : C) (r : R) (α : F ⟶ G) : (r • α).app X = r • α.app X := rfl
+
+end nat_trans
+
+end category_theory

src/category_theory/monoidal/linear.lean

@@ -0,0 +1,45 @@
+/-
+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.linear.linear_functor
+import category_theory.monoidal.preadditive
+
+/-!
+# Linear monoidal categories
+
+A monoidal category is `monoidal_linear R` if it is monoidal preadditive and
+tensor product of morphisms is `R`-linear in both factors.
+-/
+
+namespace category_theory
+
+open category_theory.limits
+open category_theory.monoidal_category
+
+variables (R : Type*) [semiring R]
+variables (C : Type*) [category C] [preadditive C] [linear R C]
+variables [monoidal_category C] [monoidal_preadditive C]
+
+/--
+A category is `monoidal_linear R` if tensoring is `R`-linear in both factors.
+-/
+class monoidal_linear :=
+(tensor_smul' : ∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z),
+  f ⊗ (r • g) = r • (f ⊗ g) . obviously)
+(smul_tensor' : ∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z),
+  (r • f) ⊗ g = r • (f ⊗ g) . obviously)
+
+restate_axiom monoidal_linear.tensor_smul'
+restate_axiom monoidal_linear.smul_tensor'
+attribute [simp] monoidal_linear.tensor_smul monoidal_linear.smul_tensor
+
+variables [monoidal_linear R C]
+
+instance tensor_left_linear (X : C) : (tensor_left X).linear R := {}
+instance tensor_right_linear (X : C) : (tensor_right X).linear R := {}
+instance tensoring_left_linear (X : C) : ((tensoring_left C).obj X).linear R := {}
+instance tensoring_right_linear (X : C) : ((tensoring_right C).obj X).linear R := {}
+
+end category_theory

src/category_theory/monoidal/transport.lean

@@ -32,7 +32,7 @@ variables {D : Type u₂} [category.{v₂} D]
 /--
 Transport a monoidal structure along an equivalence of (plain) categories.
 -/
-@[simps]
+@[simps {attrs := [`_refl_lemma]}] -- We just want these simp lemmas locally
 def transport (e : C ≌ D) : monoidal_category.{v₂} D :=
 { tensor_obj := λ X Y, e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y),
   tensor_hom := λ W X Y Z f g, e.functor.map (e.inverse.map f ⊗ e.inverse.map g),
@@ -137,6 +137,13 @@ def transported (e : C ≌ D) := D
 instance (e : C ≌ D) : monoidal_category (transported e) := transport e
 instance (e : C ≌ D) : inhabited (transported e) := ⟨𝟙_ _⟩
 
+section
+local attribute [simp] transport_tensor_unit
+
+section
+local attribute [simp] transport_tensor_hom transport_associator
+  transport_left_unitor transport_right_unitor
+
 /--
 We can upgrade `e.functor` to a lax monoidal functor from `C` to `D` with the transported structure.
 -/
@@ -191,6 +198,7 @@ def lax_to_transported (e : C ≌ D) : lax_monoidal_functor C (transported e) :=
     congr' 1,
     simp only [←right_unitor_naturality, id_comp, ←tensor_comp_assoc, comp_id],
   end, }.
+end
 
 /--
 We can upgrade `e.functor` to a monoidal functor from `C` to `D` with the transported structure.
@@ -200,6 +208,7 @@ def to_transported (e : C ≌ D) : monoidal_functor C (transported e) :=
 { to_lax_monoidal_functor := lax_to_transported e,
   ε_is_iso := by { dsimp, apply_instance, },
   μ_is_iso := λ X Y, by { dsimp, apply_instance, }, }
+end
 
 instance (e : C ≌ D) : is_equivalence (to_transported e).to_functor :=
 by { dsimp, apply_instance, }

src/category_theory/preadditive/functor_category.lean

@@ -21,7 +21,7 @@ open category_theory.limits preadditive
 
 variables {C D : Type*} [category C] [category D] [preadditive D]
 
-instance : preadditive (C ⥤ D) :=
+instance functor_category_preadditive : preadditive (C ⥤ D) :=
 { hom_group := λ F G,
   { add := λ α β,
     { app := λ X, α.app X + β.app X,

src/representation_theory/Action.lean

@@ -10,9 +10,11 @@ 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.monoidal.linear
 import category_theory.monoidal.braided
 import category_theory.abelian.functor_category
 import category_theory.abelian.transfer
+import category_theory.linear.functor_category
 
 /-!
 # `Action V G`, the category of actions of a monoid `G` inside some category `V`.
@@ -25,7 +27,7 @@ and construct the restriction functors `res {G H : Mon} (f : G ⟶ H) : Action V
 
 * When `V` has (co)limits so does `Action V G`.
 * When `V` is monoidal, braided, or symmetric, so is `Action V G`.
-* When `V` is preadditive or abelian so is `Action V G`.
+* When `V` is preadditive, linear, or abelian so is `Action V G`.
 -/
 
 universes u
@@ -272,8 +274,33 @@ instance : preadditive (Action V G) :=
 
 instance : functor.additive (functor_category_equivalence V G).functor := {}
 
+@[simp] lemma zero_hom {X Y : Action V G} : (0 : X ⟶ Y).hom = 0 := rfl
+@[simp] lemma neg_hom {X Y : Action V G} (f : X ⟶ Y) : (-f).hom = -f.hom := rfl
+@[simp] lemma add_hom {X Y : Action V G} (f g : X ⟶ Y) : (f + g).hom = f.hom + g.hom := rfl
+
 end preadditive
 
+section linear
+variables [preadditive V] {R : Type*} [semiring R] [linear R V]
+
+instance : linear R (Action V G) :=
+{ hom_module := λ X Y,
+  { smul := λ r f, ⟨r • f.hom, by simp [f.comm]⟩,
+    one_smul := by { intros, ext, exact one_smul _ _, },
+    smul_zero := by { intros, ext, exact smul_zero _, },
+    zero_smul := by { intros, ext, exact zero_smul _ _, },
+    add_smul := by { intros, ext, exact add_smul _ _ _, },
+    smul_add := by { intros, ext, exact smul_add _ _ _, },
+    mul_smul := by { intros, ext, exact mul_smul _ _ _, }, },
+  smul_comp' := by { intros, ext, exact linear.smul_comp _ _ _ _ _ _, },
+  comp_smul' := by { intros, ext, exact linear.comp_smul _ _ _ _ _ _, }, }
+
+instance : functor.linear R (functor_category_equivalence V G).functor := {}
+
+@[simp] lemma smul_hom {X Y : Action V G} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom := rfl
+
+end linear
+
 section abelian
 /-- Auxilliary construction for the `abelian (Action V G)` instance. -/
 def abelian_aux : Action V G ≌ (ulift.{u} (single_obj G) ⥤ V) :=
@@ -290,6 +317,47 @@ variables [monoidal_category V]
 instance : monoidal_category (Action V G) :=
 monoidal.transport (Action.functor_category_equivalence _ _).symm
 
+@[simp] lemma tensor_V {X Y : Action V G} : (X ⊗ Y).V = X.V ⊗ Y.V := rfl
+@[simp] lemma tensor_rho {X Y : Action V G} {g : G} : (X ⊗ Y).ρ g = X.ρ g ⊗ Y.ρ g := rfl
+@[simp] lemma tensor_hom {W X Y Z : Action V G} (f : W ⟶ X) (g : Y ⟶ Z) :
+  (f ⊗ g).hom = f.hom ⊗ g.hom := rfl
+@[simp] lemma associator_hom_hom {X Y Z : Action V G} :
+  hom.hom (α_ X Y Z).hom = (α_ X.V Y.V Z.V).hom :=
+begin
+  dsimp [monoidal.transport_associator],
+  simp,
+end
+@[simp] lemma associator_inv_hom {X Y Z : Action V G} :
+  hom.hom (α_ X Y Z).inv = (α_ X.V Y.V Z.V).inv :=
+begin
+  dsimp [monoidal.transport_associator],
+  simp,
+end
+@[simp] lemma left_unitor_hom_hom {X : Action V G} :
+  hom.hom (λ_ X).hom = (λ_ X.V).hom :=
+begin
+  dsimp [monoidal.transport_left_unitor],
+  simp,
+end
+@[simp] lemma left_unitor_inv_hom {X : Action V G} :
+  hom.hom (λ_ X).inv = (λ_ X.V).inv :=
+begin
+  dsimp [monoidal.transport_left_unitor],
+  simp,
+end
+@[simp] lemma right_unitor_hom_hom {X : Action V G} :
+  hom.hom (ρ_ X).hom = (ρ_ X.V).hom :=
+begin
+  dsimp [monoidal.transport_right_unitor],
+  simp,
+end
+@[simp] lemma right_unitor_inv_hom {X : Action V G} :
+  hom.hom (ρ_ X).inv = (ρ_ X.V).inv :=
+begin
+  dsimp [monoidal.transport_right_unitor],
+  simp,
+end
+
 variables (V G)
 
 /-- When `V` is monoidal the forgetful functor `Action V G` to `V` is monoidal. -/
@@ -302,20 +370,35 @@ def forget_monoidal : monoidal_functor (Action V G) V :=
 instance forget_monoidal_faithful : faithful (forget_monoidal V G).to_functor :=
 by { change faithful (forget V G), apply_instance, }
 
-instance [braided_category V] : braided_category (Action V G) :=
+section
+variables [braided_category V]
+
+instance : braided_category (Action V G) :=
 braided_category_of_faithful (forget_monoidal V G) (λ X Y, mk_iso (β_ _ _) (by tidy)) (by tidy)
 
 /-- When `V` is braided the forgetful functor `Action V G` to `V` is braided. -/
 @[simps]
-def forget_braided [braided_category V] : braided_functor (Action V G) V :=
+def forget_braided : braided_functor (Action V G) V :=
 { ..forget_monoidal _ _, }
 
-instance forget_braided_faithful [braided_category V] : faithful (forget_braided V G).to_functor :=
+instance forget_braided_faithful : faithful (forget_braided V G).to_functor :=
 by { change faithful (forget V G), apply_instance, }
 
+end
+
 instance [symmetric_category V] : symmetric_category (Action V G) :=
 symmetric_category_of_faithful (forget_braided V G)
 
+variables [preadditive V] [monoidal_preadditive V]
+
+local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor
+
+instance : monoidal_preadditive (Action V G) := {}
+
+variables {R : Type*} [semiring R] [linear R V] [monoidal_linear R V]
+
+instance : monoidal_linear R (Action V G) := {}
+
 end monoidal
 
 /-- Actions/representations of the trivial group are just objects in the ambient category. -/
@@ -365,6 +448,14 @@ attribute [simps] res_comp
 -- TODO promote `res` to a pseudofunctor from
 -- the locally discrete bicategory constructed from `Monᵒᵖ` to `Cat`, sending `G` to `Action V G`.
 
+variables {G} {H : Mon.{u}} (f : G ⟶ H)
+
+instance res_additive [preadditive V] : (res V f).additive := {}
+
+variables {R : Type*} [semiring R]
+
+instance res_linear [preadditive V] [linear R V] : (res V f).linear R := {}
+
 end Action
 
 namespace category_theory.functor
@@ -387,4 +478,12 @@ def map_Action (F : V ⥤ W) (G : Mon.{u}) : Action V G ⥤ Action W G :=
   map_id' := λ M, by { ext, simp only [Action.id_hom, F.map_id], },
   map_comp' := λ M N P f g, by { ext, simp only [Action.comp_hom, F.map_comp], }, }
 
+variables (F : V ⥤ W) (G : Mon.{u}) [preadditive V] [preadditive W]
+
+instance map_Action_preadditive [F.additive] : (F.map_Action G).additive := {}
+
+variables {R : Type*} [semiring R] [category_theory.linear R V] [category_theory.linear R W]
+
+instance map_Action_linear [F.additive] [F.linear R] : (F.map_Action G).linear R := {}
+
 end category_theory.functor

src/representation_theory/Rep.lean

@@ -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` is an abelian symmetric monoidal category with all (co)limits.
+We verify that `Rep k G` is a `k`-linear abelian symmetric monoidal category with all (co)limits.
 -/
 
 universes u
@@ -27,10 +27,14 @@ 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, abelian]]
+@[derive [large_category, concrete_category, has_limits, has_colimits,
+  preadditive, abelian]]
 abbreviation Rep (k G : Type u) [ring k] [monoid G] :=
 Action (Module.{u} k) (Mon.of G)
 
+instance (k G : Type u) [comm_ring k] [monoid G] : linear k (Rep k G) :=
+by apply_instance
+
 namespace Rep
 
 variables {k G : Type u} [ring k] [monoid G]
@@ -64,5 +68,7 @@ variables {k G : Type u} [comm_ring k] [monoid G]
 
 -- Verify that the symmetric monoidal structure is available.
 example : symmetric_category (Rep k G) := by apply_instance
+example : monoidal_preadditive (Rep k G) := by apply_instance
+example : monoidal_linear k (Rep k G) := by apply_instance
 
 end Rep