49 lines
1.7 KiB
Agda
49 lines
1.7 KiB
Agda
|
open import Algebra.G-Set
|
|||
|
|
open import Algebra.Group
|
|||
|
|
open import Category.G-Sets
|
|||
|
|
open import Categories.FreeObjects.Free
|
|||
|
|
open import Categories.Functor.Core
|
|||
|
|
open import Categories.Category.Instance.Sets
|
|||
|
|
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
|
|||
|
|
open import Data.Product
|
|||
|
|
|
|||
|
|
-- The category G-Sets has free objects
|
|||
|
|
|
|||
|
|
module Category.G-Sets.Properties.FreeObject {ℓ} (G : Group ℓ) where
|
|||
|
|
open Group using () renaming (Carrier to ∣_∣)
|
|||
|
|
open G-Set using () renaming (X to ∣_∣)
|
|||
|
|
open G-Set-Morphism using () renaming (u to <_>)
|
|||
|
|
open FreeObject
|
|||
|
|
open Group G hiding (Carrier)
|
|||
|
|
|
|||
|
|
forgetfulF : Functor (G-Sets G) (Sets ℓ)
|
|||
|
|
forgetfulF = record
|
|||
|
|
{ F₀ = λ GS → ∣ GS ∣
|
|||
|
|
; F₁ = λ f → < f >
|
|||
|
|
; identity = ≡.refl
|
|||
|
|
; homomorphism = ≡.refl
|
|||
|
|
; F-resp-≈ = λ x → x
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
free-G-Set : ∀ {X : Set ℓ} → FreeObject forgetfulF X
|
|||
|
|
free-G-Set {X} .FX = record
|
|||
|
|
{ X = ∣ G ∣ × X
|
|||
|
|
; _⊳_ = λ g (h , x) → (g ∙ h , x)
|
|||
|
|
; ε⊳ = λ {(g , x)} → ≡.cong (_, x) idˡ
|
|||
|
|
; ∘⊳ = λ {g} {h} {(f , x)} → ≡.cong (_, x) assoc
|
|||
|
|
}
|
|||
|
|
free-G-Set .η x = (ε , x)
|
|||
|
|
free-G-Set {X} ._* {GS} f = record
|
|||
|
|
{ u = λ (g , x) → g ⊳ f x
|
|||
|
|
; equivariance = λ {g} {x} → ∘⊳
|
|||
|
|
}
|
|||
|
|
where open G-Set GS
|
|||
|
|
free-G-Set {X} .*-lift {GS} f {x} = ε⊳
|
|||
|
|
where open G-Set GS
|
|||
|
|
free-G-Set {X} .*-uniq {GS} f f' g-prop {(h , y)} = ≡.trans (≡.cong < f' > (≡.cong (_, y) (≡.sym idʳ)) )
|
|||
|
|
(≡.trans (f'.equivariance)
|
|||
|
|
(≡.cong (h ⊳_) g-prop))
|
|||
|
|
where
|
|||
|
|
open G-Set GS
|
|||
|
|
module f' = G-Set-Morphism f'
|