From e2bde40a31e0ab0fea7e412bd2f9b03edcc026dd Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 21 Oct 2025 21:45:34 +0200 Subject: restructure --- Nominal/Basic.lean | 363 ---------------------------------------------- Nominal/Instances.lean | 91 ++++++++++++ Nominal/Permutations.lean | 40 ++++- Nominal/Support.lean | 264 +++++++++++++++++++++++++++++++++ 4 files changed, 387 insertions(+), 371 deletions(-) delete mode 100644 Nominal/Basic.lean create mode 100644 Nominal/Instances.lean create mode 100644 Nominal/Support.lean diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean deleted file mode 100644 index 66f43b1..0000000 --- a/Nominal/Basic.lean +++ /dev/null @@ -1,363 +0,0 @@ -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 diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean new file mode 100644 index 0000000..793baa4 --- /dev/null +++ b/Nominal/Instances.lean @@ -0,0 +1,91 @@ +import Nominal.Permutations +import Nominal.Support + +/-! +# Instances + +This file contains common instances of (FPerm 𝔸)-sets and nominal sets. +-/ + +variable (𝔸 : Type) + +/-! +## Atoms + +The set 𝔸 of atoms itself is a nominal set, where supp a = {a}. +-/ +section Atoms + +private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by + simp [PermSet.HasSupport, PermSet.fix, PermSet.fix'] + +instance : NominalSet 𝔸 𝔸 where + fin_supp := 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₂ + +end Atoms + +/-! +## Discrete Nominal Sets + +Every set can be made into a discrete nominal set, where supp x = ∅. +-/ +section Discrete + +def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where + smul π x := x + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl + is_discrete := by intro _ _; rfl + fin_supp := 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 + constructor + · intro π hπ + simp [PermSet.fix'] + exact DiscreteNominalSet.is_discrete x π + · exact 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 Discrete diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 5f62ec0..6819c67 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -103,15 +103,14 @@ namespace Equiv.Perm /-- The support of a transposition (x y). -/ lemma supp_swap {x y : X} : (Equiv.swap x y).supp = if x ≠ y then {x, y} else ∅ := by - if h : (x ≠ y) then - ext z + by_cases h : x = y + · simp [h, supp] + · simp [h]; ext z by_cases hx : z = x - · aesop + · simp [hx, Ne.symm h] · by_cases hy : z = y - · simp [hy] + · simp [hy, h] · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy] - else - aesop end Equiv.Perm @@ -120,8 +119,7 @@ namespace FPerm def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by apply Set.Finite.subset · apply ({x, y} : Finset X).finite_toSet - · simp [Equiv.Perm.supp_swap] - aesop⟩ + · by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]⟩ notation "⸨" a "," b "⸩" => FPerm.swap a b @@ -130,3 +128,29 @@ end FPerm example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩ end Transposition + +/-! +## (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 + +end PermSet diff --git a/Nominal/Support.lean b/Nominal/Support.lean new file mode 100644 index 0000000..7875ad3 --- /dev/null +++ b/Nominal/Support.lean @@ -0,0 +1,264 @@ +import Mathlib.Tactic +import Nominal.Permutations +import Nominal.Helpers.Finset + +/-! +# Support + +This file provides basic definitions for support of (FPerm 𝔸)-sets and nominal sets. +-/ + +variable (𝔸 : Type) + +/-! +## 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 {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 + +/-- Alternative definition with fix 𝔸 S unfolded. -/ +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π + +/-- If a support is a subset of another set, that set is also a support. -/ +lemma support_superset {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 + +/-! +## Nominal Sets + +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 + fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite + +/-- A discrete nominal set where permutations do not change anything. -/ +class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X where + is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x + +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.fin_supp 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.fin_supp 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 + +/-- If S is a finite support for x, then supp x is a subset of it. -/ +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 + +end NominalSet -- cgit v1.3.1