feat(representation_theory): Rep k G is symmetric monoidal (#13685)

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

src/representation_theory/Action.lean

@@ -10,6 +10,7 @@ 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.braided
 import category_theory.abelian.functor_category
 import category_theory.abelian.transfer
 
@@ -23,7 +24,7 @@ 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` is monoidal, braided, or symmetric, so is `Action V G`.
 * When `V` is preadditive or abelian so is `Action V G`.
 -/
 
@@ -216,11 +217,11 @@ def forget : Action V G ⥤ V :=
 { obj := λ M, M.V,
   map := λ M N f, f.hom, }
 
+instance : faithful (forget V G) :=
+{ map_injective' := λ X Y f g w, hom.ext _ _ w, }
+
 instance [concrete_category V] : concrete_category (Action V G) :=
-{ forget := forget V G ⋙ (concrete_category.forget V),
-  forget_faithful :=
-  { map_injective' := λ M N f g w,
-      hom.ext _ _ (faithful.map_injective (concrete_category.forget V) w), } }
+{ forget := forget V G ⋙ (concrete_category.forget V), }
 
 instance has_forget_to_V [concrete_category V] : has_forget₂ (Action V G) V :=
 { forget₂ := forget V G }
@@ -284,18 +285,36 @@ abelian_of_equivalence abelian_aux.functor
 end abelian
 
 section monoidal
+variables [monoidal_category V]
 
-instance [monoidal_category V] : monoidal_category (Action V G) :=
+instance : monoidal_category (Action V G) :=
 monoidal.transport (Action.functor_category_equivalence _ _).symm
 
+variables (V G)
+
 /-- When `V` is monoidal the forgetful functor `Action V G` to `V` is monoidal. -/
 @[simps]
-def forget_monoidal [monoidal_category V] : monoidal_functor (Action V G) V :=
+def forget_monoidal : monoidal_functor (Action V G) V :=
 { ε := 𝟙 _,
   μ := λ X Y, 𝟙 _,
   ..Action.forget _ _, }
 
--- TODO braiding and symmetry
+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) :=
+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 :=
+{ ..forget_monoidal _ _, }
+
+instance forget_braided_faithful [braided_category V] : faithful (forget_braided V G).to_functor :=
+by { change faithful (forget V G), apply_instance, }
+
+instance [symmetric_category V] : symmetric_category (Action V G) :=
+symmetric_category_of_faithful (forget_braided V G)
 
 end monoidal
 

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 monoidal category with all (co)limits.
+We verify that `Rep k G` is an abelian symmetric monoidal category with all (co)limits.
 -/
 
 universes u
@@ -62,7 +62,7 @@ end Rep
 namespace Rep
 variables {k G : Type u} [comm_ring k] [monoid G]
 
--- Verify that the monoidal structure is available.
-example : monoidal_category (Rep k G) := by apply_instance
+-- Verify that the symmetric monoidal structure is available.
+example : symmetric_category (Rep k G) := by apply_instance
 
 end Rep