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