91 lines
3.3 KiB
Agda
91 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 }
|