import Mathlib import Nominal.Support import Nominal.Equivariance import Nominal.Category import Nominal.Permutations import Nominal.Instances.Basic import Nominal.Instances.Abstraction import Nominal.NameRestriction.Finsupp variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] -- M₀ algebra structure: Equivariant join semilattices with name restriction class AlgebraStructure (X : Type) [NominalSet 𝔸 X] where bot : Unit →ₑ[𝔸] X join : (X × X) →ₑ[𝔸] X res : NameAbstraction 𝔸 X →ₑ[𝔸] X ax_neutral : ∀ x, join (x, bot ()) = x ax_idempotent : ∀ x, join (x, x) = x ax_commutative : ∀ x y, join (x, y) = join (y, x) ax_associative : ∀ x y z, join (join (x, y), z) = join (x, join (y, z)) ax_fresh : ∀ a x, a # x → res (⟪a⟫ x) = x ax_swap : ∀ a b x, res (⟪a⟫ res (⟪b⟫ x)) = res (⟪b⟫ res (⟪a⟫ x)) ax_distributive : ∀ a x y, res (⟪a⟫ join (x, y)) = join (res (⟪a⟫ x), res (⟪a⟫ y)) ax_redundant : ∀ a x, x = join (x, res (⟪a⟫ x)) private abbrev AlgebraStructure.bot' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] := (AlgebraStructure.bot : Unit →ₑ[𝔸] X) private abbrev AlgebraStructure.join' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] := (AlgebraStructure.join : (X × X) →ₑ[𝔸] X) notation "⊥[" A "]" => AlgebraStructure.bot' A () notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y) infixl:60 " \\ " => fun a x => AlgebraStructure.res (⟪a⟫ x) namespace AlgebraStructure variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] lemma bot_supp : NominalSet.supp 𝔸 (⊥[𝔸] : X) = ∅ := by rw [← Set.subset_empty_iff] show NominalSet.supp 𝔸 ((bot' 𝔸).toFun ()) ⊆ ∅ grw [Function.Equivariant.supp_subset] simp lemma join_equivariant {x y : X} {π : FPerm 𝔸} : π • (x ∨[𝔸] y) = (π • x) ∨[𝔸] (π • y) := by show π • (join' 𝔸).toFun (x, y) = (join' 𝔸).toFun (π • (x, y)) rw [← Function.equivariant] lemma res_equivariant {a : 𝔸} {x : X} {π : FPerm 𝔸} : π • (a \ x) = (π • a) \ (π • x) := by show π • res.toFun (⟪a⟫ x) = res.toFun (π • (⟪a⟫ x)) rw [← Function.equivariant] end AlgebraStructure -- Base Model: M₀ X def BaseModel (X : Type) [NominalSet 𝔸 X] : Type := PermSet.FinSet 𝔸 X namespace BaseModel variable {X : Type} [NominalSet 𝔸 X] instance : NominalSet 𝔸 (BaseModel 𝔸 X) := PermSet.FinSet.instNominalSet 𝔸 instance : EmptyCollection (BaseModel 𝔸 X) := PermSet.FinSet.instEmptyCollection 𝔸 instance : Union (BaseModel 𝔸 X) := PermSet.FinSet.instUnion 𝔸 instance : Inter (BaseModel 𝔸 X) := PermSet.FinSet.instInter 𝔸 instance : SDiff (BaseModel 𝔸 X) := PermSet.FinSet.instSDiff 𝔸 @[simp] lemma empty_val : (∅ : BaseModel 𝔸 X).val = ∅ := rfl @[simp] lemma union_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl @[simp] lemma inter_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl @[simp] lemma sdiff_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ \ S₂).val = S₁.val \ S₂.val := rfl @[simp] lemma smul_val {L : BaseModel 𝔸 X} {π : FPerm 𝔸} : (π • L).val = π • L.val := rfl def bot : Unit → BaseModel 𝔸 X := fun _ ↦ ∅ instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → BaseModel 𝔸 X) := by constructor; intro _ π apply Subtype.eq; simp [bot] def union : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X := PermSet.FinSet.union 𝔸 instance : Function.Equivariant 𝔸 (union 𝔸 : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X) := PermSet.FinSet.instEquivariantProdUnion 𝔸 def restrict : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X := Quotient.lift (fun ⟨a, S⟩ ↦ ⟨{x ∈ S.val | a # x}, by apply Set.Finite.subset S.prop; simp⟩) (by intro ⟨a₁, S₁⟩ ⟨a₂, S₂⟩ haeq apply Subtype.eq simp only rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (BaseModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq cases haeq with | inl h => rw [h.left, h.right] | inr h => ext x; constructor · intro ⟨hx, ha₁⟩ have hx' : ⸨a₁, a₂⸩ • x ∈ S₂.val := by rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv] show x ∈ (⸨a₁, a₂⸩ • S₂).val rw [← h.right.right]; exact hx have ha₂ := h.right.left rw [PermSet.FinSet.fresh] at ha₂ specialize ha₂ (⸨a₁, a₂⸩ • x) hx' nth_rw 1 [show a₁ = ⸨a₁, a₂⸩ • a₂ by simp] at ha₂ rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] at ha₂ constructor · rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂] exact hx' · exact ha₂ · intro ⟨hx, ha₂⟩ have hx' : ⸨a₁, a₂⸩ • x ∈ S₁.val := by rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv] show x ∈ (⸨a₁, a₂⸩ • S₁).val rw [h.right.right, ← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul] exact hx have ha₁ := h.right.left rw [PermSet.FinSet.fresh] at ha₁ specialize ha₁ x hx rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂] at hx' rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul] at hx' exact ⟨hx', ha₁⟩) instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X) := by constructor apply Quotient.ind intro ⟨a, S⟩ π apply Subtype.eq simp only [restrict, NameAbstraction.smul, Quotient.lift_mk, smul_val] ext x; constructor · intro ⟨hx, hfresh⟩ rw [Set.mem_smul_set_iff_inv_smul_mem]; constructor · rw [← Set.mem_smul_set_iff_inv_smul_mem]; exact hx · rw [show a = π⁻¹ • π • a by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh] exact hfresh · rw [Set.mem_smul_set_iff_inv_smul_mem] intro ⟨hx, hfresh⟩; constructor · rw [Set.mem_smul_set_iff_inv_smul_mem]; exact hx · rw [show x = π • π⁻¹ • x by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh] exact hfresh lemma restrict_eq {a : 𝔸} {S : BaseModel 𝔸 X} : (restrict 𝔸 (⟪a⟫ S)).val = {x ∈ S.val | a # x} := rfl instance : AlgebraStructure 𝔸 (BaseModel 𝔸 X) where bot := ⟨bot 𝔸, inferInstance⟩ join := ⟨union 𝔸, inferInstance⟩ res := ⟨restrict 𝔸, inferInstance⟩ ax_neutral x := by apply Subtype.eq show x.val ∪ ∅ = x.val simp ax_idempotent x := by apply Subtype.eq show x.val ∪ x.val = x.val simp ax_commutative x y := by apply Subtype.eq show x.val ∪ y.val = y.val ∪ x.val apply Set.union_comm ax_associative x y z := by apply Subtype.eq show (x.val ∪ y.val) ∪ z.val = x.val ∪ (y.val ∪ z.val) apply Set.union_assoc ax_fresh a S := by intro hfresh show restrict 𝔸 (⟪a⟫ S) = S apply Subtype.eq rw [restrict_eq] rw [PermSet.FinSet.fresh] at hfresh ext x; constructor · intro ⟨hS, _⟩; exact hS · intro hS; exact ⟨hS, hfresh x hS⟩ ax_swap a b S := by show restrict 𝔸 (⟪a⟫ restrict 𝔸 (⟪b⟫ S)) = restrict 𝔸 (⟪b⟫ restrict 𝔸 (⟪a⟫ S)) apply Subtype.eq ext x simp only [restrict_eq, Set.mem_setOf_eq] ac_nf ax_distributive a S₁ S₂ := by show restrict 𝔸 (⟪a⟫ S₁ ∪ S₂) = restrict 𝔸 (⟪a⟫ S₁) ∪ restrict 𝔸 (⟪a⟫ S₂) apply Subtype.eq simp [restrict_eq] ax_redundant a S := by show S = S ∪ restrict 𝔸 (⟪a⟫ S) apply Subtype.eq; ext x simp only [union_val, restrict_eq, Set.mem_union, Set.mem_setOf_eq, iff_self_or, and_imp] intro h _; exact h @[simp] lemma bot_eq : (⊥[𝔸] : BaseModel 𝔸 X) = ∅ := rfl @[simp] lemma join_eq {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∨[𝔸] S₂) = S₁ ∪ S₂ := rfl @[simp] lemma res_eq {a : 𝔸} {S : BaseModel 𝔸 X} : (a \ S) = restrict 𝔸 (⟪a⟫ S) := rfl end BaseModel -- Step Model: \bar{M₁} X def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] := { f : PermSet.FinsuppFunction 𝔸 𝔸 X | ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) ∧ ∀ c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a) } def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type := permissibleFunctions 𝔸 X namespace StepModel variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by constructor; intro f π hf a simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] constructor · have hf₁ := (hf (π⁻¹ • a)).left rw [show NominalSet.supp 𝔸 (π • f) = π • NominalSet.supp 𝔸 f from Function.equivariant _ _ _ _] rw [show ({a} : Set 𝔸) = π • {π⁻¹ • a} by simp] rw [← Set.smul_set_union] rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)] exact hf₁ · intro c hcf hca have hf₂ := (hf (π⁻¹ • a)).right (π⁻¹ • c) specialize hf₂ (by rw [show f = π⁻¹ • π • f by simp] rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] exact hcf) specialize hf₂ (by intro hcontra have : π • π⁻¹ • c = π • π⁻¹ • a := by rw [hcontra] simp only [smul_inv_smul] at this exact hca this) nth_rw 1 [hf₂] rw [AlgebraStructure.join_equivariant, AlgebraStructure.res_equivariant] simp only [smul_inv_smul, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] suffices π • ⸨π⁻¹ • a,π⁻¹ • c⸩ • f.val (π⁻¹ • c) = ⸨a, c⸩ • π • f.val (π⁻¹ • c) by rw [this] rw [← MulAction.mul_smul, ← MulAction.mul_smul] suffices π * ⸨π⁻¹ • a,π⁻¹ • c⸩ = ⸨a,c⸩ * π by rw [this] rw [FPerm.mul_swap_eq_swap_mul, show π⁻¹ • a = π⁻¹ a from rfl, show π⁻¹ • c = π⁻¹ c from rfl] simp instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸 @[simp] lemma smul_val (π : FPerm 𝔸) (f : StepModel 𝔸 X) : (π • f).val = π • f.val := Subtype.smul_val 𝔸 π f instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X) := Subtype.instValEquivariant 𝔸 @[simp] lemma supp {f : StepModel 𝔸 X} : NominalSet.supp 𝔸 f = NominalSet.supp 𝔸 f.val := Subtype.supp 𝔸 @[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val := Subtype.fresh 𝔸 end StepModel