module PermSet where
{-
This file contains definitions of PermSet, equivariant functions along with some examples.
It also shows that PermSets form a category.
-}
open import Basics
open import Perms
open import CatDef
open import Group
PermSet = GAct PermG
-----------------------------------------------------------------------------------------------------------------------
--Boolean is a discrete Perm-Set
-----------------------------------------------------------------------------------------------------------------------
𝔹Perm : PermSet
𝔹Perm = record { AₛP = 𝔹
; ≈ₐP = _≡_
; eq≈ₐP = aEquiv≡ 𝔹
; ActP = λ π → λ b → b
; resP = λ π₁≈π₂ → λ b≡b → b≡b
; p₁p₂↠P = λ p₁ p₂ → λ {b} → (Reflex (aEquiv≡ 𝔹)) {b}
; ι↠P = λ {b} → (Reflex (aEquiv≡ 𝔹)) {b}
}
--------------------------------------------------------------------------------------------------------------------------
--Product of Perm Sets
-------------------------------------------------------------------------------------------------------------------------
ProdP : (X Y : PermSet) → PermSet
ProdP X Y = record { AₛP = (AₛP X) × (AₛP Y)
; ≈ₐP = λ p₁ p₂ → (((≈ₐP X) (proj₁ p₁) (proj₁ p₂)) × ((≈ₐP Y) (proj₂ p₁) (proj₂ p₂)))
; eq≈ₐP = record { Reflex = λ {p₁} → ((Reflex (eq≈ₐP X)) {proj₁ p₁} , (Reflex (eq≈ₐP Y)) {proj₂ p₁})
; Symm = λ {p₁ p₂} → λ p₁≈p₂ → ((Symm (eq≈ₐP X)) (proj₁ p₁≈p₂) , (Symm (eq≈ₐP Y)) (proj₂ p₁≈p₂))
; Trans = λ {p₁ p₂ p₃} → λ p₁≈p₂ → λ p₂≈p₃ → ((Trans (eq≈ₐP X)) (proj₁ p₁≈p₂) (proj₁ p₂≈p₃) , (Trans (eq≈ₐP Y)) (proj₂ p₁≈p₂) (proj₂ p₂≈p₃))
}
; ActP = λ π → λ p → ((ActP X) π (proj₁ p) , (ActP Y) π (proj₂ p))
; resP = λ {π₁ π₂ p₁ p₂} → λ π₁≈π₂ → λ p₁≈p₂ → ((resP X) {π₁} {π₂} {proj₁ p₁} {proj₁ p₂} π₁≈π₂ (proj₁ p₁≈p₂) , (resP Y) {π₁}{π₂}{proj₂ p₁}{proj₂ p₂} π₁≈π₂ (proj₂ p₁≈p₂))
; p₁p₂↠P = λ π π' → (λ {p} → (((p₁p₂↠P X) π π' {proj₁ p}) , ((p₁p₂↠P Y) π π' {proj₂ p})))
; ι↠P = λ {p} → ((ι↠P X) {proj₁ p} , (ι↠P Y) {proj₂ p})
}
--------------------------------------------------------------------------------------------------------------------
--Equivariant functions
--------------------------------------------------------------------------------------------------------------------
record EquivarP (X Y : PermSet) : Set where
field
pufun : AₛP X → AₛP Y
peqi≈ : pufun Preserves (≈ₐP X) ⟶ (≈ₐP Y)
pequiv : (p : Perm) → (x : AₛP X) → (≈ₐP Y) ((ActP Y) p (pufun x)) (pufun ((ActP X) p x))
open EquivarP public
---------------------------------------------------------------------------------------------------------------------
--Group Action is an equivariant function
---------------------------------------------------------------------------------------------------------------------
GX→XEq : (X : PermSet) → EquivarP (ProdP PermGP X) X
GX→XEq X = record { pufun = λ gx → (ActP X) (proj₁ gx) (proj₂ gx)
; peqi≈ = λ {g₁x₁ g₂x₂} g₁x₁≈g₂x₂ → (resP X) (proj₁ g₁x₁≈g₂x₂) (proj₂ g₁x₁≈g₂x₂)
; pequiv = λ p gx → let (g , x) = gx in let px = (ActP X) p x in let pg = (ActP PermGP) p g in
let pgx≈gpx = ((ActP X) p ((ActP X) g x))
≣< ((ActP X) (g ++ p) x) and ((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) on
((p₁p₂↠P X) p g {x}) >
(((ActP X) (g ++ p) x)
≣< ((ActP X) (g ++ p) ((ActP X) ι x)) and ((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) on
((Symm (eq≈ₐP X)) ((resP X) (λ {w} → P≡≈ (g ++ p) {w}) ((ι↠P X) {x}))) >
(((ActP X) (g ++ p) ((ActP X) ι x))
≣< ((ActP X) (g ++ p) ((ActP X) (p ++ (invPerm p)) x)) and ((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) on
((Symm (eq≈ₐP X)) ((resP X) (λ {w} → P≡≈ (g ++ p) {w}) ((resP X) (λ {v} → pp⁻¹≡ι p {v}) (≈≡ (eq≈ₐP X) {x}{x} refl)))) >
(((ActP X) (g ++ p) ((ActP X) (p ++ (invPerm p)) x))
≣< ((ActP X) (g ++ p) ((ActP X) (invPerm p) px)) and ((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) on
((Symm (eq≈ₐP X)) ((resP X) (λ {w} → P≡≈ (g ++ p) {w})((p₁p₂↠P X) (invPerm p) p {x}))) >
(((ActP X) (g ++ p) ((ActP X) (invPerm p) px))
≣< ((ActP X) pg px) and ((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) on
((p₁p₂↠P X) (g ++ p) (invPerm p) {px}) >
(((ActP X) pg px) by (≈ₐP X) as (eq≈ₐP X) ▴))))) in pgx≈gpx
}
record FunPerm (A : PermSet) (B : PermSet) : Set where
constructor FP
field
underFun : (AₛP A) → (AₛP B)
congFun : underFun Preserves (≈ₐP A) ⟶ (≈ₐP B)
open FunPerm public
------------------------------------------------------------------------------------------------------------------------------------------------------------
--Perm Sets form a category
------------------------------------------------------------------------------------------------------------------------------------------------------------
--------------------------------------------------------------------------------------------------------------------------------------------
--Equivalence relation on equivariant functions
--------------------------------------------------------------------------------------------------------------------------------------------
≈̬P : {X Y : PermSet} → Rel (EquivarP X Y)
≈̬P {X}{Y} = λ F G → (∀ x → (≈ₐP Y) ((pufun F) x) ((pufun G) x))
vEqP : ∀ {X Y} → isEquivalence (EquivarP X Y) (≈̬P {X}{Y})
vEqP {X}{Y} = record { Reflex = λ {F} → (λ x → (Reflex (eq≈ₐP Y)) {(pufun F) x})
; Symm = λ {F G} → λ F≈G → (λ x → (Symm (eq≈ₐP Y)) (F≈G x))
; Trans = λ {F G H} → λ F≈G → λ G≈H → (λ x → (Trans (eq≈ₐP Y)) (F≈G x) (G≈H x))
}
------------------------------------------------------------------------------------------------------------------------------------
--Composition of equivariant functions
-----------------------------------------------------------------------------------------------------------------------------------
øP : {X Y Z : PermSet} → (F : EquivarP X Y) → (G : EquivarP Y Z) → EquivarP X Z
øP {X}{Y}{Z} F G = record { pufun = (pufun G) ∘ (pufun F)
; peqi≈ = λ {x₁ x₂} → λ x₁≈x₂ → (peqi≈ G) ((peqi≈ F) x₁≈x₂)
; pequiv = λ p x → let pgfx = (ActP Z) p (((pufun G) ∘ (pufun F)) x) in
let x≈x = ((((pufun G) ∘ (pufun F)) ((ActP X) p x))
≣< ((pufun G) ((ActP Y) p ((pufun F) x))) and pgfx by (≈ₐP Z) as (eq≈ₐP Z) on ((peqi≈ G) ((Symm (eq≈ₐP Y)) ( (pequiv F) p x ) )) >
(((pufun G) ((ActP Y) p ((pufun F) x)))
≣< pgfx and pgfx by (≈ₐP Z) as (eq≈ₐP Z) on ((Symm (eq≈ₐP Z)) ((pequiv G) p ((pufun F) x))) >
(pgfx by (≈ₐP Z) as (eq≈ₐP Z) ▴))) in (Symm (eq≈ₐP Z)) x≈x
}
---------------------------------------------------------------------------------------------------------------------------------
--identity equivariant function
---------------------------------------------------------------------------------------------------------------------------------
ø1P : (X : PermSet) → EquivarP X X
ø1P X = record { pufun = λ x → x
; peqi≈ = λ x₁≈x₂ → x₁≈x₂
; pequiv = λ p x → (Reflex (eq≈ₐP X)) {(ActP X) p x}
}
------------------------------------------------------------------------------------------------------------------------------
--identity axioms
------------------------------------------------------------------------------------------------------------------------------
idlP : {X Y : PermSet} → (F : EquivarP X Y) → ≈̬P (øP (ø1P X) F) F
idlP {X}{Y} F = λ x → (Reflex (eq≈ₐP Y)) {(pufun F) x}
idrP : {X Y : PermSet} → (G : EquivarP X Y) → ≈̬P (øP G (ø1P Y)) G
idrP {X}{Y} G = λ x → (Reflex (eq≈ₐP Y)) {(pufun G) x}
-------------------------------------------------------------------------------------------------------------------------------
--associativity axiom
-------------------------------------------------------------------------------------------------------------------------------
assoEqP : {X Y Z W : PermSet} → (F : EquivarP X Y) → (G : EquivarP Y Z) → (H : EquivarP Z W) → ≈̬P (øP (øP F G) H) (øP F (øP G H))
assoEqP {X}{Y}{Z}{W} F G H = λ x → (Reflex (eq≈ₐP W)) {(((pufun H) ∘ (pufun G)) ∘ (pufun F)) x}
----------------------------------------------------------------------------------------------------------------------------
--PermSets form a category
----------------------------------------------------------------------------------------------------------------------------
PermCat : Cat
PermCat = record { Obj = PermSet
; _⇒_ = λ X Y → EquivarP X Y
; _≈_ = λ {M N} → ≈̬P {M}{N}
; isEq = λ {M N} → vEqP {M}{N}
; id = λ {N} → ø1P N
; _⊚_ = λ MN NO → øP MN NO
; id1 = λ F → idlP F
; id2 = λ G → idrP G
; asso = λ f g h → assoEqP f g h
; resp = λ {X Y Z} → λ {f g h i} → λ f≈g → λ h≈i → (λ x → let igx = ((pufun i) ∘ (pufun g)) x in
let hf≈ig = ( ((pufun h) ∘ (pufun f)) x
≣< (((pufun h) ∘ (pufun g)) x) and igx by (≈ₐP Z) as (eq≈ₐP Z) on ((peqi≈ h) (f≈g x)) >
( ((pufun h) ∘ (pufun g)) x
≣< igx and igx by (≈ₐP Z) as (eq≈ₐP Z) on (h≈i ((pufun g) x)) >
( igx by (≈ₐP Z) as (eq≈ₐP Z) ▴))) in hf≈ig)
}
------------------------------------------------------------------------------------------------------------------------------------