feat(representation_theory): fdRep k G is k-linear with finite dimens…

…ional hom spaces (#13789)

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

src/algebra/category/FinVect.lean

@@ -13,9 +13,17 @@ import algebra.category.Module.monoidal
 # The category of finite dimensional vector spaces
 
 This introduces `FinVect K`, the category of finite dimensional vector spaces over a field `K`.
-It is implemented as a full subcategory on a subtype of `Module K`, which inherits monoidal and
-symmetric structure as `finite_dimensional K` is a monoidal predicate.
-We also provide a right rigid monoidal category instance.
+It is implemented as a full subcategory on a subtype of `Module K`.
+
+We first create the instance as a `K`-linear category,
+then as a `K`-linear monoidal category and then as a right-rigid monoidal category.
+
+## Future work
+
+* Show that `FinVect K` is a symmetric monoidal category (it is already monoidal).
+* Show that `FinVect K` is abelian.
+* Show that `FinVect K` is rigid (it is already right rigid).
+
 -/
 noncomputable theory
 
@@ -36,8 +44,9 @@ instance closed_predicate_finite_dimensional :
 { prop_ihom' := λ X Y hX hY, by exactI @linear_map.finite_dimensional K _ X _ _ hX Y _ _ hY }
 
 /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/
-@[derive [large_category, concrete_category, monoidal_category, symmetric_category,
-monoidal_closed]]
+@[derive [large_category, concrete_category, preadditive, linear K,
+  monoidal_category, symmetric_category, monoidal_preadditive, monoidal_linear K,
+  monoidal_closed]]
 def FinVect := full_subcategory (λ (V : Module.{u} K), finite_dimensional K V)
 
 namespace FinVect
@@ -50,12 +59,28 @@ instance : inhabited (FinVect K) := ⟨⟨Module.of K K, finite_dimensional.fini
 def of (V : Type u) [add_comm_group V] [module K V] [finite_dimensional K V] : FinVect K :=
 ⟨Module.of K V, by { change finite_dimensional K V, apply_instance }⟩
 
+instance (V W : FinVect K) : finite_dimensional K (V ⟶ W) :=
+(by apply_instance : finite_dimensional K (V.obj →ₗ[K] W.obj))
+
 instance : has_forget₂ (FinVect.{u} K) (Module.{u} K) :=
 by { dsimp [FinVect], apply_instance, }
 
 instance : full (forget₂ (FinVect K) (Module.{u} K)) :=
 { preimage := λ X Y f, f, }
 
+/-- The forgetful functor `FinVect K ⥤ Module K` as a monoidal functor. -/
+def forget₂_monoidal : monoidal_functor (FinVect K) (Module.{u} K) :=
+monoidal_category.full_monoidal_subcategory_inclusion _
+
+instance forget₂_monoidal_faithful : faithful (forget₂_monoidal K).to_functor :=
+by { dsimp [forget₂_monoidal], apply_instance, }
+
+instance forget₂_monoidal_additive : (forget₂_monoidal K).to_functor.additive :=
+by { dsimp [forget₂_monoidal], apply_instance, }
+
+instance forget₂_monoidal_linear : (forget₂_monoidal K).to_functor.linear K :=
+by { dsimp [forget₂_monoidal], apply_instance, }
+
 variables (V W : FinVect K)
 
 @[simp] lemma ihom_obj : (ihom V).obj W = FinVect.of K (V.obj →ₗ[K] W.obj) := rfl

src/category_theory/linear/default.lean

@@ -88,13 +88,18 @@ section induced_category
 universes u'
 variables {C} {D : Type u'} (F : D → C)
 
-instance induced_category.category : linear.{w v} R (induced_category C F) :=
+instance induced_category : linear.{w v} R (induced_category C F) :=
 { hom_module := λ X Y, @linear.hom_module R _ C _ _ _ (F X) (F Y),
   smul_comp' := λ P Q R f f' g, smul_comp' _ _ _ _ _ _,
   comp_smul' := λ P Q R f g g', comp_smul' _ _ _ _ _ _, }
 
 end induced_category
 
+instance full_subcategory (Z : C → Prop) : linear.{w v} R (full_subcategory Z) :=
+{ hom_module := λ X Y, @linear.hom_module R _ C _ _ _ X.obj Y.obj,
+  smul_comp' := λ P Q R f f' g, smul_comp' _ _ _ _ _ _,
+  comp_smul' := λ P Q R f g g', comp_smul' _ _ _ _ _ _, }
+
 variables (R)
 
 /-- Composition by a fixed left argument as an `R`-linear map. -/

src/category_theory/linear/linear_functor.lean

@@ -71,6 +71,10 @@ instance induced_functor_linear : functor.linear R (induced_functor F) := {}
 
 end induced_category
 
+instance full_subcategory_inclusion_linear
+  {C : Type*} [category C] [preadditive C] [category_theory.linear R C] (Z : C → Prop) :
+  (full_subcategory_inclusion Z).linear R := {}
+
 section
 
 variables {R} {C D : Type*} [category C] [category D]

src/category_theory/monoidal/linear.lean

@@ -35,11 +35,32 @@ 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]
+variables {C} [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 := {}
 
+/-- A faithful linear monoidal functor to a linear monoidal category
+ensures that the domain is linear monoidal. -/
+def monoidal_linear_of_faithful
+  {D : Type*} [category D] [preadditive D] [linear R D]
+  [monoidal_category D] [monoidal_preadditive D]
+  (F : monoidal_functor D C) [faithful F.to_functor]
+  [F.to_functor.additive] [F.to_functor.linear R] :
+  monoidal_linear R D :=
+{ tensor_smul' := begin
+    intros,
+    apply F.to_functor.map_injective,
+    simp only [F.to_functor.map_smul r (f ⊗ g), F.to_functor.map_smul r g, F.map_tensor,
+      monoidal_linear.tensor_smul, linear.smul_comp, linear.comp_smul],
+  end,
+  smul_tensor' := begin
+    intros,
+    apply F.to_functor.map_injective,
+    simp only [F.to_functor.map_smul r (f ⊗ g), F.to_functor.map_smul r f, F.map_tensor,
+      monoidal_linear.smul_tensor, linear.smul_comp, linear.comp_smul],
+  end, }
+
 end category_theory

src/category_theory/monoidal/preadditive.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.preadditive.additive_functor
-import category_theory.monoidal.category
+import category_theory.monoidal.functor
 
 /-!
 # Preadditive monoidal categories
@@ -41,7 +41,7 @@ restate_axiom monoidal_preadditive.tensor_add'
 restate_axiom monoidal_preadditive.add_tensor'
 attribute [simp] monoidal_preadditive.tensor_zero monoidal_preadditive.zero_tensor
 
-variables [monoidal_preadditive C]
+variables {C} [monoidal_preadditive C]
 
 local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor
 
@@ -50,6 +50,26 @@ instance tensor_right_additive (X : C) : (tensor_right X).additive := {}
 instance tensoring_left_additive (X : C) : ((tensoring_left C).obj X).additive := {}
 instance tensoring_right_additive (X : C) : ((tensoring_right C).obj X).additive := {}
 
+/-- A faithful additive monoidal functor to a monoidal preadditive category
+ensures that the domain is monoidal preadditive. -/
+def monoidal_preadditive_of_faithful {D : Type*} [category D] [preadditive D] [monoidal_category D]
+  (F : monoidal_functor D C) [faithful F.to_functor] [F.to_functor.additive] :
+  monoidal_preadditive D :=
+{ tensor_zero' := by { intros, apply F.to_functor.map_injective, simp [F.map_tensor], },
+  zero_tensor' := by { intros, apply F.to_functor.map_injective, simp [F.map_tensor], },
+  tensor_add' := begin
+    intros,
+    apply F.to_functor.map_injective,
+    simp only [F.map_tensor, F.to_functor.map_add, preadditive.comp_add, preadditive.add_comp,
+      monoidal_preadditive.tensor_add],
+  end,
+  add_tensor' := begin
+    intros,
+    apply F.to_functor.map_injective,
+    simp only [F.map_tensor, F.to_functor.map_add, preadditive.comp_add, preadditive.add_comp,
+      monoidal_preadditive.add_tensor],
+  end, }
+
 open_locale big_operators
 
 lemma tensor_sum {P Q R S : C} {J : Type*} (s : finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) :

src/category_theory/monoidal/subcategory.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Labelle
 -/
 import category_theory.monoidal.braided
+import category_theory.monoidal.linear
 import category_theory.concrete_category.basic
+import category_theory.preadditive.additive_functor
+import category_theory.linear.linear_functor
 import category_theory.closed.monoidal
 
 /-!
@@ -82,6 +85,28 @@ instance full_monoidal_subcategory.full :
 instance full_monoidal_subcategory.faithful :
   faithful (full_monoidal_subcategory_inclusion P).to_functor := full_subcategory.faithful P
 
+section
+
+variables [preadditive C]
+
+instance full_monoidal_subcategory_inclusion_additive :
+  (full_monoidal_subcategory_inclusion P).to_functor.additive :=
+functor.full_subcategory_inclusion_additive _
+
+instance [monoidal_preadditive C] : monoidal_preadditive (full_subcategory P) :=
+monoidal_preadditive_of_faithful (full_monoidal_subcategory_inclusion P)
+
+variables (R : Type*) [ring R] [linear R C]
+
+instance full_monoidal_subcategory_inclusion_linear :
+  (full_monoidal_subcategory_inclusion P).to_functor.linear R :=
+functor.full_subcategory_inclusion_linear R _
+
+instance [monoidal_preadditive C] [monoidal_linear R C] : monoidal_linear R (full_subcategory P) :=
+monoidal_linear_of_faithful R (full_monoidal_subcategory_inclusion P)
+
+end
+
 variables {P} {P' : C → Prop} [monoidal_predicate P']
 
 /-- An implication of predicates `P → P'` induces a monoidal functor between full monoidal

src/category_theory/preadditive/additive_functor.lean

@@ -98,6 +98,10 @@ instance induced_functor_additive : functor.additive (induced_functor F) := {}
 
 end induced_category
 
+instance full_subcategory_inclusion_additive
+  {C : Type*} [category C] [preadditive C] (Z : C → Prop) :
+  (full_subcategory_inclusion Z).additive := {}
+
 section
 -- To talk about preservation of biproducts we need to specify universes explicitly.
 
@@ -154,7 +158,7 @@ full_subcategory (λ (F : C ⥤ D), F.additive)
 infixr ` ⥤+ `:26 := AdditiveFunctor
 
 instance : preadditive (C ⥤+ D) :=
-preadditive.induced_category.category _
+preadditive.induced_category _
 
 /-- An additive functor is in particular a functor. -/
 @[derive full, derive faithful]

src/category_theory/preadditive/default.lean

@@ -83,13 +83,18 @@ section induced_category
 universes u'
 variables {C} {D : Type u'} (F : D → C)
 
-instance induced_category.category : preadditive.{v} (induced_category C F) :=
+instance induced_category : preadditive.{v} (induced_category C F) :=
 { hom_group := λ P Q, @preadditive.hom_group C _ _ (F P) (F Q),
   add_comp' := λ P Q R f f' g, add_comp' _ _ _ _ _ _,
   comp_add' := λ P Q R f g g', comp_add' _ _ _ _ _ _, }
 
 end induced_category
 
+instance full_subcategory (Z : C → Prop) : preadditive.{v} (full_subcategory Z) :=
+{ hom_group := λ P Q, @preadditive.hom_group C _ _ P.obj Q.obj,
+  add_comp' := λ P Q R f f' g, add_comp' _ _ _ _ _ _,
+  comp_add' := λ P Q R f g g', comp_add' _ _ _ _ _ _, }
+
 instance (X : C) : add_comm_group (End X) := by { dsimp [End], apply_instance, }
 
 instance (X : C) : ring (End X) :=

src/representation_theory/Action.lean

@@ -267,9 +267,15 @@ section has_zero_morphisms
 variables [has_zero_morphisms V]
 
 instance : has_zero_morphisms (Action V G) :=
-{ has_zero := λ X Y, ⟨⟨0, by tidy⟩⟩, }
+{ has_zero := λ X Y, ⟨⟨0, by { intro g, simp }⟩⟩,
+  comp_zero' := λ P Q f R, by { ext1, simp },
+  zero_comp' := λ P Q R f, by { ext1, simp }, }
 
-instance : functor.preserves_zero_morphisms (functor_category_equivalence V G).functor := {}
+instance forget_preserves_zero_morphisms : functor.preserves_zero_morphisms (forget V G) := {}
+instance forget₂_preserves_zero_morphisms [concrete_category V] :
+  functor.preserves_zero_morphisms (forget₂ (Action V G) V) := {}
+instance functor_category_equivalence_preserves_zero_morphisms :
+  functor.preserves_zero_morphisms (functor_category_equivalence V G).functor := {}
 
 end has_zero_morphisms
 
@@ -289,8 +295,12 @@ instance : preadditive (Action V G) :=
   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 := {}
-instance forget_additive : functor.additive (forget V G) := {}
+instance forget_additive :
+  functor.additive (forget V G) := {}
+instance forget₂_additive [concrete_category V] :
+  functor.additive (forget₂ (Action V G) V) := {}
+instance functor_category_equivalence_additive :
+  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
@@ -315,7 +325,12 @@ instance : linear R (Action V G) :=
   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 := {}
+instance forget_linear :
+  functor.linear R (forget V G) := {}
+instance forget₂_linear [concrete_category V] :
+  functor.linear R (forget₂ (Action V G) V) := {}
+instance functor_category_equivalence_linear :
+  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
 
@@ -412,10 +427,10 @@ instance [symmetric_category V] : symmetric_category (Action V G) :=
 symmetric_category_of_faithful (forget_braided V G)
 
 section
-local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor
-
 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]

src/representation_theory/fdRep.lean

@@ -17,13 +17,15 @@ 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 `fdRep k G` is a rigid monoidal category.
+We verify that `fdRep k G` is a `k`-linear monoidal category, and right rigid when `G` is a group.
 
 ## TODO
+* `fdRep k G ≌ full_subcategory (finite_dimensional k)`
+* Upgrade the right rigid structure to a rigid structure (this just needs to be done for `FinVect`).
 * `fdRep k G` has all finite (co)limits.
 * `fdRep k G` is abelian.
 * `fdRep k G ≌ FinVect (monoid_algebra k G)` (this will require generalising `FinVect` first).
-* Upgrade the right rigid structure to a rigid structure.
+
 -/
 
 universes u
@@ -32,14 +34,16 @@ open category_theory
 open category_theory.limits
 
 /-- The category of finite dimensional `k`-linear representations of a monoid `G`. -/
-@[derive [large_category, concrete_category/-, has_limits, has_colimits-/]]
+@[derive [large_category, concrete_category, preadditive]]
 abbreviation fdRep (k G : Type u) [field k] [monoid G] :=
 Action (FinVect.{u} k) (Mon.of G)
 
 namespace fdRep
 
 variables {k G : Type u} [field k] [monoid G]
 
+instance : linear k (fdRep k G) := by apply_instance
+
 instance : has_coe_to_sort (fdRep k G) (Type u) := concrete_category.has_coe_to_sort _
 
 instance (V : fdRep k G) : add_comm_group V :=
@@ -51,6 +55,11 @@ by { change module k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_inst
 instance (V : fdRep k G) : finite_dimensional k V :=
 by { change finite_dimensional k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_instance, }
 
+/-- All hom spaces are finite dimensional. -/
+instance (V W : fdRep k G) : finite_dimensional k (V ⟶ W) :=
+finite_dimensional.of_injective
+  ((forget₂ (fdRep k G) (FinVect k)).map_linear_map k) (functor.map_injective _)
+
 /-- The monoid homomorphism corresponding to the action of `G` onto `V : fdRep k G`. -/
 def ρ (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ
 
@@ -66,9 +75,6 @@ begin
   exact (i.hom.comm g).symm,
 end
 
--- This works well with the new design for representations:
-example (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ
-
 /-- Lift an unbundled representation to `fdRep`. -/
 @[simps ρ]
 def of {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V]
@@ -80,6 +86,8 @@ instance : has_forget₂ (fdRep k G) (Rep k G) :=
 
 -- Verify that the monoidal structure is available.
 example : monoidal_category (fdRep k G) := by apply_instance
+example : monoidal_preadditive (fdRep k G) := by apply_instance
+example : monoidal_linear k (fdRep k G) := by apply_instance
 
 end fdRep