-
Notifications
You must be signed in to change notification settings - Fork 63
/
representations-monoids.lagda.md
81 lines (64 loc) · 2.68 KB
/
representations-monoids.lagda.md
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
69
70
71
72
73
74
75
76
77
78
79
80
81
# Representations of monoids
```agda
module group-theory.representations-monoids where
```
<details><summary>Imports</summary>
```agda
open import category-theory.categories
open import category-theory.endomorphisms-in-categories
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels
open import group-theory.homomorphisms-monoids
open import group-theory.monoids
```
</details>
## Idea
A **representation** of a [monoid](group-theory.monoids.md) `M` in a
[category](category-theory.categories.md) `C` consist of an object `V` in `C`
[equipped](foundation.structure.md) with a
[monoid homomorphism](group-theory.homomorphisms-monoids.md) from `M` to the
monoid of [endomorphisms](category-theory.endomorphisms-in-categories.md) on
`V`.
## Definition
### Representations of a monoid in a category
```agda
representation-category-Monoid :
{l1 l2 l3 : Level} (C : Category l1 l2) (M : Monoid l3) → UU (l1 ⊔ l2 ⊔ l3)
representation-category-Monoid C M =
Σ (obj-Category C) (λ V → type-hom-Monoid M (monoid-endo-Category C V))
module _
{l1 l2 l3 : Level} (C : Category l1 l2) (M : Monoid l3)
(ρ : representation-category-Monoid C M)
where
obj-representation-category-Monoid : obj-Category C
obj-representation-category-Monoid = pr1 ρ
hom-action-representation-category-Monoid :
type-hom-Monoid M
( monoid-endo-Category C obj-representation-category-Monoid)
hom-action-representation-category-Monoid = pr2 ρ
action-representation-category-Monoid :
type-Monoid M → type-endo-Category C obj-representation-category-Monoid
action-representation-category-Monoid =
map-hom-Monoid M
( monoid-endo-Category C obj-representation-category-Monoid)
( hom-action-representation-category-Monoid)
preserves-mul-action-representation-category-Monoid :
( x y : type-Monoid M) →
( action-representation-category-Monoid (mul-Monoid M x y)) =
( comp-endo-Category C
( obj-representation-category-Monoid)
( action-representation-category-Monoid x)
( action-representation-category-Monoid y))
preserves-mul-action-representation-category-Monoid =
preserves-mul-hom-Monoid M
( monoid-endo-Category C obj-representation-category-Monoid)
( hom-action-representation-category-Monoid)
preserves-unit-action-representation-category-Monoid :
action-representation-category-Monoid (unit-Monoid M) =
id-endo-Category C obj-representation-category-Monoid
preserves-unit-action-representation-category-Monoid =
preserves-unit-hom-Monoid M
( monoid-endo-Category C obj-representation-category-Monoid)
( hom-action-representation-category-Monoid)
```