48 lines
1.7 KiB
Agda
48 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'
|