name restrictionsname-restriction-model

1 files changed, 302 insertions, 11 deletions

diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index 3df5999..6cac016 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -1280,32 +1280,24 @@ noncomputable instance : Depth1AlgebraStructure 𝔸 (StepModel 𝔸 X) X where
       rw [abs_eq 𝔸 c hcres hca hcb]
       nth_rw 2 [← show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
       rw [← AlgebraStructure.res_equivariant]
-      rw [← MulAction.mul_smul]
-      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
-      rw [MulAction.mul_smul]
       rw [AlgebraStructure.res_self]
-      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
       rw [restrict_eq 𝔸 c hcabs hcb hcb]
       simp only [PermSet.atom_swap, Equiv.swap_apply_left, PermSet.Finsupp.smul_val,
         PermSet.smul_function, FPerm.swap_inv]
-      nth_rw 1 [← show ⸨b, c⸩ • b = c by simp]
+      nth_rw 3 [← show ⸨b, c⸩ • b = c by simp]
       rw [← AlgebraStructure.res_equivariant]
       rw [abs_eq 𝔸 d hdx hda hdc]
       nth_rw 4 [← show ⸨c, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)]
       rw [← AlgebraStructure.res_equivariant]
-      nth_rw 3 [← show ⸨a, d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca (Ne.symm hdc)]
+      nth_rw 5 [← show ⸨a, d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca (Ne.symm hdc)]
       rw [← AlgebraStructure.res_equivariant]
       rw [show (c \ x) = x from AlgebraStructure.ax_fresh c x hcx]
       nth_rw 4 [← show ⸨a, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hdb)]
       rw [← AlgebraStructure.res_equivariant]
-      nth_rw 2 [← MulAction.mul_smul]
+      nth_rw 3 [← MulAction.mul_smul]
       rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)]
       rw [MulAction.mul_smul]
       rw [NominalSet.fresh_swap_fix 𝔸 hcres hdres]
-      rw [← MulAction.mul_smul]
-      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
-      rw [MulAction.mul_smul]
-      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
     · rw [restrict_fresh 𝔸 _ _ _ (Ne.symm heq)]
       have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (b \ x) ∪ {a} ∪ {b} ∪ {l})ᶜ.Infinite := by
         apply Set.Finite.infinite_compl
@@ -1441,6 +1433,305 @@ instance {f : X → Y} [Function.Equivariant 𝔸 f] [AlgebraMorphism 𝔸 f] :
 
 end StepModel
 
+namespace ActualBase
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+private def restrict' : (X × Set 𝔸) → Set X :=
+  fun (x, N) ↦ {π • x | π ∈ PermSet.fix 𝔸 N}
+
+instance : Function.Equivariant 𝔸 (restrict' 𝔸 : (X × Set 𝔸) → Set X) := by
+  constructor; intro x π
+  ext y; rw [restrict', restrict']; constructor
+  · intro ⟨τ, hτ, hy⟩
+    rw [Set.mem_smul_set]
+    simp only [Prod.smul_fst] at hy
+    use (π⁻¹ • τ • π • x.fst); constructor
+    · use (π⁻¹ * τ * π); constructor
+      · simp only [PermSet.fix, Prod.smul_snd, Set.mem_setOf_eq] at hτ
+        simp only [PermSet.fix, Set.mem_setOf_eq, MulAction.mul_smul]
+        intro a ha
+        specialize hτ (π • a) (by rw [@Set.smul_mem_smul_set_iff]; exact ha)
+        rw [hτ, inv_smul_eq_iff]
+      · simp [MulAction.mul_smul]
+    · rw [smul_inv_smul]; exact hy
+  · intro hy
+    rw [show y = π • π⁻¹ • y by simp] at hy
+    rw [Set.smul_mem_smul_set_iff] at hy
+    obtain ⟨τ, hτ, hy⟩ := hy
+    use π * τ * π⁻¹;constructor
+    · intro a ha
+      simp only [mul_smul]
+      rw [show a = π • π⁻¹ • a by simp] at ha
+      simp only [Prod.smul_snd, Set.smul_mem_smul_set_iff] at ha
+      specialize hτ (π⁻¹ • a) ha
+      rw [hτ]
+      simp
+    · simp only [Prod.smul_fst, mul_smul, inv_smul_smul]
+      rw [hy]
+      simp
+
+def Restriction (X : Type) [NominalSet 𝔸 X] : Type :=
+  {xN : Set X // ∃ x N, N ⊆ NominalSet.supp 𝔸 x ∧ xN = restrict' 𝔸 (x, N)}
+
+def restrict (x : X) (N : Set 𝔸) (hN : N ⊆ NominalSet.supp 𝔸 x) : Restriction 𝔸 X :=
+  ⟨restrict' 𝔸 (x, N), by use x, N⟩
+
+lemma restrict_ind (xN : Restriction 𝔸 X) : ∃ x N hN, xN = restrict 𝔸 x N hN := by
+  obtain ⟨x, N, ⟨h₁, h₂⟩⟩ := xN.prop
+  use x, N, h₁
+  apply Subtype.eq
+  exact h₂
+
+instance : PermSet 𝔸 (Restriction 𝔸 X) where
+  smul π xN := ⟨π • xN.val, by
+    obtain ⟨x, N, ⟨h₁, h₂⟩⟩ := xN.prop
+    use (π • x), (π • N); constructor
+    · rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)]
+      show (π • N).Subset (π • NominalSet.supp 𝔸 x)
+      rw [← Rel.equivariant 𝔸 Set.Subset]
+      exact h₁
+    · rw [h₂, ← Function.equivariant 𝔸, Prod.smul_mk]⟩
+  one_smul xN := by
+    apply Subtype.eq
+    show 1 • xN.val = xN.val
+    apply MulAction.one_smul
+  mul_smul π τ xN := by
+    apply Subtype.eq
+    show (π * τ) • xN.val = π • τ • xN.val
+    apply MulAction.mul_smul
+
+
+lemma fix_inverse (π : FPerm 𝔸) (S : Set 𝔸) : π ∈ PermSet.fix 𝔸 S → π⁻¹ ∈ PermSet.fix 𝔸 S := by
+  intro hπ a ha
+  rw [← hπ a ha, inv_smul_smul, hπ a ha]
+
+lemma fix_set_support (N : Set 𝔸) : PermSet.HasSupport 𝔸 N N := by
+  intro π hπ
+  ext a
+  rw [Set.mem_smul_set_iff_inv_smul_mem]
+  constructor
+  · intro ha
+    rw [show a = π • π⁻¹ • a by simp, hπ _ ha]
+    exact ha
+  · intro ha
+    rw [← hπ _ ha]
+    simp [ha]
+
+@[simp] lemma smul_restriction_val (π : FPerm 𝔸) (xN : Restriction 𝔸 X) : (π • xN).val = π • xN.val := rfl
+
+@[simp] lemma smul_restrict (π : FPerm 𝔸) (x : X) (N : Set 𝔸) (hN : N ⊆ NominalSet.supp 𝔸 x) :
+    π • (restrict 𝔸 x N hN) = restrict 𝔸 (π • x) (π • N) (by
+      rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)]
+      show (π • N).Subset (π • NominalSet.supp 𝔸 x)
+      rw [← Rel.equivariant 𝔸 Set.Subset]
+      exact hN) := by
+  apply Subtype.eq
+  simp only [restrict, smul_restriction_val]
+  rw [← Function.equivariant]
+  simp
+
+private lemma restrict_supp' {x : X} {N : Set 𝔸} {hN : N ⊆ NominalSet.supp 𝔸 x} :
+    PermSet.HasSupport 𝔸 (restrict 𝔸 x N hN) N := by
+  intro π hπ
+  apply Subtype.eq
+  simp only [smul_restriction_val, restrict]
+  rw [← Function.equivariant, Prod.smul_mk, fix_set_support 𝔸 N hπ]
+  ext y; constructor
+  · intro ⟨τ, hτ, hy⟩
+    use τ * π; constructor
+    · intro a ha; rw [MulAction.mul_smul, hπ _ ha, hτ _ ha]
+    · rw [MulAction.mul_smul, hy]
+  · intro ⟨τ, hτ, hy⟩
+    use τ * π⁻¹; constructor
+    · intro a ha
+      rw [MulAction.mul_smul, fix_inverse 𝔸 π N hπ a ha, hτ _ ha]
+    · rw [MulAction.mul_smul, inv_smul_smul, hy]
+
+instance : NominalSet 𝔸 (Restriction 𝔸 X) where
+  fin_supp xN := by
+    obtain ⟨x, N, hN, h⟩ := restrict_ind 𝔸 xN; rw [h]
+    use N; constructor
+    · apply restrict_supp'
+    · apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hN
+
+lemma restrict_supp (x : X) (N : Set 𝔸) (hN : N ⊆ NominalSet.supp 𝔸 x) :
+    NominalSet.supp 𝔸 (restrict 𝔸 x N hN) = N := by
+  ext a; constructor
+  · apply NominalSet.support_subset_supp 𝔸
+    · exact restrict_supp' 𝔸
+    · apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hN
+  · intro ha
+    suffices ¬(PermSet.HasSupport 𝔸 (restrict 𝔸 x N hN) (N \ {a})) by
+      by_contra h
+      have hcontra : PermSet.HasSupport 𝔸 (restrict 𝔸 x N hN) (N \ {a}) := by
+        intro π hπ
+        apply NominalSet.supp_is_support
+        apply PermSet.fix_antitone_mem 𝔸 hπ
+        rw [Eq.symm (Set.diff_singleton_eq_self h)]
+        apply Set.diff_subset_diff_left
+        exact NominalSet.support_subset_supp 𝔸 (restrict_supp' 𝔸) (Set.Finite.subset (NominalSet.supp_finite 𝔸) hN)
+      contradiction
+    intro hsupp
+    have hinf : (NominalSet.supp 𝔸 x ∪ {a})ᶜ.Infinite := by
+      apply Set.Finite.infinite_compl
+      rw [Set.finite_union]
+      constructor
+      · apply NominalSet.supp_finite
+      · apply Set.finite_singleton
+    obtain ⟨b, hb⟩ := hinf.nonempty
+    simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hb
+    have hbfresh : b # x := hb.left
+    have hba : b ≠ a := hb.right
+    have heq : ⸨a,b⸩ • restrict 𝔸 x N hN = restrict 𝔸 x N hN := by
+      apply hsupp
+      intro c hc
+      simp only [Set.mem_diff, Set.mem_singleton_iff] at hc
+      apply FPerm.swap_apply_of_ne_of_ne
+      · exact hc.right
+      · intro hcontra; rw [← hcontra] at hbfresh
+        have : c ∈ NominalSet.supp 𝔸 x := hN hc.left
+        contradiction
+    rw [Subtype.eq_iff, restrict] at heq
+    simp only [smul_restriction_val] at heq
+    have hx : x ∈ restrict' 𝔸 (x, N) := by
+      use 1; constructor
+      · intro a _; apply MulAction.one_smul
+      · apply MulAction.one_smul
+    rw [← heq, ← Function.equivariant, Prod.smul_mk] at hx
+    obtain ⟨π, hπ, hx⟩ := hx
+    have hsuppeq : π • ⸨a,b⸩ • NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x := by
+      nth_rw 2 [← hx]
+      rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)]
+      rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)]
+    have hπb : π • b = b := by
+      apply hπ
+      rw [← PermSet.atom_set_swap_left]
+      exact ha
+    have hcontra : b ∈ π • ⸨a,b⸩ • NominalSet.supp 𝔸 x := by
+      rw [Set.mem_smul_set_iff_inv_smul_mem]
+      nth_rw 2 [← hπb]
+      rw [inv_smul_smul]
+      rw [← PermSet.atom_set_swap_left]
+      apply hN
+      exact ha
+    rw [hsuppeq] at hcontra
+    contradiction
+
+lemma restrict_eq {x x' : X} {N N' : Set 𝔸} {hN : N ⊆ NominalSet.supp 𝔸 x} {hN' : N' ⊆ NominalSet.supp 𝔸 x'} :
+    restrict 𝔸 x N hN = restrict 𝔸 x' N' hN' ↔
+    N = N' ∧ ∃ π ∈ PermSet.fix 𝔸 N, x' = π • x := by
+  constructor
+  · intro heq
+    constructor
+    · rw [← restrict_supp 𝔸 x N hN]
+      rw [← restrict_supp 𝔸 x' N' hN']
+      rw [heq]
+    · rw [Subtype.eq_iff] at heq
+      simp only [restrict] at heq
+      have hx' : x' ∈ restrict' 𝔸 (x', N') := by
+        use 1; constructor
+        · intro a _; apply MulAction.one_smul
+        · apply MulAction.one_smul
+      rw [← heq] at hx'
+      obtain ⟨π, heq⟩ := hx'
+      use π; constructor
+      · exact heq.left
+      · rw [heq.right]
+  · intro ⟨hNeq, ⟨π, hπ, hxeq⟩⟩
+    rw [← show π • restrict 𝔸 x N hN = restrict 𝔸 x N hN by
+      apply NominalSet.supp_is_support
+      rw [restrict_supp]; exact hπ]
+    apply Subtype.eq
+    simp only [restrict, smul_restriction_val, ← Function.equivariant, Prod.smul_mk]
+    rw [fix_set_support 𝔸 N hπ]
+    rw [hxeq, hNeq]
+
+noncomputable def Restriction.lift {Y : Type} (f : (x : X) → (N : Set 𝔸) → (hN : N ⊆ NominalSet.supp 𝔸 x) → Y) :
+    (∀ (x : X) (N : Set 𝔸) (hN : N ⊆ NominalSet.supp 𝔸 x) π hπ,
+      N = N' → π ∈ PermSet.fix 𝔸 N → f x N hN = f (π • x) N hπ) →
+    Restriction 𝔸 X → Y :=
+  fun _ res ↦
+    let x := Classical.choose res.prop
+    let hx := Classical.choose_spec res.prop
+    let N := Classical.choose hx
+    let hN := Classical.choose_spec hx
+    f x N hN.left
+
+end ActualBase
+
+def Req3 {X : Type} [NominalSet 𝔸 X] (S : PermSet.FinSet 𝔸 (ActualBase.Restriction 𝔸 X)) :=
+  ∀ x N hN N',
+    ActualBase.restrict 𝔸 x N hN ∈ S.val →
+    (hN' : N' ⊆ N) →
+    ActualBase.restrict 𝔸 x N' (by trans; exact hN'; exact hN) ∈ S.val
+
+def permissibleRestrictions (X : Type) [NominalSet 𝔸 X] :=
+  { S : PermSet.FinSet 𝔸 (ActualBase.Restriction 𝔸 X) | Req3 𝔸 S }
+
+def ActualBase (X : Type) [NominalSet 𝔸 X] : Type := permissibleRestrictions 𝔸 X
+
+namespace ActualBase
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+private lemma permissibleRestrictions_req3
+    (S : PermSet.FinSet 𝔸 (Restriction 𝔸 X)) (π : FPerm 𝔸) : Req3 𝔸 S → Req3 𝔸 (π • S) := by
+  intro hS x N hN N' h hN'
+  rw [PermSet.FinSet.smul_val, Set.mem_smul_set_iff_inv_smul_mem, smul_restrict] at h
+  specialize hS (π⁻¹ • x) (π⁻¹ • N) (by
+    rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)]
+    show (π⁻¹ • N).Subset (π⁻¹ • NominalSet.supp 𝔸 x)
+    rw [← Rel.equivariant 𝔸 (Set.Subset)]
+    exact hN) (π⁻¹ • N')
+  specialize hS h (by
+    show (π⁻¹ • N').Subset (π⁻¹ • N)
+    rw [← Rel.equivariant 𝔸 (Set.Subset)]
+    exact hN')
+  rw [PermSet.FinSet.smul_val, Set.mem_smul_set_iff_inv_smul_mem, smul_restrict]
+  exact hS
+
+instance : Set.Equivariant 𝔸 (permissibleRestrictions 𝔸 X) := by
+  constructor; exact permissibleRestrictions_req3 𝔸
+
+instance : NominalSet 𝔸 (ActualBase 𝔸 X) := Subtype.instNominalSetElem 𝔸
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (S : ActualBase 𝔸 X) : (π • S).val = π • S.val :=
+  Subtype.smul_val 𝔸 π S
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : ActualBase 𝔸 X → PermSet.FinSet 𝔸 (Restriction 𝔸 X)) :=
+  Subtype.instValEquivariant 𝔸
+
+@[simp] lemma supp {S : ActualBase 𝔸 X} : NominalSet.supp 𝔸 S = NominalSet.supp 𝔸 S.val :=
+  Subtype.supp 𝔸
+
+@[simp] lemma fresh {a : 𝔸} {S : ActualBase 𝔸 X} : a # S ↔ a # S.val :=
+  Subtype.fresh 𝔸
+
+def bot : Unit → ActualBase 𝔸 X :=
+  fun _ ↦ ⟨∅, by
+    intro _ _ _ _ h _
+    contradiction⟩
+
+instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → ActualBase 𝔸 X) := by
+  constructor; intro _ π
+  apply Subtype.eq; apply Subtype.eq; simp [bot]
+
+def union : (ActualBase 𝔸 X × ActualBase 𝔸 X) → ActualBase 𝔸 X :=
+  fun (S₁, S₂) ↦ ⟨S₁.val ∪ S₂.val, by
+    intro x N hN N' hmem hN'
+    simp only [PermSet.FinSet.union_val, Set.mem_union] at hmem
+    simp only [PermSet.FinSet.union_val, Set.mem_union]
+    cases hmem with
+    | inl h => left; exact S₁.prop x N hN N' h hN'
+    | inr h => right; exact S₂.prop x N hN N' h hN'⟩
+
+instance : Function.Equivariant 𝔸 (union 𝔸 : (ActualBase 𝔸 X × ActualBase 𝔸 X) → ActualBase 𝔸 X) := by
+  constructor; intro (S₁, S₂) π
+  apply Subtype.eq; simp [union]
+
+end ActualBase
+
 private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T))
 | 0 => ⟨BaseModel 𝔸 X, inferInstance, inferInstance⟩
 | n + 1 =>