module CoSub where
{-
This file deals with the relations between PermSets and NomSets.
-}
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import Group
open import PermSet
open import CatDef
-----------------------------------------------------------------------------------------------
--all finitely supported functions to 𝔹
-----------------------------------------------------------------------------------------------
Ωˣ : (X : Nominal) → Nominal
Ωˣ X = NomExp X 𝔹Nom
----------------------------------------------------------------------------------------------
--subset of all finitely supported elements of P
----------------------------------------------------------------------------------------------
record FinSupp (P : PermSet) : Set where
field
pel : AₛP P
psupp : List Atom
psuppAx : (b c : Atom) → (b ∉ psupp) → (c ∉ psupp) → (≈ₐP P) ((ActP P) [(b , c)] pel) pel
open FinSupp public
-----------------------------------------------------------------------------------------------
--equivalence relation on this subset
-----------------------------------------------------------------------------------------------
≈FS : (P : PermSet) → Rel (FinSupp P)
≈FS P = λ ρ₁ ρ₂ → (≈ₐP P) (pel ρ₁) (pel ρ₂)
eq≈FS : (P : PermSet) → isEquivalence (FinSupp P) (≈FS P)
eq≈FS P = record { Reflex = λ {ρ} → (Reflex (eq≈ₐP P)) {pel ρ}
; Symm = λ {ρ₁}{ρ₂} → λ ρ₁≈ρ₂ → (Symm (eq≈ₐP P)) ρ₁≈ρ₂
; Trans = λ ρ₁≈ρ₂ ρ₂≈ρ₃ → (Trans (eq≈ₐP P)) ρ₁≈ρ₂ ρ₂≈ρ₃
}
-------------------------------------------------------------------------------------------
--This is closed under action
-------------------------------------------------------------------------------------------
ActFS : (P : PermSet) → (π : Perm) → FinSupp P → FinSupp P
ActFS P π ρ = record { pel = (ActP P) π (pel ρ)
; psupp = (flatten π) ++ (psupp ρ)
; psuppAx = λ b c b∉πρ c∉πρ → let πₛ = flatten π in let ρₛ = psupp ρ in let b∉π = ∉⊆₁ {πₛ}{ρₛ} b b∉πρ in let b∉ρ = ∉⊆₂ {πₛ}{ρₛ} b b∉πρ
in let c∉π = ∉⊆₁ {πₛ}{ρₛ} c c∉πρ in let c∉ρ = ∉⊆₂ {πₛ}{ρₛ} c c∉πρ in let πρ = (ActP P) π (pel ρ) in
let πρ≈πρ = ((ActP P) [(b , c)] πρ) ≣< ((ActP P) (π ++ [(b , c)]) (pel ρ)) and πρ by (≈ₐP P) as (eq≈ₐP P) on
((p₁p₂↠P P) [(b , c)] π {pel ρ}) >
(((ActP P) (π ++ [(b , c)]) (pel ρ))
≣< ((ActP P) ([(b , c)] ++ π) (pel ρ)) and πρ by (≈ₐP P) as (eq≈ₐP P) on
((Symm (eq≈ₐP P)) ((resP P) (λ {w} → ab∉pcom b c π b∉π c∉π {w}) (≈≡ (eq≈ₐP P) {pel ρ}{pel ρ} refl))) >
(((ActP P) ([(b , c)] ++ π) (pel ρ))
≣< ((ActP P) π ((ActP P) [(b , c)] (pel ρ))) and πρ by (≈ₐP P) as (eq≈ₐP P) on
((Symm (eq≈ₐP P)) ((p₁p₂↠P P) π [(b , c)] {pel ρ})) >
(((ActP P) π ((ActP P) [(b , c)] (pel ρ)))
≣< πρ and πρ by (≈ₐP P) as (eq≈ₐP P) on
((resP P) (λ {w} → P≡≈ π {w}) ((psuppAx ρ) b c b∉ρ c∉ρ)) >
(πρ by (≈ₐP P) as (eq≈ₐP P) ▴)))) in πρ≈πρ
}
-----------------------------------------------------------------------------------------------------------------------------------------
--FUNCTOR FROM NOM TO PERM & VICE-VERSA
-----------------------------------------------------------------------------------------------------------------------------------------
-----------------------------------------------------------------------------------------------
--Nominal Set to Perm Set object
-----------------------------------------------------------------------------------------------
NomPerm : (N : Nominal) → PermSet
NomPerm N = record {AₛP = Aₛ N
; ≈ₐP = ≈ₐ N
; eq≈ₐP = eq≈ₐ N
; ActP = Act N
; resP = res N
; p₁p₂↠P = p₁p₂↠ N
; ι↠P = ι↠ N
}
----------------------------------------------------------------------------------------------
--PermSet to Nominal Set object
----------------------------------------------------------------------------------------------
PermNom : (P : PermSet) → Nominal
PermNom P = record { Aₛ = FinSupp P
; ≈ₐ = ≈FS P
; eq≈ₐ = eq≈FS P
; Act = λ π ρ → ActFS P π ρ
; res = λ {π₁}{π₂}{ρ₁}{ρ₂} → λ π₁≈π₂ ρ₁≈ρ₂ → (resP P) π₁≈π₂ ρ₁≈ρ₂
; p₁p₂↠ = λ π₁ π₂ {ρ} → (p₁p₂↠P P) π₁ π₂ {pel ρ}
; ι↠ = λ {ρ} → (ι↠P P) {pel ρ}
; some_supp = λ ρ → psupp ρ
; suppAx = λ ρ → λ b c b∉ρ c∉ρ → (psuppAx ρ) b c b∉ρ c∉ρ
}
------------------------------------------------------------------------------------------------------------
--Nominal to Perm morphism
------------------------------------------------------------------------------------------------------------
NomPermEq : (M N : Nominal) → (F : Equivar M N) → EquivarP (NomPerm M) (NomPerm N)
NomPermEq M N F = record { pufun = λ m → (ufun F) m
; peqi≈ = λ m₁≈m₂ → (eqi≈ F) m₁≈m₂
; pequiv = λ π m → (equiv F) π m
}
-------------------------------------------------------------------------------------------------------
--Perm to Norm Morphism
-------------------------------------------------------------------------------------------------------
PermNomEq : (P Q : PermSet) → (G : EquivarP P Q) → Equivar (PermNom P) (PermNom Q)
PermNomEq P Q G = record { ufun = λ ρ → record { pel = (pufun G) (pel ρ)
; psupp = psupp ρ
; psuppAx = λ b c b∉ρ c∉ρ → let gρ = (pufun G) (pel ρ) in
let gρ≈gρ = ((ActP Q) [(b , c)] gρ) ≣< ((pufun G) ((ActP P) [(b , c)] (pel ρ))) and gρ by (≈ₐP Q) as (eq≈ₐP Q) on
((pequiv G) [(b , c)] (pel ρ)) >
(((pufun G) ((ActP P) [(b , c)] (pel ρ)))
≣< gρ and gρ by (≈ₐP Q) as (eq≈ₐP Q) on
((peqi≈ G) ((psuppAx ρ) b c b∉ρ c∉ρ)) >
(gρ by (≈ₐP Q) as (eq≈ₐP Q) ▴)) in gρ≈gρ
}
; eqi≈ = λ ρ₁≈ρ₂ → (peqi≈ G) ρ₁≈ρ₂
; equiv = λ π ρ → (pequiv G) π (pel ρ)
}
-------------------------------------------------------------------------------------------------------------
--functors
-------------------------------------------------------------------------------------------------------------
Nom→Perm : Functor NomCat PermCat
Nom→Perm = record { onObj = λ N → NomPerm N
; onMor = λ M N → λ MN → NomPermEq M N MN
; res≈ = λ M N → λ MN MN' → λ MNN' → λ m → MNN' m
; onId = λ M → λ m → (Reflex (eq≈ₐP (NomPerm M))) {m}
; onComp = λ M N O → λ F G → λ m → let Pₒ = NomPerm O in let PF = NomPermEq M N F in let PG = NomPermEq N O G in
let gfm = ((pufun PG) ∘ (pufun PF)) m in (Reflex (eq≈ₐP Pₒ)) {gfm}
}
Perm→Nom : Functor PermCat NomCat
Perm→Nom = record { onObj = λ P → PermNom P
; onMor = λ P Q → λ PQ → PermNomEq P Q PQ
; res≈ = λ P Q → λ PQ PQ' → λ PQQ' → λ p → PQQ' (pel p)
; onId = λ P → λ p → (Reflex (eq≈ₐ (PermNom P))) {p}
; onComp = λ P Q R → λ I J → λ p → (Reflex (eq≈ₐ (PermNom R))) {((ufun (PermNomEq Q R J)) ∘ (ufun (PermNomEq P Q I))) p}
}
----------------------------------------------------------------------------------------------
--counit
---------------------------------------------------------------------------------------------
NPN : (P : PermSet) → (EquivarP (NomPerm (PermNom P)) P)
NPN P = record { pufun = λ ρ → pel ρ
; peqi≈ = λ ρ₁≈ρ₂ → ρ₁≈ρ₂
; pequiv = λ π ρ → (Reflex (eq≈ₐP P)) {(ActP P) π (pel ρ)}
}
-----------------------------------------------------------------------------------------
--unique morphism
-----------------------------------------------------------------------------------------
NP⟶NP : (P : PermSet) → (N : Nominal) → (EquivarP (NomPerm N) P) → Equivar N (PermNom P)
NP⟶NP P N J = record { ufun = λ n → record { pel = (pufun J) n
; psupp = (some_supp N) n
; psuppAx = λ b c b∉n c∉n → let jn = (pufun J) n in
let n≈n = ((ActP P) [(b , c)] jn) ≣< ((pufun J) ((Act N) [(b , c)] n)) and jn by (≈ₐP P) as (eq≈ₐP P) on ((pequiv J) [(b , c)] n) >
(((pufun J) ((Act N) [(b , c)] n)) ≣< jn and jn by (≈ₐP P) as (eq≈ₐP P) on ((peqi≈ J) ((suppAx N) n b c b∉n c∉n)) >
(jn by (≈ₐP P) as (eq≈ₐP P) ▴)) in n≈n
}
; eqi≈ = λ n₁≈n₂ → (peqi≈ J) n₁≈n₂
; equiv = λ π n → (pequiv J) π n
}
-----------------------------------------------------------------------------------------------
--coreflective subcategory
-----------------------------------------------------------------------------------------------
CoR : Adjoint NomCat PermCat Nom→Perm Perm→Nom
CoR = record { counit = λ P → NPN P
; f̂ = λ P N F → NP⟶NP P N F
; f̂ε = λ P N F → λ n → (Reflex (eq≈ₐP P)) {(pufun F) n}
; unif̂ = λ P N F G G∘C → λ n → G∘C n
}
----------------------------------------------------------------------------------------------------------------------------------------
--PowerSets
---------------------------------------------------------------------------------------------------------------------------------------
ℙX : (X : PermSet) → PermSet
ℙX X = record { AₛP = FunPerm X 𝔹Perm
; ≈ₐP = λ f g → ∀ (x : AₛP X) → ((underFun f) x) ≡ ((underFun g) x)
; eq≈ₐP = record { Reflex = λ {f} → λ x → refl
; Symm = λ f≈g → λ x → sym (f≈g x)
; Trans = λ {f}{g}{h} f≈g g≈h → λ x → ((underFun f) x) ≡< f≈g x > (((underFun g) x) ≡< g≈h x > (((underFun h) x) ▪))
}
; ActP = λ π f → FP (λ x → (underFun f) ((ActP X) (invPerm π) x)) (λ {x₁}{x₂} x₁≈x₂ → (congFun f) ((resP X) (λ {w} → P≡≈ (invPerm π) {w}) x₁≈x₂))
; resP = λ {π₁}{π₂}{f}{g} π₁≈π₂ f≈g → λ x →
(underFun f (ActP X (invPerm π₁) x))
≡< (congFun f) ((resP X) (p≈q⇒p⁻¹≈q⁻¹ π₁ π₂ π₁≈π₂) (≈≡ (eq≈ₐP X) {x}{x} refl)) >
(((underFun f) (ActP X (invPerm π₂) x))
≡< f≈g (ActP X (invPerm π₂) x) >
((underFun g (ActP X (invPerm π₂) x)) ▪))
; p₁p₂↠P = λ π₁ π₂ {f} → λ x → let π₁π₂ix = (ActP X (invPerm π₂) (ActP X (invPerm π₁) x)) in let π₁₂ix = (ActP X (invPerm (π₂ ++ π₁)) x) in
let π₁π₂π₁₂ = π₁π₂ix ≣< (ActP X ((invPerm π₁) ++ (invPerm π₂)) x) and π₁₂ix by (≈ₐP X) as (eq≈ₐP X) on (p₁p₂↠P X) (invPerm π₂) (invPerm π₁) {x} >
((ActP X ((invPerm π₁) ++ (invPerm π₂)) x) ≣< π₁₂ix and π₁₂ix by (≈ₐP X) as (eq≈ₐP X) on ((Symm (eq≈ₐP X)) ((resP X) (p₁p₂⁻¹≈p₂⁻¹p₁⁻¹ π₂ π₁)
(≈≡ (eq≈ₐP X) {x}{x} refl))) >
(π₁₂ix by (≈ₐP X) as (eq≈ₐP X) ▴)) in (congFun f) π₁π₂π₁₂
; ι↠P = λ {f} → λ x → congFun f (ι↠P X)
}
PₛX : (X : Nominal) → Nominal
PₛX X = PermNom (ℙX (NomPerm X))
------------------------------------------------------------------------------------------------
--finitely supported subsets of PermSet constitute the powerset of NomSet
------------------------------------------------------------------------------------------------
Power : (X : Nominal) → Iso {NomCat} (Ωˣ X) (PₛX X)
Power X = record { liso = record { ufun = λ F → record { pel = FP (λ x → (ffun F) x) (λ x₁≈x₂ → (feqi≈ F) x₁≈x₂)
; psupp = fsupp F
; psuppAx = λ b c b∉p c∉p → λ x → (fsuppAx F) b c b∉p c∉p x
}
; eqi≈ = λ F≈G → λ x → F≈G x
; equiv = λ π F → λ x → (((ffun F) ((Act X) (invPerm π) x)) ▪)
}
; riso = record { ufun = λ X₁ → record { ffun = λ x → (underFun (pel X₁)) x
; fsupp = psupp X₁
; fsuppAx = λ b c b∉x c∉x x → (psuppAx X₁) b c b∉x c∉x x
; feqi≈ = λ x₁≈x₂ → (congFun (pel X₁)) x₁≈x₂
}
; eqi≈ = λ X₁≈X₂ → λ x → X₁≈X₂ x
; equiv = λ π X₁ → λ x → (((underFun (pel X₁)) ((Act X) (invPerm π) x)) ▪)
}
; idisl = λ F x → (((ffun F) x) ▪)
; idisr = λ X₁ x → (((underFun (pel X₁)) x) ▪)
}
--------------------------------------------------------------------------------------------------------------