import Mathlib import Nominal.Permutations import Nominal.Support /-! # Definitions and Properties for Equivariance We define equivariance for functions, sets, and binary relations. -/ variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] /-! ## Definitions Basic definitions for equivariance. -/ section Definition variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] /-- A function is equivariant if it is invariant to applying a permutation before or after the function. -/ def Equivariant (f : X β†’ Y) : Prop := βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x /-- A set is equivariant if it is closed under permutations. -/ def EquivariantSet (S : Set X) : Prop := βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S β†’ Ο€ β€’ x ∈ S /-- A binary relation is equivariant if it is closed under permutations. -/ 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 : Y β†’ Z} {g : X β†’ Y} : Equivariant 𝔸 f β†’ Equivariant 𝔸 g β†’ Equivariant 𝔸 (f ∘ g) := by intro hf hg x Ο€ calc f (g (Ο€ β€’ x)) = f (Ο€ β€’ g x) := by rw [hg] _ = Ο€ β€’ (f (g x)) := by rw [hf] /-- 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. -/ section Support variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] namespace Equivariant /-- Equivariant functions preserve supports. -/ lemma preserve_support {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant 𝔸 f β†’ PermSet.HasSupport 𝔸 x S β†’ PermSet.HasSupport 𝔸 (f x) S := by intro hequi hsupp Ο€ hΟ€ calc Ο€ β€’ f x = f (Ο€ β€’ x) := by rw [← hequi] _ = f x := by rw [hsupp hΟ€] /-- Equivariant injective functions exactly preserve supports. -/ lemma preserve_support_inj {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant 𝔸 f β†’ f.Injective β†’ (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by intro hequi hinj; constructor Β· exact preserve_support 𝔸 hequi Β· intro hsupp Ο€ hΟ€ by_contra h have : Ο€ β€’ f x β‰  f x := by rw [← hequi]; exact fun a => h (hinj a) have : Ο€ β€’ f x = f x := hsupp hΟ€ contradiction 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 /-! ## Nominal Sets Properties about equivariance relating to nominal sets. -/ section Nominal variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] namespace Equivariant /-- If f is equivariant, then supp (f x) βŠ† supp x. -/ lemma supp_subset {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β†’ NominalSet.supp 𝔸 (f x) βŠ† NominalSet.supp 𝔸 x := by intro hequi apply NominalSet.support_subset_supp Β· exact preserve_support 𝔸 hequi (NominalSet.supp_is_support 𝔸) Β· exact NominalSet.supp_finite 𝔸 /-- If f is equivariant and injective, then supp (f x) = supp x. -/ lemma supp_eq_if_inj {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β†’ Function.Injective f β†’ NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by intro hequi hinj simp [NominalSet.supp, preserve_support_inj 𝔸 hequi hinj] 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 /-! ## Bundled Functions In the following, we also define a bundled function type for equivariant functions. -/ section BundledFunction /-- A function carrying a proof of its equivariance. -/ structure EquivariantMap (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] where /-- The underlying function. -/ toFun : X β†’ Y /-- Proof of equivariance. -/ equivariant : Equivariant 𝔸 toFun /-- We write `X β†’β‚‘ Y` or `X β†’β‚‘[𝔸] Y` for an equivariant map X β†’ Y. -/ infixr:25 " β†’β‚‘ " => EquivariantMap _ /-- We write `X β†’β‚‘ Y` or `X β†’β‚‘[𝔸] Y` for an equivariant map X β†’ Y. -/ notation:25 X " β†’β‚‘[" A "] " Y => EquivariantMap A X Y variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] instance : FunLike (X β†’β‚‘[𝔸] Y) X Y where coe := EquivariantMap.toFun coe_injective' f g h := by cases f; cases g; congr namespace EquivariantMap /-- The identity function. -/ def id : X β†’β‚‘[𝔸] X := ⟨_root_.id, id_equivariant π”ΈβŸ© /-- Function composition. -/ def comp (f : Y β†’β‚‘[𝔸] Z) (g : X β†’β‚‘[𝔸] Y) : X β†’β‚‘[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩ @[simp] lemma toFun_eq_coe {f : X β†’β‚‘[𝔸] Y} : f.toFun = (f : X β†’ Y) := rfl @[ext] lemma ext {f g : X β†’β‚‘[𝔸] Y} (h : βˆ€ a, f a = g a) : f = g := DFunLike.ext _ _ h end EquivariantMap end BundledFunction