From 0b7c12eb301fe701e92ac02e5f6e6f92a8ededec Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 21 Oct 2025 00:00:50 +0200 Subject: add some proofs about specific least supports --- Nominal/Permutations.lean | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'Nominal/Permutations.lean') diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 40f0f13..5f62ec0 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -29,6 +29,11 @@ def supp (π : Equiv.Perm X) : Set X := @[simp] theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by rfl +/-- If an element does not occur in the support, the permutation doesn't move it. -/ +lemma supp_notin {π : Equiv.Perm X} {x : X} : x ∉ π.supp → π x = x := by + rw [show (π x = x) ↔ ¬(π x ≠ x) by simp] + simp [← (mem_supp π x).not] + /-- The support of the identity function is the empty set. -/ lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by rw [Set.eq_empty_iff_forall_notMem] @@ -92,14 +97,12 @@ Transpositions are a special case of finite permutations, where only (at most) t -/ section Transposition -notation "⸨" a "," b "⸩" => Equiv.swap a b - variable {X : Type} [DecidableEq X] namespace Equiv.Perm /-- The support of a transposition (x y). -/ -lemma supp_swap{x y : X} : ⸨x, y⸩.supp = if x ≠ y then {x, y} else ∅ := by +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 hx : z = x @@ -114,14 +117,16 @@ end Equiv.Perm namespace FPerm -lemma mem_swap {x y : X} : ⸨x, y⸩ ∈ FPerm X := by +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 + aesop⟩ + +notation "⸨" a "," b "⸩" => FPerm.swap a b end FPerm -example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [FPerm.mem_swap, FPerm.mem_mul]⟩ +example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩ end Transposition -- cgit v1.3.1