90 lines
3.3 KiB
Agda
90 lines
3.3 KiB
Agda
open import Category.G-Sets
|
||
open import Algebra.Group
|
||
open import Algebra.G-Set
|
||
open import Category.Construction.GroupAsCategory
|
||
open import Categories.Category.Construction.Functors renaming (Functors to [_,_])
|
||
open import Categories.Category.Equivalence
|
||
open import Categories.Category.Instance.Sets
|
||
open import Categories.NaturalTransformation renaming (id to idN)
|
||
open import Categories.NaturalTransformation.NaturalIsomorphism
|
||
open import Categories.Functor.Core
|
||
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
|
||
open import Data.Unit.Polymorphic
|
||
|
||
-- The category 'G-Sets' is equivalent to the category [ G , Sets ]
|
||
|
||
module Category.G-Sets.Properties.Equivalence {ℓ} (G : Group ℓ) where
|
||
open StrongEquivalence renaming (G to H)
|
||
open WeakInverse renaming (F∘G≈id to F∘H≅id; G∘F≈id to H∘F≅id)
|
||
open Functor
|
||
open NaturalIsomorphism
|
||
G-Sets≅[G,Sets] : StrongEquivalence (G-Sets G) [ GroupAsCategory G , Sets ℓ ]
|
||
|
||
-- F : G-Sets → [ G , Sets ]
|
||
G-Sets≅[G,Sets] .F .F₀ GS = record
|
||
{ F₀ = λ _ → X
|
||
; F₁ = λ f x → f ⊳ x
|
||
; identity = ε⊳
|
||
; homomorphism = ∘⊳
|
||
; F-resp-≈ = λ f≡g {x} → ≡.cong (_⊳ x) f≡g
|
||
}
|
||
where open G-Set GS
|
||
G-Sets≅[G,Sets] .F .F₁ {A} {B} f = ntHelper (record { η = λ X x → f.u x ; commute = λ g → f.equivariance })
|
||
where
|
||
module f = G-Set-Morphism f
|
||
G-Sets≅[G,Sets] .F .identity = ≡.refl
|
||
G-Sets≅[G,Sets] .F .homomorphism = ≡.refl
|
||
G-Sets≅[G,Sets] .F .F-resp-≈ = λ x → x
|
||
|
||
-- H : [ G , Sets ] → G-Sets
|
||
G-Sets≅[G,Sets] .H .F₀ M = record
|
||
{ X = M.₀ tt
|
||
; _⊳_ = λ g x → (M.₁ g) x
|
||
; ε⊳ = M.identity
|
||
; ∘⊳ = M.homomorphism
|
||
}
|
||
where
|
||
module M = Functor M
|
||
G-Sets≅[G,Sets] .H .F₁ {M} {N} α = record
|
||
{ u = α.η tt
|
||
; equivariance = λ {g} {x} → α.commute g
|
||
}
|
||
where
|
||
module α = NaturalTransformation α
|
||
G-Sets≅[G,Sets] .H .identity = ≡.refl
|
||
G-Sets≅[G,Sets] .H .homomorphism = ≡.refl
|
||
G-Sets≅[G,Sets] .H .F-resp-≈ = λ x → x
|
||
|
||
-- F∘H = Id
|
||
G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .F⇒G = ntHelper (record
|
||
{ η = λ M → ntHelper (record
|
||
{ η = λ _ x → x
|
||
; commute = λ f {x} → ≡.refl
|
||
})
|
||
; commute = λ {M} {N} α {x} → ≡.refl
|
||
})
|
||
G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .F⇐G = ntHelper (record
|
||
{ η = λ M → ntHelper (record
|
||
{ η = λ _ x → x
|
||
; commute = λ f {x} → ≡.refl
|
||
})
|
||
; commute = λ {M} {N} α {x} → ≡.refl
|
||
})
|
||
G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .iso M = record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
|
||
|
||
-- H∘F = Id
|
||
G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .F⇒G = ntHelper (record
|
||
{ η = λ GS → record
|
||
{ u = λ x → x
|
||
; equivariance = ≡.refl
|
||
}
|
||
; commute = λ {GS} {GM} f {x} → ≡.refl
|
||
})
|
||
G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .F⇐G = ntHelper (record
|
||
{ η = λ GS → record
|
||
{ u = λ x → x
|
||
; equivariance = ≡.refl
|
||
}
|
||
; commute = λ {GS} {GM} f {x} → ≡.refl
|
||
})
|
||
G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .iso GS = record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
|