blob: 343c40cc7eaf5265b05a783bb6b03ffbed00ce21 (
plain)
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
|
import Mathlib
import Nominal.Support
import Nominal.Equivariance
/-!
# Nominal Set Category
Nominal sets form a category, where the morphisms are exactly equivariant functions between them.
This file contains formalizations for this category-theoretical view.
-/
variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
open CategoryTheory
/-!
## Category Definition
Definition of the Nom category instance.
-/
section Definition
/-- An object in the category of nominal sets; i.e., a nominal set. -/
structure Nom where
/-- The underlying set. -/
carrier : Type
/-- Nominal set instance. -/
[nom : NominalSet 𝔸 carrier]
attribute [instance] Nom.nom
/-- Construct a nominal set object from a nominal set. -/
def Nom.of (X : Type) [NominalSet 𝔸 X] : Nom 𝔸 := ⟨X⟩
/-- Objects in Nom can be coerced to the underlying nominal set type. -/
instance : CoeSort (Nom 𝔸) Type := ⟨Nom.carrier⟩
/-- A morphism in the category of nominal sets; i.e., an equivariant function. -/
def Nom.Hom (X Y : Nom 𝔸) := X →ₑ[𝔸] Y
/-- Coerce morphisms to functions between the underlying sets. -/
instance (X Y : Nom 𝔸) : CoeFun (Nom.Hom 𝔸 X Y) (fun _ => X.carrier → Y.carrier) where
coe f := f.toFun
/-- Nominal sets form a category with equivariant functions as morphisms. -/
instance : Category (Nom 𝔸) where
Hom := Nom.Hom 𝔸
id X := EquivariantMap.id 𝔸
comp f g := EquivariantMap.comp 𝔸 g f
end Definition
/-!
## Forgetful Functors
Definitions of forgetful functors from the Nom category.
-/
section Forget
/-- The Nom category is a ConcreteCategory where objects correspond to types. -/
instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where
hom := id
ofHom := id
/-- There is a forgetful functor from Nom to the category of monoidal actions. -/
instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where
forget₂ :=
{ obj X := Action.ofMulAction (FPerm 𝔸) X.carrier
map f := ⟨f.toFun, by
intro π
ext x
simp only [types_comp_apply, Action.ofMulAction_apply]
rw [Function.equivariant 𝔸 f.toFun]⟩ }
end Forget
|
