add category definition

1 files changed, 43 insertions, 0 deletions

diff --git a/Nominal/Category.lean b/Nominal/Category.lean
new file mode 100644
index 0000000..fc7e161
--- /dev/null
+++ b/Nominal/Category.lean
@@ -0,0 +1,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