Mercurial > hg > Members > kono > Proof > galois

comparison PermAbel.agda @ 0:dc677bac3c54

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Permutation group
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Aug 2020 11:03:37 +0900
parents
children 298dbf2b420d
comparison
equal deleted inserted replaced
-1:000000000000 0:dc677bac3c54
1 module PermAbel where
2
3 open import Level hiding ( suc ; zero )
4 open import Algebra
5 open import Algebra.Structures
6 open import Data.Fin
7 open import Data.Fin.Permutation
8 open import Function hiding (id ; flip)
9 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
10 open import Function.LeftInverse using ( _LeftInverseOf_ )
11 open import Function.Equality using (Π)
12 open import Data.Nat using (ℕ; suc; zero)
13 open import Relation.Binary.PropositionalEquality
14
15 f1 : Fin 3 → Fin 3
16 f1 zero = suc (suc zero)
17 f1 (suc zero) = zero
18 f1 (suc (suc zero)) = suc zero
19
20 lemma1 : Permutation 3 3
21 lemma1 = permutation f1 ( f1 ∘ f1 ) lemma2 where
22 lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
23 lemma3 zero = refl
24 lemma3 (suc zero) = refl
25 lemma3 (suc (suc zero)) = refl
26 lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
27 lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }
28
29 fid : {p : ℕ } → Fin p → Fin p
30 fid x = x
31
32 -- Data.Fin.Permutation.id
33 pid : {p : ℕ } → Permutation p p
34 pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
35
36 -- Data.Fin.Permutation.flip
37 pinv : {p : ℕ } → Permutation p p → Permutation p p
38 pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
39
40 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
41
42 PPP0 : {p : ℕ } (P : Permutation p p ) (x : Fin p) → (_⟨$⟩ˡ_ P) ((_⟨$⟩ʳ_ P) x) ≡ x
43 PPP0 P x = inverseˡ P
44
45 PPP1 : {p : ℕ } (P : Permutation p p ) (x : Fin p) → (_⟨$⟩ʳ_ P) ((_⟨$⟩ˡ_ P) x) ≡ x
46 PPP1 P x = inverseʳ P
47
48 Pp : {p : ℕ } → (P : Permutation p p ) → P ≡ permutation (_⟨$⟩ʳ_ P ) (_⟨$⟩ˡ_ P )
49 record { left-inverse-of = λ x → PPP0 P x ; right-inverse-of = λ x → PPP1 P x }
50 Pp P = {!!}
51
52 p-≅ : {p : ℕ } → {f0 g0 f1 g1 : Fin p → Fin p } → f0 ≡ f1 → g0 ≡ g1
53 → {fg0 : (x : Fin p ) → f0 (g0 x) ≡ x } → {fg1 : (x : Fin p ) → f1 (g1 x) ≡ x }
54 → {gf0 : (x : Fin p ) → g0 (f0 x) ≡ x } → {gf1 : (x : Fin p ) → g1 (f1 x) ≡ x }
55 → fg0 ≅ fg1 → gf0 ≅ gf1 → permutation f0 g0 record { left-inverse-of = gf0 ; right-inverse-of = fg0 }
56 ≡ permutation f1 g1 record { left-inverse-of = gf1 ; right-inverse-of = fg1 }
57 p-≅ refl refl HE.refl HE.refl = refl
58
59 p-≡ : {p : ℕ } → (x y : Permutation p p ) → (_⟨$⟩ˡ_ x) ≡ (_⟨$⟩ˡ_ y) → (_⟨$⟩ʳ_ x ) ≡ (_⟨$⟩ʳ_ y ) → x ≡ y
60 p-≡ _ _ refl refl = {!!}
61
62 pgroup : ℕ → AbelianGroup Level.zero Level.zero
63 pgroup p = record {
64 Carrier = Permutation p p
65 ; _≈_ = _≡_
66 ; _∙_ = _∘ₚ_
67 ; ε = pid
68 ; _⁻¹ = pinv
69 ; isAbelianGroup = record { isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
70 isEquivalence = record {refl = refl ; trans = trans ; sym = sym}
71 ; ∙-cong = presp }
72 ; assoc = passoc }
73 ; identity = {!!} }
74 ; inverse = {!!}
75 ; ⁻¹-cong = {!!}
76 } ; comm = {!!}
77 }
78 } where
79 presp : {x y u v : Permutation p p } → x ≡ y → u ≡ v → (x ∘ₚ u) ≡ (y ∘ₚ v)
80 presp refl refl = refl
81 passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) ≡ (x ∘ₚ (y ∘ₚ z))
82 passoc x y z = p-≡ _ _ refl refl
83
84