diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Equivariance.lean | 92 | ||||
| -rw-r--r-- | Nominal/Instances.lean | 13 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 9 |
3 files changed, 112 insertions, 2 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 4d23e56..c9a5261 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -31,9 +31,62 @@ def EquivariantSet (S : Set X) : Prop := def EquivariantRelation (R : Rel X Y) : Prop := ∀ (x : X) (y : Y) (Ï€ : FPerm ð”¸), R x y → R (Ï€ • x) (Ï€ • y) +/-- For equivariant sets, we even have "if and only if". -/ +lemma equivariant_set_iff {S : Set X} : EquivariantSet 𔸠S ↔ ∀ (x : X) (Ï€ : FPerm ð”¸), x ∈ S ↔ Ï€ • x ∈ S := by + constructor + · intro h x Ï€; constructor + · intro hx; exact h x Ï€ hx + · intro hx + apply (h (Ï€ • x) Ï€â»Â¹) at hx + simp at hx + exact hx + · intro h x Ï€ hx + exact (h x Ï€).mp hx + +/-- For equivariant relations, we even have "if and only if". -/ +lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𔸠R ↔ ∀ (x : X) (y : Y) (Ï€ : FPerm ð”¸), R x y ↔ R (Ï€ • x) (Ï€ • y) := by + constructor + · intro h x y Ï€; constructor + · intro hxy; exact h x y Ï€ hxy + · intro hxy + apply (h (Ï€ • x) (Ï€ • y) Ï€â»Â¹) at hxy + simp at hxy + exact hxy + · intro h x y Ï€ hxy + exact (h x y Ï€).mp hxy + end Definition /-! +## Trivial Instances + +Some trivial instances of equivariant functions, sets, and relations. +-/ +section Trivial + +variable {X Y Z : Type} [PermSet 𔸠X] [PermSet 𔸠Y] [PermSet 𔸠Z] + +/-- The identity function is equivariant. -/ +lemma id_equivariant : Equivariant 𔸠(id : X → X) := by + simp [Equivariant] + +/-- The composition of two equivariant functions is equivariant. -/ +lemma comp_equivariant {f : X → Y} {g : Y → Z} : Equivariant 𔸠f → Equivariant 𔸠g → Equivariant 𔸠(g ∘ f) := by + intro hf hg x Ï€ + calc + g (f (Ï€ • x)) = g (Ï€ • f x) := by rw [hf] + _ = Ï€ • (g (f x)) := by rw [hg] + +/-- The subset relation is equivariant. -/ +lemma subset_equivariant : EquivariantRelation 𔸠(Set.Subset : Set X → Set X → Prop) := by + intro S T Ï€ hST x hx + rw [Set.mem_smul_set_iff_inv_smul_mem] at hx + rw [Set.mem_smul_set_iff_inv_smul_mem] + exact hST hx + +end Trivial + +/-! ## Support Propositions relating equivariance to support in (FPerm ð”¸)-sets. @@ -63,6 +116,24 @@ lemma preserve_support_inj {x : X} {f : X → Y} {S : Set ð”¸} : Equivariant ð end Equivariant +/-- HasSupport is an equivariant relation. -/ +lemma PermSet.support_equivariant : EquivariantRelation 𔸠(HasSupport 𔸠: X → Set 𔸠→ Prop) := by + intro x S Ï€ hS σ hσ + have hfix : (Ï€â»Â¹ * σ * Ï€) ∈ fix 𔸠S := by + intro a ha + calc + (Ï€â»Â¹ * σ * Ï€) • a = Ï€â»Â¹ • (σ • (Ï€ • a)) := rfl + _ = Ï€â»Â¹ • (Ï€ • a) := by rw [hσ (Ï€ • a) (Set.smul_mem_smul_set ha)] + _ = (Ï€â»Â¹ * Ï€) • a := rfl + _ = (1 : FPerm ð”¸) • a := by rw [@Group.inv_mul_cancel] + _ = a := rfl + calc + σ • (Ï€ • x) = (σ * Ï€) • x := by apply smul_smul + _ = (1 * σ * Ï€) • x := rfl + _ = (Ï€ * Ï€â»Â¹ * σ * Ï€) • x := by rw [@mul_inv_cancel] + _ = Ï€ • ((Ï€â»Â¹ * σ * Ï€) • x) := by symm; apply smul_smul + _ = Ï€ • x := by rw [hS hfix] + end Support /-! @@ -90,4 +161,25 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𔸠f → Function.Inj end Equivariant +/-- supp is an equivariant function. -/ +lemma NominalSet.supp_equivariant : Equivariant 𔸠(supp 𔸠: X → Set ð”¸) := by + intro x Ï€; ext a; constructor + · apply support_subset_supp 𔸠+ · apply PermSet.support_equivariant + exact supp_is_support 𔸠+ · apply Set.Finite.smul_set + exact supp_finite 𔸠+ · intro ha S hS + have hsupp : PermSet.HasSupport 𔸠x (Ï€â»Â¹ • S) := by + rw [show x = Ï€â»Â¹ • Ï€ • x by exact eq_inv_smul_iff.mpr rfl] + apply PermSet.support_equivariant + exact hS.out.left + rw [Set.mem_smul_set_iff_inv_smul_mem] at ha + suffices Ï€â»Â¹ • a ∈ Ï€â»Â¹ • S by rw [Set.smul_mem_smul_set_iff] at this; assumption + suffices supp 𔸠x ⊆ Ï€â»Â¹ • S by exact this ha + apply support_subset_supp 𔸠+ · exact hsupp + · apply Set.Finite.smul_set + exact hS.out.right + end Nominal diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index e28fe28..b637b32 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -1,5 +1,6 @@ import Mathlib import Nominal.Support +import Nominal.Equivariance /-! # Instances @@ -132,6 +133,12 @@ instance : NominalSet 𔸠(X × Y) where lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𔸠(x, y) = supp 𔸠(y, x) := by simp; apply Set.union_comm +lemma Prod.fst_equivariant : Equivariant 𔸠(Prod.fst : X × Y → X) := by + simp [Equivariant] + +lemma Prod.snd_equivariant : Equivariant 𔸠(Prod.snd : X × Y → Y) := by + simp [Equivariant] + end Products /-! @@ -190,4 +197,10 @@ instance : NominalSet 𔸠(X ⊕ Y) where @[simp] lemma NominalSet.fresh_coproductâ‚‚ {a : ð”¸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by simp [IsFresh] +lemma Sum.inl_equivariant : Equivariant 𔸠(Sum.inl : X → X ⊕ Y) := by + simp [Equivariant] + +lemma Sum.inr_equivariant : Equivariant 𔸠(Sum.inr : Y → X ⊕ Y) := by + simp [Equivariant] + end Coproducts diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index c8fdd86..4a3e88f 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -141,16 +141,21 @@ class PermSet (𔸠: Type) [Infinite ð”¸] [Countable ð”¸] [DecidableEq ð”¸] variable (𔸠: Type) [Infinite ð”¸] [Countable ð”¸] [DecidableEq ð”¸] -/-- The set of atoms itself forms a (FPerm ð”¸)-Set. -/ +/-- The set of atoms itself forms an (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. -/ +/-- The set of finite permutations forms an (FPerm ð”¸)-Set. -/ instance : PermSet 𔸠(FPerm ð”¸) where smul Ï€ Ï„ := Ï€ * Ï„ one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl +open Pointwise + +/-- The powerset of an (FPerm ð”¸)-Set forms an (FPerm ð”¸)-Set using pointwise permutation. -/ +instance {X : Type} [PermSet 𔸠X] : PermSet 𔸠(Set X) where + end PermSet |