From aa280ca672aff145e811b79f4315ba200a09bad5 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 5 Dec 2025 23:19:57 +0100
Subject: define algebras

---
 Nominal/Instances/Basic.lean | 60 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

(limited to 'Nominal/Instances')

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 64b6425..b627c1b 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -237,6 +237,66 @@ end Sum
 
 end Coproducts
 
+/-!
+## Finitary Functions
+
+We can view functions with a finite domain as a finite product. As such, if the codomain is a
+nominal set, the set of such functions is itself a nominal set, where supp f = ⋃₀ {supp (f x) | x}.
+-/
+section FinitaryFunctions
+
+namespace Function
+
+instance {X Y : Type} [Fintype X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) where
+
+variable {X Y : Type} [Fintype X] [NominalSet 𝔸 Y]
+
+private lemma supp' {f : X → Y} : PermSet.HasSupport 𝔸 f (⋃₀ {NominalSet.supp 𝔸 (f x) | x : X}) := by
+  intro π hπ
+  ext x; rw [Pi.smul_apply]
+  show π ∈ PermSet.fix' 𝔸 (f x)
+  apply NominalSet.supp_is_support
+  apply PermSet.fix_antitone_mem 𝔸 hπ
+  apply Set.subset_sUnion_of_mem
+  use x
+
+private lemma fin {f : X → Y} : (⋃₀ {NominalSet.supp 𝔸 (f x) | x : X}).Finite := by
+  apply Set.Finite.sUnion
+  · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+    apply Set.finite_range
+  · intro S ⟨x, hS⟩
+    rw [← hS]
+    apply NominalSet.supp_finite
+
+instance : NominalSet 𝔸 (X → Y) where
+  fin_supp := by
+    intro f; use ⋃₀ {NominalSet.supp 𝔸 (f x) | x : X}
+    exact ⟨supp' 𝔸, fin 𝔸⟩
+
+@[simp] lemma supp {f : X → Y} : NominalSet.supp 𝔸 f = ⋃₀ {NominalSet.supp 𝔸 (f x) | x : X} := by
+  ext a; constructor
+  · apply NominalSet.support_subset_supp
+    · exact supp' 𝔸
+    · exact fin 𝔸
+  · intro hb
+    obtain ⟨S, ⟨x, hx⟩, ha⟩ := hb
+    subst hx
+    intro S hS
+    suffices PermSet.HasSupport 𝔸 (f x) S by
+      apply ha; exact ⟨this, hS.out.right⟩
+    intro π hπ
+    suffices π ∈ PermSet.fix' 𝔸 f by
+      rw [PermSet.fix', Set.mem_setOf_eq] at this
+      rw [PermSet.fix', Set.mem_setOf_eq, ← Pi.smul_apply, this]
+    exact (hS.out.left hπ).out
+
+@[simp] lemma fresh {a : 𝔸} {f : X → Y} : a # f ↔ ∀ x, a # (f x) := by
+  simp [NominalSet.IsFresh]
+
+end Function
+
+end FinitaryFunctions
+
 /-!
 ## Quotient Types
 
-- 
cgit v1.3.1