Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 17:58 31529827

View on Github →

feat(representation/Rep): linear structures (#13782) Make Rep k G a k-linear (and k-linear monoidal) category.

Estimated changes

Modified src/algebra/category/Module/monoidal.lean

Modified src/category_theory/linear/default.lean

Created src/category_theory/linear/functor_category.lean

added def category_theory.nat_trans.app_linear_map

added theorem category_theory.nat_trans.app_smul

Created src/category_theory/monoidal/linear.lean

Modified src/category_theory/monoidal/transport.lean

Modified src/category_theory/preadditive/functor_category.lean

Modified src/representation_theory/Action.lean

added theorem Action.add_hom

added theorem Action.associator_hom_hom

added theorem Action.associator_inv_hom

modified def Action.forget_braided

added theorem Action.left_unitor_hom_hom

added theorem Action.left_unitor_inv_hom

added theorem Action.neg_hom

added theorem Action.right_unitor_hom_hom

added theorem Action.right_unitor_inv_hom

added theorem Action.smul_hom

added theorem Action.tensor_V

added theorem Action.tensor_hom

added theorem Action.tensor_rho

added theorem Action.zero_hom

Modified src/representation_theory/Rep.lean