diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 2682a55..e9bd850 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -25,7 +25,7 @@ class inductive Function.Equivariant (f : X โ Y) : Prop lemma Function.equivariant (f : X โ Y) [Equivariant ๐ธ f] : โ (x : X) (ฯ : FPerm ๐ธ), f (ฯ โข x) = ฯ โข f x := by - cases (inferInstanceAs (Equivariant ๐ธ f)); assumption + cases (inferInstance : Equivariant ๐ธ f); assumption /-- A set is equivariant if it is closed under permutations. -/ class inductive Set.Equivariant (S : Set X) : Prop @@ -34,7 +34,7 @@ class inductive Set.Equivariant (S : Set X) : Prop /-- For equivariant sets, we even have "if and only if". -/ lemma Set.equivariant (S : Set X) [Equivariant ๐ธ S] : โ (x : X) (ฯ : FPerm ๐ธ), x โ S โ ฯ โข x โ S := by - cases (inferInstanceAs (Equivariant ๐ธ S)); rename_i h + cases (inferInstance : Equivariant ๐ธ S); rename_i h intro x ฯ; constructor ยท intro hx; exact h x ฯ hx ยท intro hx @@ -49,7 +49,7 @@ class inductive Rel.Equivariant (R : Rel X Y) : Prop /-- For equivariant relations, we even have "if and only if". -/ lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant ๐ธ R] : โ (x : X) (y : Y) (ฯ : FPerm ๐ธ), R x y โ R (ฯ โข x) (ฯ โข y) := by - cases (inferInstanceAs (Equivariant ๐ธ R)); rename_i h + cases (inferInstance : Equivariant ๐ธ R); rename_i h intro x y ฯ; constructor ยท intro hxy; exact h x y ฯ hxy ยท intro hxy @@ -83,6 +83,7 @@ instance Function.Equivariant.comp _ = ฯ โข (f (g x)) := by rw [โ Function.equivariant ๐ธ f] /-- If a function is equivariant, its inverse is also equivariant. -/ +@[reducible] def Function.Equivariant.inv {f : X โ Y} [Function.Equivariant ๐ธ f] {inv : Y โ X} (hleft : Function.LeftInverse inv f) @@ -191,6 +192,7 @@ lemma preserve_fresh_inj {a : ๐ธ} {x : X} {f : X โ Y} [Equivariant ๐ธ f] : end Function.Equivariant /-- If there is an equivariant surjection from a nominal set into an (FPerm ๐ธ)-Set, then that set is nominal. -/ +@[reducible] def NominalSet.ofEquivariantSurjective {X Y : Type} [NominalSet ๐ธ X] [PermSet ๐ธ Y] (f : X โ Y) [Function.Equivariant ๐ธ f] (hsurj : Function.Surjective f) : @@ -385,6 +387,7 @@ instance EquivariantEquiv.invFunEquivariant equiv.invFun_equivariant /-- If an (FPerm ๐ธ)-Set is equivalent to a nominal set, it is also a nominal set. -/ +@[reducible] def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet ๐ธ X] [NominalSet ๐ธ Y] (equiv : EquivariantEquiv ๐ธ X Y) : NominalSet ๐ธ X := NominalSet.ofEquivariantSurjective ๐ธ equiv.invFun equiv.symm.surjective |