diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 264 |
1 files changed, 264 insertions, 0 deletions
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 |