diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 7087076..4ba580d 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -77,6 +77,12 @@ lemma comp_equivariant {f : Y โ Z} {g : X โ Y} : Function.Equivariant ๐ธ f f (g (ฯ โข x)) = f (ฯ โข g x) := by rw [hg] _ = ฯ โข (f (g x)) := by rw [hf] +/-- If a function is equivariant, its inverse is also equivariant. -/ +lemma Function.inv_equivariant {f : X โ Y} {inv : Y โ X} : Function.LeftInverse inv f โ Function.RightInverse inv f โ Function.Equivariant ๐ธ f โ Function.Equivariant ๐ธ inv := by + intro hleft hright hequi y ฯ + apply hleft.injective + rw [hequi, hright, hright] + /-- The subset relation is equivariant. -/ lemma Set.subset_equivariant : Rel.Equivariant ๐ธ (Set.Subset : Set X โ Set X โ Prop) := by intro S T ฯ hST x hx @@ -332,3 +338,36 @@ class EquivariantSetoid (X : Type) [PermSet ๐ธ X] extends Setoid X where equivariant : Rel.Equivariant ๐ธ r end BundledFunction + +/-! +## Equivalences + +If two types are equivalent and the conversion function is also equivariant, we know some additional information about nominal set structures. +-/ +section Equivalence + +/-- An equivalence where the function is equivariant. -/ +structure EquivariantEquiv (X Y : Type) [PermSet ๐ธ X] [PermSet ๐ธ Y] extends Equiv X Y where + toFun_equivariant : Function.Equivariant ๐ธ toFun + invFun_equivariant : Function.Equivariant ๐ธ invFun := Function.inv_equivariant ๐ธ left_inv right_inv toFun_equivariant + +def Equivariant.Equiv.symm {๐ธ X Y : Type} [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] [PermSet ๐ธ X] [PermSet ๐ธ Y] (equiv : EquivariantEquiv ๐ธ X Y) : EquivariantEquiv ๐ธ Y X := + { toFun := equiv.invFun + invFun := equiv.toFun + toFun_equivariant := equiv.invFun_equivariant + left_inv := equiv.right_inv + right_inv := equiv.left_inv + } + +/-- If an (FPerm ๐ธ)-Set is equivalent to a nominal set, it is also a nominal set. -/ +def NominalSet.fromEquivariantEquiv {X Y : Type} [PermSet ๐ธ X] [NominalSet ๐ธ Y] (equiv : EquivariantEquiv ๐ธ X Y) : NominalSet ๐ธ X := + NominalSet.fromEquivariantSurjective ๐ธ equiv.invFun equiv.invFun_equivariant equiv.symm.surjective + +/-- If two nominal sets are equivalent, the corresponding least supports are equal. -/ +lemma EquivariantEquiv.supp_eq {X Y : Type} [NominalSet ๐ธ X] [NominalSet ๐ธ Y] (equiv : EquivariantEquiv ๐ธ X Y) (x : X) : NominalSet.supp ๐ธ x = NominalSet.supp ๐ธ (equiv.toFun x) := by + symm + apply Function.Equivariant.supp_eq_if_inj + ยท exact equiv.toFun_equivariant + ยท exact equiv.injective + +end Equivalence |