blob: 4d23e56d160627ce66b101e82739969a87033661 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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
|
