|
4
|
1 module PermGroup where
|
|
0
|
2
|
|
|
3 open import Level hiding ( suc ; zero )
|
|
|
4 open import Algebra
|
|
|
5 open import Algebra.Structures
|
|
|
6 open import Data.Fin
|
|
3
|
7 open import Data.Product
|
|
0
|
8 open import Data.Fin.Permutation
|
|
|
9 open import Function hiding (id ; flip)
|
|
|
10 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
11 open import Function.LeftInverse using ( _LeftInverseOf_ )
|
|
|
12 open import Function.Equality using (Π)
|
|
|
13 open import Data.Nat using (ℕ; suc; zero)
|
|
|
14 open import Relation.Binary.PropositionalEquality
|
|
|
15
|
|
|
16 f1 : Fin 3 → Fin 3
|
|
|
17 f1 zero = suc (suc zero)
|
|
|
18 f1 (suc zero) = zero
|
|
|
19 f1 (suc (suc zero)) = suc zero
|
|
|
20
|
|
|
21 lemma1 : Permutation 3 3
|
|
|
22 lemma1 = permutation f1 ( f1 ∘ f1 ) lemma2 where
|
|
|
23 lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
|
|
|
24 lemma3 zero = refl
|
|
|
25 lemma3 (suc zero) = refl
|
|
|
26 lemma3 (suc (suc zero)) = refl
|
|
|
27 lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
|
|
|
28 lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }
|
|
|
29
|
|
|
30 fid : {p : ℕ } → Fin p → Fin p
|
|
|
31 fid x = x
|
|
|
32
|
|
|
33 -- Data.Fin.Permutation.id
|
|
|
34 pid : {p : ℕ } → Permutation p p
|
|
|
35 pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
|
|
|
36
|
|
|
37 -- Data.Fin.Permutation.flip
|
|
|
38 pinv : {p : ℕ } → Permutation p p → Permutation p p
|
|
|
39 pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
|
|
|
40
|
|
3
|
41 record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where
|
|
|
42 field
|
|
|
43 peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
|
|
0
|
44
|
|
3
|
45 open _=p=_
|
|
0
|
46
|
|
3
|
47 prefl : {p : ℕ } { x : Permutation p p } → x =p= x
|
|
|
48 peq (prefl {p} {x}) q = refl
|
|
1
|
49
|
|
3
|
50 psym : {p : ℕ } { x y : Permutation p p } → x =p= y → y =p= x
|
|
|
51 peq (psym {p} {x} {y} eq ) q = sym (peq eq q)
|
|
1
|
52
|
|
3
|
53 ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y → y =p= z → x =p= z
|
|
|
54 peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
|
|
0
|
55
|
|
4
|
56 Pgroup : ℕ → Group Level.zero Level.zero
|
|
|
57 Pgroup p = record {
|
|
0
|
58 Carrier = Permutation p p
|
|
3
|
59 ; _≈_ = _=p=_
|
|
0
|
60 ; _∙_ = _∘ₚ_
|
|
|
61 ; ε = pid
|
|
|
62 ; _⁻¹ = pinv
|
|
3
|
63 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
64 isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
|
|
0
|
65 ; ∙-cong = presp }
|
|
|
66 ; assoc = passoc }
|
|
3
|
67 ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } )) }
|
|
|
68 ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))
|
|
|
69 ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q }
|
|
0
|
70 }
|
|
|
71 } where
|
|
3
|
72 presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
|
|
|
73 presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
|
|
|
74 lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
|
|
|
75 lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
|
|
|
76 passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z))
|
|
|
77 passoc x y z = record { peq = λ q → refl }
|
|
|
78 p-inv : {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
|
|
|
79 p-inv {i} {j} i=j q = begin
|
|
4
|
80 i ⟨$⟩ˡ q ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩
|
|
|
81 i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩
|
|
|
82 i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i ⟩
|
|
|
83 j ⟨$⟩ˡ q
|
|
3
|
84 ∎ where open ≡-Reasoning
|
|
0
|
85
|
|
|
86
|
