very rough draft for support_inter

1 files changed, 115 insertions, 9 deletions

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index dde26fc..66f43b1 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -86,14 +86,120 @@ lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T
   intro a ha
   exact hπ a (hsub ha)
 
-#check Set.Finite.exists_injOn_of_encard_le
-#check Set.injOn_iff_injective
-#check Function.partialInv_of_injective
-
-lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
-  sorry
+/-- 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₁]
 
-lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
+/-- 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]
@@ -106,7 +212,7 @@ lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (
       apply hS
       simp
     · intro S C' hS hC' hsing
-      rw [show (⋂₀ (insert S C' : Finset (Set 𝔸))) = S ∩ (⋂₀ C') by aesop]
+      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
@@ -152,7 +258,7 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
   · grind
 
 /-- The least finite support is itself a support. -/
-lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
+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