-- 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 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.
--- /dev/null
+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.ε
+ ∎)
--- /dev/null
+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
projects / darcs-mirror-agda-free-groups.git / commitdiff