open import Relation.Binary open import Level module FreeGroups {c ℓ} (S : Setoid c ℓ) where open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; inspect) import Relation.Binary.List.Pointwise as LP import Relation.Binary.EqReasoning open import Data.Product hiding (map) open import Function open import Relation.Binary import Data.Bool open import Data.List open import Data.List.Properties open import Relation.Nullary open import Relation.Nullary.Negation open import Data.Empty import Algebra.FunctionProperties as FP open import Algebra open import Generators -- -- G is the set of generators (and their inverses) -- Word are the elements of the free group -- G : Set c G = Setoid.Carrier (setoid S) Word : Set c Word = List G -- -- We define a reduction relation, representing the cancellation -- of two adjacent elements in a word. -- data RedTo : Rel Word c where reds : (xs : Word) → (x : G) → (ys : Word) → RedTo (xs ++ invert₁ x ∷ x ∷ ys) (xs ++ ys) -- -- This cancellation is respected by list concatenation. -- lem-++-red1 : (zs : Word) → RedTo =[ (λ xs → xs ++ zs) ]⇒ RedTo lem-++-red1 zs (reds xs x ys) = P.subst₂ RedTo (P.sym (Monoid.assoc (monoid G) xs (invert₁ x ∷ x ∷ ys) zs)) (P.sym (Monoid.assoc (monoid G) xs ys zs)) (reds xs x (ys ++ zs)) lem-++-red2 : (zs : Word) → RedTo =[ (λ xs → zs ++ xs) ]⇒ RedTo lem-++-red2 zs (reds xs x ys) = P.subst₂ RedTo (Monoid.assoc (monoid G) zs xs (invert₁ x ∷ x ∷ ys)) (Monoid.assoc (monoid G) zs xs ys) (reds (zs ++ xs) x ys) -- -- The equivalence relation that the free groups are based on is -- the equivalence hull of the reduction relation. -- _≈f_ : Rel (Word) _ _≈f_ = EqCl RedTo -- -- Inverting a word, which is involutive, commutes with append -- and respected the reduction relation -- inv : Word → Word inv x = reverse (Data.List.map invert₁ x) inv-inv : FP.Involutive _≡_ inv inv-inv x = begin inv (inv x) ≡⟨ P.cong reverse (reverse-map-commute invert₁ (map invert₁ x)) ⟩ reverse (reverse (map invert₁ (map invert₁ x))) ≡⟨ reverse-inv (map invert₁ (map invert₁ x)) ⟩ map invert₁ (map invert₁ x) ≡⟨ P.sym (map-compose x) ⟩ map (invert₁ ∘ invert₁) x ≡⟨ map-cong invert₁-inv x ⟩ map id x ≡⟨ map-id x ⟩ x ∎ where open P.≡-Reasoning inv-++-commute : (xs ys : Word) → (inv ys ++ inv xs ≡ inv (xs ++ ys)) inv-++-commute xs ys = begin inv ys ++ inv xs ≡⟨ P.sym (reverse-++-commute (map invert₁ xs) (map invert₁ ys)) ⟩ reverse (map invert₁ xs ++ map invert₁ ys) ≡⟨ P.sym (P.cong reverse (map-++-commute invert₁ xs ys)) ⟩ inv (xs ++ ys) ∎ where open P.≡-Reasoning lem-inv-red : RedTo =[ inv ]⇒ RedTo lem-inv-red (reds xs x ys) = P.subst₂ RedTo p1 p2 (reds (inv ys) x (inv xs)) where open P.≡-Reasoning p1 = begin inv ys ++ invert₁ x ∷ x ∷ inv xs ≡⟨ P.sym \$ P.cong (λ y → inv ys ++ invert₁ x ∷ y ∷ inv xs) \$ invert₁-inv x ⟩ inv ys ++ invert₁ x ∷ invert₁ (invert₁ x) ∷ inv xs ≡⟨ P.sym \$ Monoid.assoc (monoid G) (inv ys) [ invert₁ x ] \$ invert₁ (invert₁ x) ∷ inv xs ⟩ (inv ys ++ [ invert₁ x ]) ++ invert₁ (invert₁ x) ∷ inv xs ≡⟨ P.cong (λ y → y ++ invert₁ (invert₁ x) ∷ inv xs) \$ inv-++-commute [ x ] ys ⟩ inv (x ∷ ys) ++ invert₁ (invert₁ x) ∷ inv xs ≡⟨ P.sym \$ Monoid.assoc (monoid G) (inv (x ∷ ys)) [ invert₁ (invert₁ x)] (inv xs) ⟩ (inv (x ∷ ys) ++ [ invert₁ (invert₁ x) ]) ++ inv xs ≡⟨ P.cong (λ y → y ++ inv xs) \$ inv-++-commute [ invert₁ x ] (x ∷ ys) ⟩ inv (invert₁ x ∷ x ∷ ys) ++ inv xs ≡⟨ inv-++-commute xs (invert₁ x ∷ x ∷ ys) ⟩ inv (xs ++ invert₁ x ∷ x ∷ ys) ∎ p2 = inv-++-commute xs ys -- -- Here, we define the actual group and check the group axioms -- group : Group _ _ group = record { Carrier = Word; _≈_ = _≈f_; _∙_ = _++_; ε = []; _⁻¹ = inv; isGroup = record { isMonoid = record { isSemigroup = record { isEquivalence = L.isEquivalence; assoc = λ x y z → L.reflexive (Monoid.assoc (monoid G) x y z); ∙-cong = cong1 }; identity = (λ x → L.refl) , (λ x → L.reflexive (proj₂ (Monoid.identity (monoid G)) x)) }; inverse = linv , rinv; ⁻¹-cong = mapEq lem-inv-red } } where module L = Setoid (eqSetoid RedTo) cong1 : {x y u v : Word} → x ≈f y → u ≈f v → (x ++ u) ≈f (y ++ v) cong1 {x} {y} {u} {v} p1 p2 = begin x ++ u ≈⟨ mapEq (lem-++-red1 u) p1 ⟩ y ++ u ≈⟨ mapEq (lem-++-red2 y) p2 ⟩ y ++ v ∎ where open Relation.Binary.EqReasoning (eqSetoid RedTo) linv : FP.LeftInverse _≈f_ [] inv _++_ linv [] = reflEq linv (x ∷ xs) = begin inv (x ∷ xs) ++ x ∷ xs ≡⟨ P.sym (P.cong (λ y → y ++ x ∷ xs) (inv-++-commute [ x ] xs)) ⟩ (inv xs ++ [ invert₁ x ]) ++ x ∷ xs ≡⟨ Monoid.assoc (monoid G) (inv xs) [ invert₁ x ] (x ∷ xs) ⟩ inv xs ++ invert₁ x ∷ x ∷ xs ≈⟨ impEq (reds (inv xs) x xs) ⟩ inv xs ++ xs ≈⟨ linv xs ⟩ [] ∎ where open Relation.Binary.EqReasoning (eqSetoid RedTo) rinv : FP.RightInverse _≈f_ [] inv _++_ rinv x = begin x ++ inv x ≡⟨ P.cong (λ y → y ++ inv x) (P.sym (inv-inv x)) ⟩ inv (inv x) ++ inv x ≈⟨ linv (inv x) ⟩ [] ∎ where open Relation.Binary.EqReasoning (eqSetoid RedTo)