blob: fc7e1618e09a35448b6f7736c223c8a43121b7e6 (
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
|
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 𝔸]
/-!
## 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
/-- A morphism in the category of nominal sets; i.e., an equivariant function. -/
structure Nom.Hom (X Y : Nom 𝔸) where
/-- The underlying function. -/
toFun : X.carrier → Y.carrier
/-- Equivariance of the function. -/
equivariant : Equivariant 𝔸 toFun
/-- Nominal sets form a category with equivariant functions as morphisms. -/
instance : CategoryTheory.Category (Nom 𝔸) where
Hom := Nom.Hom 𝔸
id X := ⟨id, id_equivariant 𝔸⟩
comp f g := ⟨g.toFun ∘ f.toFun, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
end Definition
|
