import Mathlib.Tactic import Nominal.Permutations import Nominal.Helpers.Finset /-! # Basic Definitions This file provides basic definitions for nominal sets. -/ /-! ## (FPerm 𝔸)-Sets Sets equipped with a permutation operation. -/ section PermSet variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] /-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/ class PermSet (X : Type) extends MulAction (FPerm 𝔸) X /-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where smul π a := π a one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl /-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 (FPerm 𝔸) where smul π τ := π * τ one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl class DiscretePermSet (X : Type) extends PermSet 𝔸 X where is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x /-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/ def PermSet.discrete (X : Type) : DiscretePermSet 𝔸 X where smul π x := x one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl is_discrete := by intro _ _; rfl /-- We consider Unit a discrete (FPerm 𝔸)-Set. -/ instance : DiscretePermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit /-- We consider Bool a discrete (FPerm 𝔸)-Set. -/ instance : DiscretePermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool end PermSet /-! ## Support Definitions We can define the notion of "supports" on elements of (FPerm 𝔸)-Sets as the atoms which need to be left unchanged to also fix the element. -/ section Support variable (𝔸 : Type) {X : Type} [PermSet 𝔸 X] namespace PermSet /-- The permutations that leave an element x unchanged. -/ def fix' (x : X) : Set (FPerm 𝔸) := { π : FPerm 𝔸 | π • x = x } /-- The permutations that leave all elements in A unchanged. -/ def fix (A : Set X) : Set (FPerm 𝔸) := { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x } /-- A set S ⊆ 𝔸 is a support for x if every permutation that fixes S also leaves x unchanged. -/ def HasSupport (x : X) (S : Set 𝔸) : Prop := fix 𝔸 S ⊆ fix' 𝔸 x @[simp] lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by constructor · intro hsupp π hπ exact hsupp hπ · intro hsupp π hπ exact hsupp π hπ lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by intro hS hsub π hπ apply hS intro a ha exact hπ a (hsub ha) /-- For two finite supports, the intersection is also a support. -/ lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by intro hsuppS hfinS hsuppT hfinT π hfixπ have h_cod_inf : ((π.val.supp ∪ S ∪ T)ᶜ).Infinite := by apply Set.Finite.infinite_compl simp; exact ⟨⟨π.val_prop, hfinS⟩, hfinT⟩ have h_dom_fin : (S \ T).Finite := Set.Finite.diff hfinS have hle : (S \ T).encard ≤ ((π.val.supp ∪ S ∪ T)ᶜ).encard := by rw [Set.Infinite.encard_eq h_cod_inf, Set.Finite.encard_eq_coe h_dom_fin] simp obtain ⟨σ, ⟨hpreσ, hinjσ⟩⟩ := Set.Finite.exists_injOn_of_encard_le h_dom_fin hle have himσ {a : 𝔸} : a ∈ S \ T → σ a ∉ S \ T := by intro ha suffices : σ a ∈ (π.val.supp ∪ S ∪ T)ᶜ · have h : S \ T ⊆ π.val.supp ∪ S ∪ T := by calc S \ T ⊆ S := Set.diff_subset _ ⊆ π.val.supp ∪ S := Set.subset_union_right _ ⊆ π.val.supp ∪ S ∪ T := Set.subset_union_left exact Set.notMem_subset h (hpreσ ha) · rw [← Set.image_subset_iff] at hpreσ exact hpreσ (Set.mem_image_of_mem σ ha) have himσ' {a : 𝔸} : a ∈ S \ T → σ a ∉ π.val.supp := by intro ha suffices : σ a ∈ (π.val.supp ∪ S ∪ T)ᶜ · have h : π.val.supp ⊆ π.val.supp ∪ S ∪ T := by calc π.val.supp ⊆ π.val.supp ∪ S := Set.subset_union_left _ ⊆ π.val.supp ∪ S ∪ T := Set.subset_union_left exact Set.notMem_subset h (hpreσ ha) · rw [← Set.image_subset_iff] at hpreσ exact hpreσ (Set.mem_image_of_mem σ ha) rw [Set.injOn_iff_injective] at hinjσ obtain hσinv := Function.partialInv_of_injective hinjσ have {a : 𝔸} : Decidable (a ∈ S \ T) := Classical.propDecidable (a ∈ S \ T) let τ : 𝔸 → 𝔸 := fun a => if h : a ∈ S \ T then (S \ T).restrict σ ⟨a, h⟩ else if let .some b := ((S \ T).restrict σ).partialInv a then b else a have hselfinvτ : ∀ a, τ (τ a) = a := by intro a by_cases h₁ : a ∈ S \ T · have h₂ : ((S \ T).restrict σ).partialInv (((S \ T).restrict σ) ⟨a, h₁⟩) = .some ⟨a, h₁⟩ := Function.partialInv_left hinjσ ⟨a, h₁⟩ simp at h₂ simp [τ, h₁, himσ h₁, h₂] · cases h₂ : ((S \ T).restrict σ).partialInv a with | some b => simp [τ, h₂, h₁] rwa [← Set.restrict_apply σ (S \ T) b, ← hσinv] | none => simp [τ, h₂, h₁] have hfinsuppτ : {a | τ a ≠ a}.Finite := by apply Set.Finite.subset · exact Set.finite_union.mpr ⟨h_dom_fin, Set.Finite.image σ h_dom_fin⟩ · intro a ha₁; by_contra ha₂ rw [← Set.mem_compl_iff, Set.compl_union, Set.mem_inter_iff] at ha₂ suffices τ a = a by contradiction have ha₃ : a ∉ S \ T := by rw [← Set.mem_compl_iff]; exact ha₂.left cases ha₄ : ((S \ T).restrict σ).partialInv a with | some b => rw [hσinv, Set.restrict_apply] at ha₄ have : a ∈ (σ '' (S \ T)) := by rw [← ha₄, Set.mem_image]; use b; simp have : a ∉ (σ '' (S \ T)) := Set.notMem_of_mem_diff ha₂ contradiction | none => simp [τ, ha₃, ha₄] let τ' : FPerm 𝔸 := ⟨⟨τ, τ, hselfinvτ, hselfinvτ⟩, hfinsuppτ⟩ have h₁ : τ' ∈ fix 𝔸 T := by intro a haT; show τ a = a have ha₁ : a ∉ S \ T := Set.notMem_diff_of_mem haT have h₁ : σ '' (S \ T) ⊆ (π.val.supp ∪ S ∪ T)ᶜ := by rwa [Set.image_subset_iff] have h₂ : a ∉ (π.val.supp ∪ S ∪ T)ᶜ := by rw [Set.notMem_compl_iff] apply Set.mem_union_right; assumption cases ha₂ : ((S \ T).restrict σ).partialInv a with | some b => rw [hσinv, Set.restrict_apply] at ha₂ have : a ∈ (σ '' (S \ T)) := by rw [← ha₂, Set.mem_image]; use b; simp have : a ∉ (σ '' (S \ T)) := fun x => h₂ (h₁ x) contradiction | none => simp [τ, ha₁, ha₂] have h₂ : (τ' * π * τ') ∈ fix 𝔸 S := by intro a haS; show τ (π (τ a)) = a by_cases haT : a ∈ T · have ht : τ a = a := by -- XXX: copied from above have ha₁ : a ∉ S \ T := Set.notMem_diff_of_mem haT have h₁ : σ '' (S \ T) ⊆ (π.val.supp ∪ S ∪ T)ᶜ := by rwa [Set.image_subset_iff] have h₂ : a ∉ (π.val.supp ∪ S ∪ T)ᶜ := by rw [Set.notMem_compl_iff] apply Set.mem_union_right; assumption cases ha₂ : ((S \ T).restrict σ).partialInv a with | some b => rw [hσinv, Set.restrict_apply] at ha₂ have : a ∈ (σ '' (S \ T)) := by rw [← ha₂, Set.mem_image]; use b; simp have : a ∉ (σ '' (S \ T)) := fun x => h₂ (h₁ x) contradiction | none => simp [τ, ha₁, ha₂] calc τ (π (τ a)) = τ (π a) := by rw [ht] _ = τ (π • a) := rfl _ = τ a := by rw [hfixπ a (Set.mem_inter haS haT)] _ = a := by rw [ht] · have h₁ : a ∈ S \ T := Set.mem_diff_of_mem haS haT have h₂ : π (τ a) = τ a := by apply Equiv.Perm.supp_notin rw [show τ a = σ a by simp [τ, h₁]] exact himσ' h₁ rw [h₂] exact hselfinvτ a calc π • x = (1 * π * 1) • x := rfl _ = ((τ' * τ'⁻¹) * π * (τ' * τ'⁻¹)) • x := by rw [@mul_inv_cancel] _ = ((τ' * τ' * π * τ') * τ') • x := rfl _ = (τ' * τ' * π * τ') • x := by rw [@mul_smul, hsuppT h₁] _ = (τ' * (τ' * π * τ')) • x := rfl _ = τ' • x := by rw [@mul_smul, hsuppS h₂] _ = x := by rw [hsuppT h₁] /-- For a finite number of finite supports, the intersection is also a support. -/ lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite · intro hfin rw [show C = hfin.toFinset.toSet by simp] intro hne h exact (this hfin.toFinset hne h).left · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸) apply Finset.Nonempty.induction · intro S hS rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp] apply hS simp · intro S C' hS hC' hsing rw [Finset.coe_insert S C', Set.sInter_insert S ↑C'] have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by intro S' hS' apply hsing exact Finset.mem_insert_of_mem hS' specialize hC' hother specialize hsing S (by simp) constructor · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right · apply Set.Finite.inter_of_left exact hsing.right end PermSet end Support /-! ## Basic Nominal Set Definition Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely supported. -/ section NominalSet variable (𝔸 : Type) /-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/ class NominalSet (X : Type) extends PermSet 𝔸 X where finsupp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite namespace NominalSet variable {X : Type} [nom : NominalSet 𝔸 X] /-- For every element x of a nominal set, there exists a least finite support, denoted "supp x". --/ def supp (x : X) : Set 𝔸 := ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S ∧ S.Finite } /-- The least finite support in a nominal set is always finite. -/ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by unfold supp obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x apply Set.Finite.subset · exact hfinS · grind /-- The least finite support is itself a support. -/ lemma supp_is_support [Infinite 𝔸] {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by unfold supp; ext a constructor · intro h T hT apply h exact hT.out.right · intro h T hT suffices : a ∈ S ∩ T · apply Set.mem_of_mem_inter_right; assumption · apply h constructor · exact Set.inter_subset_left · constructor · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right · apply Set.Finite.inter_of_left; assumption rw [suppf] apply PermSet.support_sInter · apply Set.Finite.subset · apply Set.Finite.powerset exact hfinS · intro T hT exact hT.out.left · use S exact ⟨by rfl, ⟨hsuppS, hfinS⟩⟩ · intro T hT exact hT.right lemma support_subset_supp {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x ⊆ S := by intro hsupp hfin apply Set.sInter_subset_of_mem exact ⟨hsupp, hfin⟩ end NominalSet private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by simp [PermSet.fix'] /-- The set of atoms is a nominal set, where supp a = {a}. -/ instance : NominalSet 𝔸 𝔸 where finsupp := by intro a use {a} constructor · exact NominalSet.supp_atoms' 𝔸 · simp lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by ext b; constructor · apply support_subset_supp · apply NominalSet.supp_atoms' · simp · suffices : a ∈ supp 𝔸 a · simp; intro h; rw [h]; assumption · intro S ⟨hsuppS, hfinS⟩ by_contra ha obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset) simp at hc have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by intro d hd rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl] apply Equiv.Perm.supp_notin simp [Equiv.Perm.supp_swap, Ne.symm hc.left] exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ have ha₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] have ha₂ : ⸨a, c⸩ • a = a := by specialize hsuppS hfix simpa [PermSet.fix'] rw [ha₁] at ha₂ exact hc.left ha₂ class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X private lemma NominalSet.supp_discrete' {X : Type} [disc : DiscretePermSet 𝔸 X] {x : X} : PermSet.HasSupport 𝔸 x ∅ := by intro π hπ simp [PermSet.fix'] exact DiscretePermSet.is_discrete x π /-- Every set can be made into a discrete nominal set where every element has empty support. -/ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X := { PermSet.discrete 𝔸 X with finsupp := by intro x use {} constructor · intro π hπ; simp [PermSet.fix']; rfl · simp } lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by rw [← Set.subset_empty_iff] apply Set.sInter_subset_of_mem exact ⟨NominalSet.supp_discrete' 𝔸, Set.finite_empty⟩ /-- We consider Unit a discrete nominal set. -/ instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit /-- We consider Bool a discrete nominal set. -/ instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool end NominalSet