diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean new file mode 100644 index 0000000..4d23e56 --- /dev/null +++ b/Nominal/Equivariance.lean @@ -0,0 +1,93 @@ +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) + +end Definition + +/-! +## 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 + +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 + +end Nominal |