restructure

1 files changed, 0 insertions, 363 deletions

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