Show Universal Property
[darcs-mirror-agda-free-groups.git] / UnivProp.agda
1 module UnivProp where
2
3 open import FreeGroups
4 open import GroupHom
5 open import Relation.Binary
6 open import Algebra
7 open import Function.Equality hiding (cong)
8 open import Data.List
9 open import Generators
10 open import Data.Product hiding (map)
11 import Relation.Binary.EqReasoning as EqR
12
13 appGen : ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} → (f : A ⟶ Group.setoid B) → Gen (Setoid.Carrier A) → Group.Carrier B
14 appGen f (gen y) = f ⟨$⟩ y
15 appGen {B = B} f (gen-inv y) = (f ⟨$⟩ y)⁻¹ where open Group B
16
17 gConcat : ∀{c ℓ} → {B : Group c ℓ} → List (Group.Carrier B) → Group.Carrier B
18 gConcat {B = B} = foldr _∙_ ε where open Group B
19
20 [_]* : ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} → (f : A ⟶ Group.setoid B) → group A -Group→ B
21 [_]* {c} {ℓ} {A} {B} f = record {
22      ⟦_⟧ = f*;
23      ⟦⟧-cong = cong;
24      ∙-homo = homo  }
25      where
26      open Group (group A) renaming (_∙_ to _∙₁_; _≈_ to _≈₁_)
27      open Group B renaming (_∙_ to _∙₂_; _≈_ to _≈₂_; ∙-cong to ∙₂-cong;
28           refl to refl₂; sym to sym₂; assoc to assoc₂;
29           ε to ε₂; inverse to inverse₂; identity to identity₂)
30      f* : Word A → Group.Carrier B
31      f* = λ x → gConcat {B = B} (map (appGen {B = B} f) x)
32      
33      open EqR (Group.setoid B)
34
35      homo : (x y : Word A) → f* (x ∙₁ y) ≈₂ (f* x ∙₂ f* y)
36      homo [] y = Group.sym B (proj₁ (Group.identity B) _)
37      homo (x ∷ xs) y =
38        begin
39          f* ((x ∷ xs) ∙₁ y)
40        ≈⟨ refl₂ ⟩
41          appGen {B = B} f x ∙₂ f* (xs ∙₁ y)
42        ≈⟨ ∙₂-cong refl₂ (homo xs y)  ⟩
43          appGen {B = B} f x ∙₂ (f* xs ∙₂ f* y)
44        ≈⟨ sym₂ (assoc₂ _ _ _) ⟩
45          (appGen {B = B} f x ∙₂ f* xs) ∙₂ f* y
46        ≈⟨ refl₂ ⟩
47          f* (x ∷ xs) ∙₂ f* y
48        ∎
49
50      appGenCancel : ∀{x} → appGen {B = B} f (invert₁ x) ∙₂ appGen {B = B} f x ≈₂ ε₂
51      appGenCancel {gen y} = proj₁ inverse₂ _
52      appGenCancel {gen-inv y} = proj₂ inverse₂ _
53
54      cong' : {i j : Word A} → RedTo A i j → f* i ≈₂ f* j
55      cong' (reds xs x ys) =
56        begin
57          f* (xs ++ invert₁ x ∷ x ∷ ys)
58        ≈⟨ homo xs _ ⟩
59          f* xs ∙₂ f* (invert₁ x ∷ x ∷ ys)
60        ≈⟨ refl₂ ⟩
61          f* xs ∙₂ (appGen {B = B} f (invert₁ x) ∙₂ (appGen {B = B} f x ∙₂ f* ys))
62        ≈⟨ ∙₂-cong refl₂ (sym₂ (assoc₂ _ _ _)) ⟩
63          f* xs ∙₂ ((appGen {B = B} f (invert₁ x) ∙₂ appGen {B = B} f x) ∙₂ f* ys)
64        ≈⟨ ∙₂-cong refl₂ (∙₂-cong (appGenCancel {x}) refl₂) ⟩
65          f* xs ∙₂ (ε₂ ∙₂ f* ys)
66        ≈⟨ ∙₂-cong refl₂ (proj₁ identity₂ _) ⟩
67          f* xs ∙₂ f* ys
68        ≈⟨ Group.sym B (homo xs _) ⟩
69          f* (xs ++ ys)
70        ∎
71
72      cong : f* Preserves _≈₁_ ⟶ _≈₂_
73      cong = liftEqCl {B = Group.setoid B} {f = f*} cong'
74
75 lift-uniq :
76   ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} →
77   (f : A ⟶ Group.setoid B) → (h : group A -Group→ B) →
78   ((z : Setoid.Carrier A) → Group._≈_ B (_-Group→_.⟦_⟧ h [ gen z ]) (f ⟨$⟩ z)) →
79   (w : Word A) → Group._≈_ B (_-Group→_.⟦_⟧ h w) (_-Group→_.⟦_⟧ ([_]* {B = B} f) w)
80 lift-uniq f h eq [] = _-Group→_.ε-homo h
81 lift-uniq {A = A} {B = B} f h eq (x ∷ xs) =
82     begin
83       ⟦ x ∷ xs ⟧
84     ≈⟨ refl₂ ⟩
85       ⟦ [ x ] ∙₁ xs ⟧
86     ≈⟨ ∙-homo _ _ ⟩
87       ⟦ [ x ] ⟧ ∙₂ ⟦ xs ⟧
88     ≈⟨ ∙₂-cong (lift-uniq-1 x) (lift-uniq f h eq xs) ⟩
89       f⟦ [ x ] ⟧ ∙₂ f⟦ xs ⟧
90     ≈⟨ sym₂ (∙₂-homo [ x ] xs) ⟩
91       f⟦ x ∷ xs ⟧
92     ∎
93   where
94      open Group B renaming (_∙_ to _∙₂_; _≈_ to _≈₂_; ∙-cong to ∙₂-cong;
95           refl to refl₂; sym to sym₂; assoc to assoc₂; trans to trans₂;
96           ε to ε₂; inverse to inverse₂; identity to identity₂)
97      open Group (group A) using () renaming (_∙_ to _∙₁_; _≈_ to _≈₁_; _⁻¹ to _⁻¹₁)
98      open EqR (Group.setoid B)
99      open _-Group→_ h
100      open _-Group→_ ([_]* {B = B} f) using () renaming
101        (⟦_⟧ to f⟦_⟧; ∙-homo to ∙₂-homo; ⟦⟧-cong to f⟦⟧-cong; ⁻¹-homo to ⁻¹₂-homo)
102  
103      lift-uniq-gen : ∀ x →  ⟦ [ gen x ] ⟧ ≈₂ f⟦ [ gen x ] ⟧
104      lift-uniq-gen y = trans₂ (eq y) (sym₂ (proj₂ identity₂ (f ⟨$⟩ y)))
105   
106      lift-uniq-1 : ∀ x →  ⟦ [ x ] ⟧ ≈₂ f⟦ [ x ] ⟧
107      lift-uniq-1 (gen y) = lift-uniq-gen y
108      lift-uniq-1 (gen-inv y) = begin 
109        ⟦ [ gen y ] ⁻¹₁ ⟧ 
110          ≈⟨ ⁻¹-homo _ ⟩
111        ⟦ [ gen y ] ⟧ ⁻¹ 
112          ≈⟨ ⁻¹-cong (lift-uniq-gen y) ⟩
113        f⟦ [ gen y ] ⟧ ⁻¹ 
114          ≈⟨ sym₂ (⁻¹₂-homo [ gen y ]) ⟩
115        f⟦ [ gen y ] ⁻¹₁ ⟧ 
116        ∎
117
118