/
Rep.lean
68 lines (49 loc) · 2.18 KB
/
Rep.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import representation_theory.Action
import algebra.category.Module.abelian
import algebra.category.Module.colimits
import algebra.category.Module.monoidal
/-!
# `Rep k G` is the category of `k`-linear representations of `G`.
If `V : Rep k G`, there is a coercion that allows you to treat `V` as a type,
and this type comes equipped with a `module k V` instance.
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.
-/
universes u
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]]
abbreviation Rep (k G : Type u) [ring k] [monoid G] :=
Action (Module.{u} k) (Mon.of G)
namespace Rep
variables {k G : Type u} [ring k] [monoid G]
instance : has_coe_to_sort (Rep k G) (Type u) := concrete_category.has_coe_to_sort _
instance (V : Rep k G) : add_comm_monoid V :=
by { change add_comm_monoid ((forget₂ (Rep k G) (Module k)).obj V), apply_instance, }
instance (V : Rep k G) : module k V :=
by { change module k ((forget₂ (Rep k G) (Module k)).obj V), apply_instance, }
-- This works well with the new design for representations:
example (V : Rep k G) : G →* (V →ₗ[k] V) := V.ρ
/-- Lift an unbundled representation to `Rep`. -/
@[simps ρ]
def of {V : Type u} [add_comm_group V] [module k V] (ρ : G →* (V →ₗ[k] V)) : Rep k G :=
⟨Module.of k V, ρ⟩
-- Verify that limits are calculated correctly.
noncomputable example : preserves_limits (forget₂ (Rep k G) (Module.{u} k)) :=
by apply_instance
noncomputable example : preserves_colimits (forget₂ (Rep k G) (Module.{u} k)) :=
by apply_instance
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
end Rep