define algebras

4 files changed, 103 insertions, 19 deletions

diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean
index 142c49c..e2cd052 100644
--- a/Algebra/Derivations.lean
+++ b/Algebra/Derivations.lean
@@ -1,7 +1,7 @@
 import Mathlib
 import Algebra.Terms
 
-namespace Algebra
+namespace NominalAlgebra
 
 section Theories
 
@@ -237,4 +237,4 @@ instance TermAtDepth.setoid : Setoid (TermAtDepth 𝔸 T.sig X n) where
 
 end DerivableEquations
 
-end Algebra
+end NominalAlgebra
diff --git a/Algebra/Semantics.lean b/Algebra/Semantics.lean
new file mode 100644
index 0000000..f5160dd
--- /dev/null
+++ b/Algebra/Semantics.lean
@@ -0,0 +1,34 @@
+import Mathlib
+import Algebra.Terms
+import Algebra.Derivations
+
+namespace NominalAlgebra
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable (sig : Signature)
+
+structure Algebra where
+  carrier : ℕ → Nom 𝔸
+  pure (f : sig.pure) {m : ℕ} :
+    (sig.pureArgs f → carrier m) →ₑ[𝔸] carrier (m + sig.pureDepth f)
+  free (f : sig.free) {m : ℕ} :
+    (𝔸 × (sig.freeArgs f → carrier m)) →ₑ[𝔸] carrier (m + sig.freeDepth f)
+  bound (f : sig.bound) {m : ℕ} :
+    NameAbstraction 𝔸 (sig.boundArgs f → carrier m) →ₑ[𝔸] carrier (m + sig.boundDepth f)
+
+instance : CoeFun (Algebra 𝔸 sig) (fun _ => ℕ → Nom 𝔸) where
+  coe A := A.carrier
+
+structure Algebra.Hom (A B : Algebra 𝔸 sig) where
+  toFun : (n : ℕ) → (A n →ₑ[𝔸] B n)
+  preserve_pure : ∀ (f : sig.pure) {m : ℕ} (args : sig.pureArgs f → A m),
+    toFun (m + sig.pureDepth f) (A.pure f args) = B.pure f (toFun m ∘ args)
+  preserve_free : ∀ (a : 𝔸) (f : sig.free) {m : ℕ} (args : sig.freeArgs f → A m),
+    toFun (m + sig.freeDepth f) (A.free f ⟨a, args⟩) = B.free f ⟨a, toFun m ∘ args⟩
+  preserve_bound : ∀ (a : 𝔸) (f : sig.bound) {m : ℕ} (args : sig.boundArgs f → A m),
+    toFun (m + sig.boundDepth f) (A.bound f (⟪a⟫ args)) = B.bound f (⟪a⟫ toFun m ∘ args)
+
+instance {A B : Algebra 𝔸 sig} : CoeFun (Algebra.Hom 𝔸 sig A B) (fun _ => (n : ℕ) → (A n →ₑ[𝔸] B n)) where
+  coe h := h.toFun
+
+end NominalAlgebra
diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean
index 997dca4..568f5cb 100644
--- a/Algebra/Terms.lean
+++ b/Algebra/Terms.lean
@@ -1,7 +1,7 @@
 import Mathlib
 import Nominal
 
-namespace Algebra
+namespace NominalAlgebra
 
 section Definitions
 
@@ -20,9 +20,9 @@ def Signature.pureArgs (sig : Signature) (f : sig.pure) : Type := sig.args (.inl
 def Signature.freeArgs (sig : Signature) (f : sig.free) : Type := sig.args (.inr (.inl f))
 def Signature.boundArgs (sig : Signature) (f : sig.bound) : Type := sig.args (.inr (.inr f))
 
-def Signature.pureArgs_fintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f)
-def Signature.freeArgs_fintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f))
-def Signature.boundArgs_fintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f))
+instance Signature.instPureArgsFintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f)
+instance Signature.instFreeArgsFintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f))
+instance Signature.instBoundArgsFintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f))
 
 def Signature.arity (sig : Signature) (f : sig.pure ⊕ sig.free ⊕ sig.bound) : ℕ := (sig.args_fintype f).card
 def Signature.pureArity (sig : Signature) (f : sig.pure) : ℕ := sig.arity (.inl f)
@@ -217,23 +217,13 @@ private def atoms : Term 𝔸 sig X → Set 𝔸
 private lemma atoms_finite (t : Term 𝔸 sig X) : t.atoms.Finite := by
   fun_induction atoms <;> all_goals expose_names
   · exact NominalSet.supp_finite 𝔸
-  · have hfin := (sig.pureArgs_fintype f).finite
-    apply Set.Finite.sUnion
+  · 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]
       exact ih1 x
-  · have hfin := (sig.freeArgs_fintype f).finite
-    apply Set.Finite.union
-    · exact Set.finite_singleton a
-    · 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]
-        exact ih1 x
-  · have hfin := (sig.boundArgs_fintype f).finite
+  all_goals
     apply Set.Finite.union
     · exact Set.finite_singleton a
     · apply Set.Finite.sUnion
@@ -319,4 +309,4 @@ end TermAtDepth
 
 end NominalSet
 
-end Algebra
+end NominalAlgebra
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
@@ -238,6 +238,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
 
 If ≈ is an equivariant relation on X × X, then X/≈ is a nominal set with `supp [x] = ⋂₀ {supp y | y ∈ [x]}`.