From e1ec8bf9ae213f329a21c25743a0afbd96d99630 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 21 Oct 2025 23:26:02 +0200 Subject: Restructure support_inter proof --- Nominal/Support.lean | 183 +++++++++++++++++++++++---------------------------- 1 file changed, 84 insertions(+), 99 deletions(-) (limited to 'Nominal') diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 7875ad3..6a1d4d9 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -50,115 +50,100 @@ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ /-- 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 + intro h_S_support h_S_finite h_T_support h_T_finite π h_π_fix + let π' := π.val + let h_π_fin := π.prop + + -- First we obtain an injection m : S \ T → (π'.supp ∪ S ∪ T)ᶜ. + have h_cod_inf : ((π'.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σ + simp; exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩ + have h_dom_fin : (S \ T).Finite := + Set.Finite.diff h_S_finite + + obtain ⟨m, ⟨h_m_preimage, h_m_injective⟩⟩ := + Set.Finite.exists_injOn_of_encard_le h_dom_fin (by + rw [Set.Infinite.encard_eq h_cod_inf, Set.Finite.encard_eq_coe h_dom_fin] + simp) + let m' := (S \ T).restrict m + rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective + obtain h_m_inv := Function.partialInv_of_injective h_m_injective + have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ := + Set.image_subset_iff.mpr h_m_preimage + + -- Show some trivial statements about subsets of (π'.supp ∪ S ∪ T), i.e. the atoms excluded from the image of m. + have h_sub_π : π'.supp ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_of_subset_left Set.subset_union_left T + have h_sub_S : S ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_of_subset_left Set.subset_union_right T + have h_sub_T : T ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_right + have h_sub_dom : (S \ T) ⊆ (π'.supp ∪ S ∪ T) := by trans; exact Set.diff_subset; exact h_sub_S + have h_m_image_notIn_sub {U : Set 𝔸} (h_sub_U : U ⊆ π'.supp ∪ S ∪ T) {a : 𝔸} (h_a_dom : a ∈ S \ T) : m a ∉ U := by + suffices m a ∈ (π'.supp ∪ S ∪ T)ᶜ by + exact Set.notMem_subset h_sub_U (h_m_preimage h_a_dom) + exact h_m_image (Set.mem_image_of_mem m h_a_dom) + + -- Next, extend m to a new permutation σ, about which we will then prove some properties. 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 + let σ' : 𝔸 → 𝔸 := fun a => + if h : a ∈ S \ T then m' ⟨a, h⟩ + else if let .some b := m'.partialInv a then b else a - have hselfinvτ : ∀ a, τ (τ a) = a := by + + -- First, σ is self-inverse and finitely supported, making it an element of FPerm 𝔸. + have h_σ_involutive : Function.Involutive σ' := 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 + · have h := Function.partialInv_left h_m_injective ⟨a, h₁⟩ + simp [σ', m', h₁, h_m_image_notIn_sub h_sub_dom h₁, h] at * + · cases h₂ : m'.partialInv a with + | some b => simp [σ', h₂, h₁]; rwa [← h_m_inv] + | none => simp [σ', h₂, h₁] + have h_σ_simple_case (a : 𝔸) (h₁ : a ∉ S \ T) (h₂ : a ∉ m '' (S \ T)) : σ' a = a := by + cases h : m'.partialInv a with + | some b => rw [h_m_inv] at h + have : a ∈ (m '' (S \ T)) := by rw [← h, Set.mem_image]; use b; simp [m'] + contradiction + | none => simp [σ', h₁, h] + have h_σ_fin : {a | σ' a ≠ a}.Finite := by apply Set.Finite.subset - · exact Set.finite_union.mpr ⟨h_dom_fin, Set.Finite.image σ h_dom_fin⟩ + · exact Set.finite_union.mpr ⟨h_dom_fin, Set.Finite.image m 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 + suffices σ' a = a by contradiction + apply h_σ_simple_case + · rw [← Set.mem_compl_iff]; exact ha₂.left + · exact Set.notMem_of_mem_diff ha₂ + let σ : FPerm 𝔸 := ⟨⟨σ', σ', h_σ_involutive, h_σ_involutive⟩, h_σ_fin⟩ + + -- Second, σ fixes T and σπσ fixes S. + have h_σ_fixT : σ ∈ fix 𝔸 T := by + intro a haT; show σ a = a + apply h_σ_simple_case + · exact Set.notMem_diff_of_mem haT + · exact fun h => h_m_image h (h_sub_T haT) + have h_σ_fixS : (σ * π * σ) ∈ 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 + σ (π (σ a)) = σ (π (σ • a)) := rfl + _ = σ (π a) := by rw [h_σ_fixT a haT] + _ = σ (π • a) := rfl + _ = σ a := by rw [h_π_fix a (Set.mem_inter haS haT)] + _ = σ • a := rfl + _ = a := by rw [h_σ_fixT a haT] + · suffices π (σ a) = σ a by rw [this]; exact h_σ_involutive a + apply Equiv.Perm.supp_notin + rw [show σ a = m a by simp [σ, σ', (Set.mem_diff_of_mem haS haT), m']] + exact h_m_image_notIn_sub h_sub_π (Set.mem_diff_of_mem haS haT) + + -- Using this carefully constructed σ, we can finally prove the statement. 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₁] + π • x = (1 * π * 1) • x := rfl + _ = ((σ * σ⁻¹) * π * (σ * σ⁻¹)) • x := by rw [@mul_inv_cancel] + _ = ((σ * σ * π * σ) * σ) • x := rfl + _ = (σ * σ * π * σ) • x := by rw [@mul_smul, h_T_support h_σ_fixT] + _ = (σ * (σ * π * σ)) • x := rfl + _ = σ • x := by rw [@mul_smul, h_S_support h_σ_fixS] + _ = x := by rw [h_T_support h_σ_fixT] /-- 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 -- cgit v1.3.1