Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 03:48 8edb3d16

View on Github →

feat(representation_theory/Rep): the category of representations (#13683) We define Rep k G, the category of k-linear representations of a monoid G. Happily, by abstract nonsense we get that this has (co)limits and a monoidal structure for free. This should play well with the new design for representations in #13573.

Estimated changes

Created src/representation_theory/Action.lean

added def Action.Action_punit_equivalence

added theorem Action.comp_hom

added def Action.forget

added def Action.forget_monoidal

added def Action.functor_category_equivalence.counit_iso

added def Action.functor_category_equivalence.functor

added def Action.functor_category_equivalence.inverse

added def Action.functor_category_equivalence.unit_iso

added def Action.functor_category_equivalence

added def Action.functor_category_equivalence_comp_evaluation

added def Action.hom.comp

added def Action.hom.id

added structure Action.hom

added theorem Action.id_hom

added def Action.mk_iso

added def Action.res

added def Action.res_comp

added def Action.res_id

added def Action.trivial

added def Action.ρ_Aut

added theorem Action.ρ_one

added structure Action

added def category_theory.functor.map_Action

Created src/representation_theory/Rep.lean

added def Rep.of

added def Rep