diff options
| -rw-r--r-- | Nominal.lean | 1 | ||||
| -rw-r--r-- | Nominal/Basic.lean | 202 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 127 |
3 files changed, 227 insertions, 103 deletions
diff --git a/Nominal.lean b/Nominal.lean index a3f0848..c94bb05 100644 --- a/Nominal.lean +++ b/Nominal.lean @@ -1,3 +1,4 @@ -- This module serves as the root of the `Nominal` library. -- Import modules here that should be built as part of the library. +import Nominal.Permutations import Nominal.Basic diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean index 534759d..eb10b44 100644 --- a/Nominal/Basic.lean +++ b/Nominal/Basic.lean @@ -1,123 +1,125 @@ import Mathlib.Tactic +import Nominal.Permutations +/-! +# Basic Definitions -section Permutations +This file provides basic definitions for nominal sets. +-/ -variable {X : Type} +/-! +## (FPerm 𝔸)-Sets -notation "⸨" a "," b "⸩" => Equiv.swap a b +Sets equipped with a permutation operation. +-/ +section PermSet --- The support of a permutation; i.e., the set of elements where the permutation actually maps the element to a different one. -def Equiv.Perm.supp (π : Equiv.Perm X) : Set X := - {x | π x ≠ x} +variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] -@[simp] -theorem mem_support (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by - simp [Equiv.Perm.supp] +/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/ +class PermSet (X : Type) extends MulAction (FPerm 𝔸) X --- 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] - intro x hx - contradiction +/-- The set of atoms itself forms a G-Set. -/ +instance : PermSet 𝔸 𝔸 where + smul π a := π a + one_smul := by aesop + mul_smul := by aesop --- The support of the inverse function is the same as the function's support. -lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by - simp [Equiv.Perm.supp, Equiv.Perm.set_support_inv_eq] +/-- The set of finite permutations forms a G-Set. -/ +instance : PermSet 𝔸 (FPerm 𝔸) where + smul π τ := π * τ + one_smul := by aesop + mul_smul := by aesop --- The support of two concatenated permutations is a subset of the individual supports as a union. -lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by - simp [Equiv.Perm.supp] - apply Equiv.Perm.set_support_mul_subset +/-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/ +instance PermSet.discrete (X : Type) : PermSet 𝔸 X where + smul π x := x + one_smul := by aesop + mul_smul := by aesop -lemma supp_swap [DecidableEq X] {x y : X} (h : x ≠ y) : ⸨x, y⸩.supp = {x, y} := by - ext z - by_cases hx : z = x - · simpa [hx] using h.symm - · by_cases hy : z = y - · simpa [Equiv.swap_apply_of_ne_of_ne, hx, hy] using h - · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy] +/-- We consider Unit a discrete (FPerm 𝔸)-Set. -/ +instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit --- The group of (finitely supported) permutations. -def FPerm (X: Type) : Subgroup (Equiv.Perm X) where - carrier := {π | π.supp.Finite} - mul_mem' {π τ} hπ hτ := by - apply (hπ.union hτ).subset - exact supp_mul_subset π τ - one_mem' := by - simp [supp_one] - inv_mem' {x} hx := by - simp [supp_inv] - exact hx +/-- We consider Bool a discrete (FPerm 𝔸)-Set. -/ +instance : PermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool -lemma supp_swap_finite [DecidableEq X] (x y : X) : ⸨x, y⸩ ∈ FPerm X := by - by_cases hx : x = y - · rw [<-Equiv.swap_eq_one_iff] at hx - simp [hx] - · simp [FPerm, supp_swap hx] +end PermSet -lemma supp_mul_finite {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X := - (FPerm X).mul_mem hπ hτ +/-! +## Support Definitions -lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X := - (FPerm X).inv_mem hπ +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 --- Since FPerm is a subgroup of Perm, it is also a group. -instance (X : Type) : Group (FPerm X) := - Subgroup.toGroup (FPerm X) +variable (𝔸 : Type) {X : Type} [PermSet 𝔸 X] --- Since FPerm is a subset of Perm, we can coerce it into a function. -instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where - coe π := (↑π : Equiv.Perm X) +namespace PermSet -example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩ +/-- The permutations that leave an element x unchanged. -/ +def fix' (x : X) : Set (FPerm 𝔸) := + { π : FPerm 𝔸 | π • x = x } -end Permutations +/-- The permutations that leave all elements in A unchanged. -/ +def fix (A : Set X) : Set (FPerm 𝔸) := + { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x } -section GSets +/-- 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 -variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] +@[simp] +lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ fix 𝔸 S ⊆ fix' 𝔸 x := by + rfl --- A G-set is a set X equipped with a group action •: (FPerm 𝔸) × X → X. -class GSet (X : Type) extends MulAction (FPerm 𝔸) X +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 + aesop -instance : GSet 𝔸 𝔸 where - smul π a := π a - one_smul := by aesop - mul_smul := by aesop +lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by + sorry -instance discreteGSet (X : Type) : GSet 𝔸 X where - smul π x := x - one_smul := by aesop - mul_smul := by aesop +end PermSet -instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit -instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool +end Support -variable {X : Type} [GSet 𝔸 X] +/-! +## Basic Nominal Set Definition --- The permutations that leave an element x unchanged. -def fix' (x : X) : Set (FPerm 𝔸) := - { π : FPerm 𝔸 | π • x = x } +Nominal sets are then just G-Sets where all elements are finitely supported. +-/ +section NominalSet --- The permutations that leave all elements in A unchanged. -def fix (A : Set X) : Set (FPerm 𝔸) := - { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x } +variable (𝔸 : Type) --- 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 +/-- A G-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 -end GSets +namespace NominalSet -section NominalSets +variable {X : Type} [nom : NominalSet 𝔸 X] -variable (𝔸 : Type) +/-- For every element x of a nominal set, there exists a least finite support, denoted "supp x". --/ +noncomputable def supp (x : X) : Set 𝔸 := + ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S } + +/-- 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 --- A G-Set X is nominal if every x ∈ X is finitely supported. -class Nominal (X : Type) extends GSet 𝔸 X where - finsupp : ∀ (x : X), ∃ (S : Set 𝔸), HasSupport 𝔸 x S ∧ S.Finite +/-- The least finite support is itself a support. -/ +lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := sorry -instance : Nominal 𝔸 𝔸 where +end NominalSet + +/-- The set of atoms is a nominal set, where supp a = {a}. -/ +instance : NominalSet 𝔸 𝔸 where finsupp := by intro a use {a} @@ -126,7 +128,10 @@ instance : Nominal 𝔸 𝔸 where aesop · simp -instance discreteNominal (X : Type) : Nominal 𝔸 X where +-- TODO: Prove supp a = {a} + +/-- Every set can be made into a discrete nominal set where every element has empty support. -/ +instance NominalSet.discrete (X : Type) : NominalSet 𝔸 X where finsupp := by intro x use {} @@ -135,21 +140,12 @@ instance discreteNominal (X : Type) : Nominal 𝔸 X where aesop · simp -instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit -instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool - -variable {X : Type} [nom : Nominal 𝔸 X] +-- TODO: Prove supp x = ∅ --- For every element x of a nominal set, there exists a least finite support, denoted "supp x". -noncomputable def supp (x : X) : Set 𝔸 := - ⋂₀ { S : Set 𝔸 | HasSupport 𝔸 x S } +/-- We consider Unit a discrete nominal set. -/ +instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit --- The least finite support in a nominal set is always finite. -theorem supp_finite (x : X) : (supp 𝔸 x).Finite := by - unfold supp - obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x - apply Set.Finite.subset - · exact hfinS - · grind +/-- We consider Bool a discrete nominal set. -/ +instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool -end NominalSets +end NominalSet diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean new file mode 100644 index 0000000..40f0f13 --- /dev/null +++ b/Nominal/Permutations.lean @@ -0,0 +1,127 @@ +import Mathlib.Tactic + +/-! +# Finitely supported permutations + +This file defines `FPerm`, the subgroup of permutations with finite support. +It also provides basic lemmas about permutation supports and transpositions. +-/ + +/-! +## Support Definition + +Support is defined on Equiv.Perm which also includes infinitely supported permutations. +-/ +section Support + +variable {X : Type} + +namespace Equiv.Perm + +/-- +The support of a permutation; i.e., the set of elements the permutation actually changes. + +Note that, while there is an Equiv.Perm.support, it only works for finite types and thus finite supports. +-/ +def supp (π : Equiv.Perm X) : Set X := + {x | π x ≠ x} + +@[simp] +theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by rfl + +/-- 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] + intro x hx + contradiction + +/-- The support of the inverse function is the same as the function's support. -/ +lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by + simp [supp, set_support_inv_eq] + +/-- The support of two concatenated permutations is a subset of the individual supports as a union. -/ +lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by + simp [supp] + apply set_support_mul_subset + +end Equiv.Perm + +end Support + +/-! +## FPerm Group + +The FPerm group is the subgroup of finitely supported permutations. +-/ +section Subgroup + +/-- The group of (finitely supported) permutations. -/ +def FPerm (X : Type) : Subgroup (Equiv.Perm X) where + carrier := {π | π.supp.Finite} + mul_mem' {π τ} hπ hτ := by + apply (hπ.union hτ).subset + exact Equiv.Perm.supp_mul_subset π τ + one_mem' := by + simp [Equiv.Perm.supp_one] + inv_mem' {x} hx := by + simp [Equiv.Perm.supp_inv] + exact hx + +variable {X : Type} + +namespace FPerm + +lemma mem_mul {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X := + (FPerm X).mul_mem hπ hτ + +lemma mem_inv {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X := + (FPerm X).inv_mem hπ + +end FPerm + +/-- Since FPerm is a subset of Equiv.Perm, we can coerce it into a function. -/ +instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where + coe π := (↑π : Equiv.Perm X) + +end Subgroup + +/-! +## Transpositions + +Transpositions are a special case of finite permutations, where only (at most) two elements are swapped. +-/ +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 + if h : (x ≠ y) then + ext z + by_cases hx : z = x + · aesop + · by_cases hy : z = y + · simp [hy] + · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy] + else + aesop + +end Equiv.Perm + +namespace FPerm + +lemma mem_swap {x y : X} : ⸨x, y⸩ ∈ FPerm X := by + apply Set.Finite.subset + · apply ({x, y} : Finset X).finite_toSet + · simp [Equiv.Perm.supp_swap] + aesop + +end FPerm + +example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [FPerm.mem_swap, FPerm.mem_mul]⟩ + +end Transposition |