Show Universal Property master
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 11 Sep 2012 15:19:58 +0000 (15:19 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 11 Sep 2012 15:19:58 +0000 (15:19 +0000)
FreeGroups.agda
Generators.agda
GroupHom.agda [new file with mode: 0644]
UnivProp.agda [new file with mode: 0644]

index 6dce2b5..7aee5fe 100644 (file)
@@ -175,4 +175,4 @@ group = record {
     inv (inv x) ++ inv x
       ≈⟨ linv (inv x) ⟩
     [] ∎
     inv (inv x) ++ inv x
       ≈⟨ linv (inv x) ⟩
     [] ∎
-    where open  Relation.Binary.EqReasoning (eqSetoid RedTo)
+    where open  Relation.Binary.EqReasoning (eqSetoid RedTo)
\ No newline at end of file
index 88cefd6..b2c95c3 100644 (file)
@@ -112,13 +112,15 @@ eqSetoid  _⟶_ = record {
 -- reflexive symmetric hull.
 --
 
 -- reflexive symmetric hull.
 --
 
+liftEqCl : ∀{c d ℓ ℓ2} → {A : Set c} → {B : Setoid d ℓ} → {T : Rel A ℓ2} → {f : A → Setoid.Carrier B } → T =[ f ]⇒ Setoid._≈_ B → EqCl T =[ f ]⇒ Setoid._≈_ B
+liftEqCl p (impEq y) = p y
+liftEqCl {B = B} p (symEq y) = Setoid.sym B (liftEqCl {B = B} p y)
+liftEqCl {B = B} p reflEq = Setoid.refl B
+liftEqCl {B = B} p (transEq y y') = Setoid.trans B (liftEqCl {B = B} p y) (liftEqCl {B = B} p y')
+
 mapEq : ∀{ℓ} → {A : Set ℓ} → {T : Rel A ℓ} → {f : A → A } →
       T =[ f ]⇒ T → EqCl T =[ f ]⇒ EqCl T
 mapEq : ∀{ℓ} → {A : Set ℓ} → {T : Rel A ℓ} → {f : A → A } →
       T =[ f ]⇒ T → EqCl T =[ f ]⇒ EqCl T
-mapEq p (impEq y) = impEq (p y)
-mapEq p (symEq y) = symEq (mapEq p y)
-mapEq p reflEq = reflEq
-mapEq p (transEq y' y0) = transEq (mapEq p y') (mapEq p y0)
-
+mapEq {T = T} p = liftEqCl {B = eqSetoid T} (impEq ∘ p)
 
 --
 -- Utility lemmata that went into the standard library, but has not released yet.
 
 --
 -- Utility lemmata that went into the standard library, but has not released yet.
diff --git a/GroupHom.agda b/GroupHom.agda
new file mode 100644 (file)
index 0000000..2b74ca9
--- /dev/null
@@ -0,0 +1,41 @@
+module GroupHom where
+
+open import Algebra.Morphism
+open import Algebra
+open import Level
+open import Relation.Binary
+import Algebra.Props.Group as GroupP
+import Relation.Binary.EqReasoning as EqR
+open import Data.Product
+
+record _-Group→_ {r₁ r₂ r₃ r₄}
+                (From : Group r₁ r₂) (To : Group r₃ r₄) :
+                Set (r₁ ⊔ r₂ ⊔ r₃ ⊔ r₄) where
+  private
+    module F = Group From
+    module T = Group To
+  open Definitions F.Carrier T.Carrier T._≈_
+
+  field
+    ⟦_⟧     : Morphism
+    ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
+    ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
+
+  open EqR T.setoid
+
+  ε-homo :  Homomorphic₀ ⟦_⟧ F.ε T.ε
+  ε-homo = GroupP.left-identity-unique To ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin
+      T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo _ _) ⟩
+      ⟦ F._∙_ _ _ ⟧         ≈⟨ ⟦⟧-cong (proj₁ F.identity _) ⟩
+      ⟦ F.ε ⟧                ∎)
+
+  ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
+  ⁻¹-homo x = GroupP.left-inverse-unique To ⟦ F._⁻¹ x  ⟧ ⟦ x ⟧ (begin
+    T._∙_ ⟦ F._⁻¹ x ⟧ ⟦ x ⟧
+      ≈⟨ T.sym (∙-homo _ _) ⟩
+    ⟦ F._∙_ (F._⁻¹ x) x ⟧
+      ≈⟨ ⟦⟧-cong (proj₁ F.inverse _) ⟩
+    ⟦ F.ε ⟧
+      ≈⟨ ε-homo ⟩
+    T.ε
+    ∎)
diff --git a/UnivProp.agda b/UnivProp.agda
new file mode 100644 (file)
index 0000000..41de3ef
--- /dev/null
@@ -0,0 +1,118 @@
+module UnivProp where
+
+open import FreeGroups
+open import GroupHom
+open import Relation.Binary
+open import Algebra
+open import Function.Equality hiding (cong)
+open import Data.List
+open import Generators
+open import Data.Product hiding (map)
+import Relation.Binary.EqReasoning as EqR
+
+appGen : ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} → (f : A ⟶ Group.setoid B) → Gen (Setoid.Carrier A) → Group.Carrier B
+appGen f (gen y) = f ⟨$⟩ y
+appGen {B = B} f (gen-inv y) = (f ⟨$⟩ y)⁻¹ where open Group B
+
+gConcat : ∀{c ℓ} → {B : Group c ℓ} → List (Group.Carrier B) → Group.Carrier B
+gConcat {B = B} = foldr _∙_ ε where open Group B
+
+[_]* : ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} → (f : A ⟶ Group.setoid B) → group A -Group→ B
+[_]* {c} {ℓ} {A} {B} f = record {
+     ⟦_⟧ = f*;
+     ⟦⟧-cong = cong;
+     ∙-homo = homo  }
+     where
+     open Group (group A) renaming (_∙_ to _∙₁_; _≈_ to _≈₁_)
+     open Group B renaming (_∙_ to _∙₂_; _≈_ to _≈₂_; ∙-cong to ∙₂-cong;
+          refl to refl₂; sym to sym₂; assoc to assoc₂;
+          ε to ε₂; inverse to inverse₂; identity to identity₂)
+     f* : Word A → Group.Carrier B
+     f* = λ x → gConcat {B = B} (map (appGen {B = B} f) x)
+     
+     open EqR (Group.setoid B)
+
+     homo : (x y : Word A) → f* (x ∙₁ y) ≈₂ (f* x ∙₂ f* y)
+     homo [] y = Group.sym B (proj₁ (Group.identity B) _)
+     homo (x ∷ xs) y =
+       begin
+         f* ((x ∷ xs) ∙₁ y)
+       ≈⟨ refl₂ ⟩
+         appGen {B = B} f x ∙₂ f* (xs ∙₁ y)
+       ≈⟨ ∙₂-cong refl₂ (homo xs y)  ⟩
+         appGen {B = B} f x ∙₂ (f* xs ∙₂ f* y)
+       ≈⟨ sym₂ (assoc₂ _ _ _) ⟩
+         (appGen {B = B} f x ∙₂ f* xs) ∙₂ f* y
+       ≈⟨ refl₂ ⟩
+         f* (x ∷ xs) ∙₂ f* y
+       ∎
+
+     appGenCancel : ∀{x} → appGen {B = B} f (invert₁ x) ∙₂ appGen {B = B} f x ≈₂ ε₂
+     appGenCancel {gen y} = proj₁ inverse₂ _
+     appGenCancel {gen-inv y} = proj₂ inverse₂ _
+
+     cong' : {i j : Word A} → RedTo A i j → f* i ≈₂ f* j
+     cong' (reds xs x ys) =
+       begin
+         f* (xs ++ invert₁ x ∷ x ∷ ys)
+       ≈⟨ homo xs _ ⟩
+         f* xs ∙₂ f* (invert₁ x ∷ x ∷ ys)
+       ≈⟨ refl₂ ⟩
+         f* xs ∙₂ (appGen {B = B} f (invert₁ x) ∙₂ (appGen {B = B} f x ∙₂ f* ys))
+       ≈⟨ ∙₂-cong refl₂ (sym₂ (assoc₂ _ _ _)) ⟩
+         f* xs ∙₂ ((appGen {B = B} f (invert₁ x) ∙₂ appGen {B = B} f x) ∙₂ f* ys)
+       ≈⟨ ∙₂-cong refl₂ (∙₂-cong (appGenCancel {x}) refl₂) ⟩
+         f* xs ∙₂ (ε₂ ∙₂ f* ys)
+       ≈⟨ ∙₂-cong refl₂ (proj₁ identity₂ _) ⟩
+         f* xs ∙₂ f* ys
+       ≈⟨ Group.sym B (homo xs _) ⟩
+         f* (xs ++ ys)
+       ∎
+
+     cong : f* Preserves _≈₁_ ⟶ _≈₂_
+     cong = liftEqCl {B = Group.setoid B} {f = f*} cong'
+
+lift-uniq :
+  ∀{c ℓ} → {A : Setoid c ℓ} → {B : Group c ℓ} →
+  (f : A ⟶ Group.setoid B) → (h : group A -Group→ B) →
+  ((z : Setoid.Carrier A) → Group._≈_ B (_-Group→_.⟦_⟧ h [ gen z ]) (f ⟨$⟩ z)) →
+  (w : Word A) → Group._≈_ B (_-Group→_.⟦_⟧ h w) (_-Group→_.⟦_⟧ ([_]* {B = B} f) w)
+lift-uniq f h eq [] = _-Group→_.ε-homo h
+lift-uniq {A = A} {B = B} f h eq (x ∷ xs) =
+    begin
+      ⟦ x ∷ xs ⟧
+    ≈⟨ refl₂ ⟩
+      ⟦ [ x ] ∙₁ xs ⟧
+    ≈⟨ ∙-homo _ _ ⟩
+      ⟦ [ x ] ⟧ ∙₂ ⟦ xs ⟧
+    ≈⟨ ∙₂-cong (lift-uniq-1 x) (lift-uniq f h eq xs) ⟩
+      f⟦ [ x ] ⟧ ∙₂ f⟦ xs ⟧
+    ≈⟨ sym₂ (∙₂-homo [ x ] xs) ⟩
+      f⟦ x ∷ xs ⟧
+    ∎
+  where
+     open Group B renaming (_∙_ to _∙₂_; _≈_ to _≈₂_; ∙-cong to ∙₂-cong;
+          refl to refl₂; sym to sym₂; assoc to assoc₂; trans to trans₂;
+          ε to ε₂; inverse to inverse₂; identity to identity₂)
+     open Group (group A) using () renaming (_∙_ to _∙₁_; _≈_ to _≈₁_; _⁻¹ to _⁻¹₁)
+     open EqR (Group.setoid B)
+     open _-Group→_ h
+     open _-Group→_ ([_]* {B = B} f) using () renaming
+       (⟦_⟧ to f⟦_⟧; ∙-homo to ∙₂-homo; ⟦⟧-cong to f⟦⟧-cong; ⁻¹-homo to ⁻¹₂-homo)
+     lift-uniq-gen : ∀ x →  ⟦ [ gen x ] ⟧ ≈₂ f⟦ [ gen x ] ⟧
+     lift-uniq-gen y = trans₂ (eq y) (sym₂ (proj₂ identity₂ (f ⟨$⟩ y)))
+  
+     lift-uniq-1 : ∀ x →  ⟦ [ x ] ⟧ ≈₂ f⟦ [ x ] ⟧
+     lift-uniq-1 (gen y) = lift-uniq-gen y
+     lift-uniq-1 (gen-inv y) = begin 
+       ⟦ [ gen y ] ⁻¹₁ ⟧ 
+         ≈⟨ ⁻¹-homo _ ⟩
+       ⟦ [ gen y ] ⟧ ⁻¹ 
+         ≈⟨ ⁻¹-cong (lift-uniq-gen y) ⟩
+       f⟦ [ gen y ] ⟧ ⁻¹ 
+         ≈⟨ sym₂ (⁻¹₂-homo [ gen y ]) ⟩
+       f⟦ [ gen y ] ⁻¹₁ ⟧ 
+       ∎
+
+  
\ No newline at end of file