1 files changed, 107 insertions, 9 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index e902e58..3df5999 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -33,19 +33,26 @@ notation "⊥[" A "]" => AlgebraStructure.bot' A ()
 notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
 notation:60 a " \\ " x => AlgebraStructure.res (⟪a⟫ x)
 
+class AlgebraMorphism
+    {X Y : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] [NominalSet 𝔸 Y] [AlgebraStructure 𝔸 Y]
+    (f : X → Y) [Function.Equivariant 𝔸 f] : Prop where
+  preserve_bot : f (⊥[𝔸]) = ⊥[𝔸]
+  preserve_join : ∀ x y, f (x ∨[𝔸] y) = (f x) ∨[𝔸] (f y)
+  preserve_res : ∀ a x, f (a \ x) = (AlgebraStructure.res : NameAbstraction 𝔸 Y →ₑ[𝔸] Y) (⟪a⟫ (f x))
+
 -- M₁ algebra structure
 
 class Depth1AlgebraStructure (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] [AlgebraStructure 𝔸 Y] extends AlgebraStructure 𝔸 X where
   pre : (𝔸 × Y) →ₑ[𝔸] X
   abs : NameAbstraction 𝔸 Y →ₑ[𝔸] X
-  ax_pre_distributive : ∀ a x y, pre (a, x ∨[𝔸] y) = join (pre (a, x), pre (a, y))
-  ax_pre_bot : ∀ a, pre (a, ⊥[𝔸]) = bot ()
-  ax_pre_restrict_self : ∀ a x, res (⟪a⟫ pre (a, x)) = bot ()
-  ax_pre_restrict_other : ∀ a b x, a ≠ b → res (⟪a⟫ pre (b, x)) = pre (b, a \ x)
-  ax_abs_distributive : ∀ a x y, abs (⟪a⟫ x ∨[𝔸] y) = join (abs (⟪a⟫ x), abs (⟪a⟫ y))
-  ax_abs_bot : ∀ a, abs (⟪a⟫ ⊥[𝔸]) = bot ()
-  ax_abs_restrict_other : ∀ a b x, a ≠ b → abs (⟪a⟫ (b \ x)) = res (⟪b⟫ abs (⟪a⟫ x))
-  ax_local : ∀ a x, abs (⟪a⟫ x) = join (abs (⟪a⟫ x), pre (a, x))
+  ax_pre_distributive : ∀ a x y, pre (a, x ∨[𝔸] y) = pre (a, x) ∨[𝔸] pre (a, y)
+  ax_pre_bot : ∀ a, pre (a, ⊥[𝔸]) = ⊥[𝔸]
+  ax_pre_restrict_self : ∀ a x, (a \ pre (a, x)) = ⊥[𝔸]
+  ax_pre_restrict_other : ∀ a b x, a ≠ b → (a \ pre (b, x)) = pre (b, a \ x)
+  ax_abs_distributive : ∀ a x y, abs (⟪a⟫ x ∨[𝔸] y) = abs (⟪a⟫ x) ∨[𝔸] abs (⟪a⟫ y)
+  ax_abs_bot : ∀ a, abs (⟪a⟫ ⊥[𝔸]) = ⊥[𝔸]
+  ax_abs_restrict_other : ∀ a b x, a ≠ b → abs (⟪a⟫ (b \ x)) = b \ abs (⟪a⟫ x)
+  ax_local : ∀ a x, abs (⟪a⟫ x) = abs (⟪a⟫ x) ∨[𝔸] pre (a, x)
 
 -- Structure Definitions
 
@@ -1088,7 +1095,7 @@ private lemma pre_req2 {a : 𝔸} {x : X} : Req2 𝔸 (pre' 𝔸 (a, x)) := by
   rw [AlgebraStructure.res_bot]
   rw [AlgebraStructure.ax_neutral]
 
-noncomputable def pre : (𝔸 × X )→ StepModel 𝔸 X :=
+noncomputable def pre : (𝔸 × X ) → StepModel 𝔸 X :=
   fun p ↦ ⟨pre' 𝔸 p, by
     suffices ∀ p, Req2 𝔸 (pre' 𝔸 p) by apply this
     intro ⟨a, x⟩
@@ -1341,6 +1348,97 @@ noncomputable instance : Depth1AlgebraStructure 𝔸 (StepModel 𝔸 X) X where
     · rw [union_eq, pre_eq_if_ne 𝔸 (Ne.symm heq)]
       rw [AlgebraStructure.ax_neutral]
 
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [AlgebraStructure 𝔸 X] [AlgebraStructure 𝔸 Y]
+
+def fmap'' (f : X → Y) [Function.Equivariant 𝔸 f] : StepModel 𝔸 X → (𝔸 → Y) :=
+  fun M ↦
+    fun b ↦ f (M.val.val b)
+
+instance {f : X → Y} [Function.Equivariant 𝔸 f] : Function.Equivariant 𝔸 (fmap'' 𝔸 f) := by
+  constructor; intro M π; ext a
+  simp only [fmap'', smul_val, PermSet.Finsupp.smul_val, PermSet.smul_function]
+  rw [Function.equivariant 𝔸 f]
+
+private def fmap' (f : X → Y) [Function.Equivariant 𝔸 f] :
+    StepModel 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 Y :=
+  fun M ↦ ⟨fmap'' 𝔸 f M, by
+    use NominalSet.supp 𝔸 M; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+private lemma fmap_req2 {f : X → Y} [Function.Equivariant 𝔸 f] [AlgebraMorphism 𝔸 f] {M : StepModel 𝔸 X} :
+    Req2 𝔸 (fmap' 𝔸 f M) := by
+  intro a c hcfresh hca
+  have hinf : (NominalSet.supp 𝔸 (M.val) ∪ NominalSet.supp 𝔸 (fmap' 𝔸 f M) ∪ {a})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · apply NominalSet.supp_finite
+      · apply NominalSet.supp_finite
+    · apply Set.finite_singleton
+  obtain ⟨d, hd⟩ := hinf.nonempty
+  simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+  have hdM : d # M.val := hd.left.left
+  have hdfmap : d # (fmap' 𝔸 f M) := hd.left.right
+  have hda : d ≠ a := hd.right
+  rw [choose_restriction' 𝔸 _ _ _ _ _ hcfresh hdfmap hca hda hca hda]
+  simp only [fmap', fmap'', PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+    PermSet.atom_swap, Equiv.swap_apply_left]
+  rw [← Function.equivariant 𝔸 f]
+  rw [← AlgebraMorphism.preserve_res]
+  rw [← AlgebraMorphism.preserve_join]
+  congr
+  suffices M.val.val a = (M.val.val a) ∨[𝔸] (d \ (⸨a,d⸩ • M.val).val a) by
+    simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
+      Equiv.swap_apply_left] at this
+    exact this
+  apply M.prop a d hdM hda
+
+def fmap (f : X → Y) [Function.Equivariant 𝔸 f] [AlgebraMorphism 𝔸 f] : StepModel 𝔸 X → StepModel 𝔸 Y :=
+  fun M ↦ ⟨fmap' 𝔸 f M, by apply fmap_req2⟩
+
+instance {f : X → Y} [Function.Equivariant 𝔸 f] [AlgebraMorphism 𝔸 f] : Function.Equivariant 𝔸 (fmap 𝔸 f) := by
+  constructor; intro x π
+  apply Subtype.eq; apply Subtype.eq
+  simp only [fmap, fmap', smul_val, PermSet.Finsupp.smul_val]
+  rw [← Function.equivariant]
+
+instance {f : X → Y} [Function.Equivariant 𝔸 f] [AlgebraMorphism 𝔸 f] : AlgebraMorphism 𝔸 (fmap 𝔸 f) where
+  preserve_bot := by
+    apply Subtype.eq; apply Subtype.eq; ext b
+    show f (⊥[𝔸]) = ⊥[𝔸]
+    exact AlgebraMorphism.preserve_bot
+  preserve_join x y :=  by
+    apply Subtype.eq; apply Subtype.eq; ext b
+    show f (x.val.val b ∨[𝔸] y.val.val b) = f (x.val.val b) ∨[𝔸] f (y.val.val b)
+    apply AlgebraMorphism.preserve_join
+  preserve_res a x := by
+    apply Subtype.eq; apply Subtype.eq; ext b
+    show f ((restrict 𝔸 (⟪a⟫ x)).val.val b) = (restrict 𝔸 (⟪a⟫ fmap 𝔸 f x)).val.val b
+    have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (fmap 𝔸 f x) ∪ {a} ∪ {b})ᶜ.Infinite := by
+      apply Set.Finite.infinite_compl
+      rw [Set.finite_union, Set.finite_union, Set.finite_union]
+      constructor
+      · constructor
+        · constructor
+          · apply NominalSet.supp_finite
+          · apply NominalSet.supp_finite
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    obtain ⟨d, hd⟩ := hinf.nonempty
+    simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+    have hdx : d # x := hd.left.left.left
+    have hdfmap : d # (fmap 𝔸 f x) := hd.left.left.right
+    have hda : d ≠ a := hd.left.right
+    have hdb : d ≠ b := hd.right
+    rw [restrict_eq 𝔸 _ hdx hda hdb]
+    rw [restrict_eq 𝔸 _ hdfmap hda hdb]
+    simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, fmap, fmap', fmap'']
+    rw [← Function.equivariant 𝔸 f]
+    apply AlgebraMorphism.preserve_res
+
 end StepModel
 
 private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T))