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
|
import Nominal.Permutations
import Nominal.Support
/-!
# Instances
This file contains common instances of (FPerm 𝔸)-sets and nominal sets.
-/
variable (𝔸 : Type)
/-!
## Atoms
The set 𝔸 of atoms itself is a nominal set, where supp a = {a}.
-/
section Atoms
private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
simp [PermSet.HasSupport, PermSet.fix, PermSet.fix']
instance : NominalSet 𝔸 𝔸 where
fin_supp := by
intro a
use {a}
exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩
lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
ext b; constructor
· apply support_subset_supp
· apply NominalSet.supp_atoms'
· apply Set.finite_singleton
· suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h]
intro S ⟨hsuppS, hfinS⟩
by_contra ha
-- Show that we can find a fresh c with (a c) ∈ fix S
obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
simp at hc
have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
intro d hd
apply Equiv.Perm.supp_notin
simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left]
exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption
rw [h₁] at h₂
exact hc.left h₂
end Atoms
/-!
## Discrete Nominal Sets
Every set can be made into a discrete nominal set, where supp x = ∅.
-/
section Discrete
def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
smul π x := x
one_smul := by intro; rfl
mul_smul := by intro _ _ _; rfl
is_discrete := by intro _ _; rfl
fin_supp := by
intro x
use {}
constructor
· intro π hπ; simp [PermSet.fix']; rfl
· exact Set.finite_empty
lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
rw [← Set.subset_empty_iff]
apply Set.sInter_subset_of_mem
constructor
· intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete]
· exact Set.finite_empty
/-- We consider Unit a discrete nominal set. -/
instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
/-- We consider Bool a discrete nominal set. -/
instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
end Discrete
|
