add forgetful functors

2 files changed, 82 insertions, 11 deletions

diff --git a/Nominal/Category.lean b/Nominal/Category.lean
index fc7e161..9ee4fe3 100644
--- a/Nominal/Category.lean
+++ b/Nominal/Category.lean
@@ -11,6 +11,8 @@ This file contains formalizations for this category-theoretical view.
 
 variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
+open CategoryTheory
+
 /-!
 ## Category Definition
 
@@ -27,17 +29,40 @@ structure Nom where
 
 attribute [instance] Nom.nom
 
+/-- 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. -/
-structure Nom.Hom (X Y : Nom 𝔸) where
-  /-- The underlying function. -/
-  toFun : X.carrier → Y.carrier
-  /-- Equivariance of the function. -/
-  equivariant : Equivariant 𝔸 toFun
+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 : CategoryTheory.Category (Nom 𝔸) where
+instance : Category (Nom 𝔸) where
   Hom := Nom.Hom 𝔸
-  id X := ⟨id, id_equivariant 𝔸⟩
-  comp f g := ⟨g.toFun ∘ f.toFun, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
+  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 {X Y} f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ }
+
+end Forget
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index c9a5261..ac50519 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -71,11 +71,11 @@ lemma id_equivariant : Equivariant 𝔸 (id : X → X) := by
   simp [Equivariant]
 
 /-- The composition of two equivariant functions is equivariant. -/
-lemma comp_equivariant {f : X → Y} {g : Y → Z} : Equivariant 𝔸 f → Equivariant 𝔸 g → Equivariant 𝔸 (g ∘ f) := by
+lemma comp_equivariant {f : Y → Z} {g : X → Y} : Equivariant 𝔸 f → Equivariant 𝔸 g → Equivariant 𝔸 (f ∘ g) := by
   intro hf hg x π
   calc
-    g (f (π • x)) = g (π • f x)   := by rw [hf]
-    _             = π • (g (f x)) := by rw [hg]
+    f (g (π • x)) = f (π • g x)   := by rw [hg]
+    _             = π • (f (g x)) := by rw [hf]
 
 /-- The subset relation is equivariant. -/
 lemma subset_equivariant : EquivariantRelation 𝔸 (Set.Subset : Set X → Set X → Prop) := by
@@ -183,3 +183,49 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
       exact hS.out.right
 
 end Nominal
+
+/-!
+## Bundled Functions
+
+In the following, we also define a bundled function type for equivariant functions.
+-/
+section BundledFunction
+
+/-- A function carrying a proof of its equivariance. -/
+structure EquivariantMap (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] where
+  /-- The underlying function. -/
+  toFun : X → Y
+  /-- Proof of equivariance. -/
+  equivariant : Equivariant 𝔸 toFun
+
+/-- We write `X →ₑ Y` or `X →ₑ[𝔸] Y` for an equivariant map X → Y. -/
+infixr:25 " →ₑ " => EquivariantMap _
+
+/-- We write `X →ₑ Y` or `X →ₑ[𝔸] Y` for an equivariant map X → Y. -/
+notation:25 X " →ₑ[" A "] " Y => EquivariantMap A X Y
+
+variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z]
+
+instance : FunLike (X →ₑ[𝔸] Y) X Y where
+  coe := EquivariantMap.toFun
+  coe_injective' f g h := by cases f; cases g; congr
+
+namespace EquivariantMap
+
+/-- The identity function. -/
+def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩
+
+/-- Function composition. -/
+def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
+
+@[simp]
+lemma toFun_eq_coe {f : X →ₑ[𝔸] Y} : f.toFun = (f : X → Y) :=
+  rfl
+
+@[ext]
+lemma ext {f g : X →ₑ[𝔸] Y} (h : ∀ a, f a = g a) : f = g :=
+  DFunLike.ext _ _ h
+
+end EquivariantMap
+
+end BundledFunction