0
|
1 open import Level hiding ( suc ; zero )
|
|
2 open import Algebra
|
4
|
3 module Solvable {n m : Level} (G : Group n m ) where
|
0
|
4
|
4
|
5 open import Data.Unit
|
|
6 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
6
|
7 open import Function
|
7
|
8 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
4
|
9 open import Relation.Nullary
|
|
10 open import Data.Empty
|
5
|
11 open import Data.Product
|
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
13
|
0
|
14
|
4
|
15 open Group G
|
0
|
16
|
4
|
17 [_,_] : Carrier → Carrier → Carrier
|
|
18 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h
|
0
|
19
|
5
|
20 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
|
6
|
21 uni : Commutator P ε
|
|
22 comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ]
|
|
23 gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g )
|
|
24 ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
|
5
|
25
|
|
26 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
|
|
27 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
|
|
28 deriving (suc i) x = Commutator (deriving i) x
|
|
29
|
4
|
30 record Solvable : Set (Level.suc n ⊔ m) where
|
|
31 field
|
|
32 dervied-length : ℕ
|
|
33 end : (x : Carrier ) → deriving dervied-length x → x ≈ ε
|
6
|
34
|
|
35 -- deriving stage is closed on multiplication and inversion
|
|
36
|
|
37 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
38
|
|
39 gsym = Algebra.Group.sym G
|
|
40 grefl = Algebra.Group.refl G
|
8
|
41
|
6
|
42 lemma3 : ε ≈ ε ⁻¹
|
|
43 lemma3 = begin
|
|
44 ε ≈⟨ gsym (proj₁ inverse _) ⟩
|
|
45 ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
|
|
46 ε ⁻¹
|
|
47 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
48
|
8
|
49 lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f
|
|
50 lemma6 {f} = begin
|
|
51 ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩
|
|
52 ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
|
|
53 (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩
|
|
54 f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
|
|
55 f ∙ ε ≈⟨ proj₂ identity _ ⟩
|
|
56 f
|
|
57 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
6
|
58
|
9
|
59 data MP : Carrier → Set (Level.suc n) where
|
|
60 am : (x : Carrier ) → MP x
|
|
61 _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y )
|
|
62
|
|
63 mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
|
|
64 mpf {x} (am x) y = x ∙ y
|
|
65 mpf (m o m₁) y = mpf m ( mpf m₁ y )
|
|
66
|
|
67 mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
|
|
68 mp-flatten {x} m = mpf {x} m ε
|
|
69
|
|
70 ∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
|
|
71 ∙-flatten {x} (am x) = gsym (proj₂ identity _)
|
|
72 ∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
|
10
|
73 ∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) with ∙-flatten (p o q ) -- t : x ∙ y ≈ mpf p (mpf q ε)
|
|
74 ... | t = begin
|
|
75 x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩
|
|
76 mpf p (mpf q ε) ∙ z ≈⟨ {!!} ⟩
|
|
77 mpf p (mpf q (mpf r ε))
|
|
78 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
9
|
79
|
|
80
|
8
|
81 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
|
|
82 lemma5 f g = begin
|
|
83 g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩
|
|
84 g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
|
|
85 g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ assoc _ _ _ ⟩
|
|
86 g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g ∙ (f ∙ g) ⁻¹)) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _)) ⟩
|
|
87 g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹) ≈⟨ gsym ( assoc _ _ _) ⟩
|
|
88 g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩
|
|
89 (g ⁻¹ ∙ f ⁻¹) ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (assoc _ _ _ ) grefl ⟩
|
|
90 (g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g))) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl (gsym (assoc _ _ _ )) ) grefl ⟩
|
|
91 (g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩
|
|
92 (g ⁻¹ ∙ (f ⁻¹ ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (assoc _ _ _) grefl ⟩
|
|
93 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl (∙-cong (proj₁ inverse _ ) grefl )) grefl ⟩
|
|
94 g ⁻¹ ∙ (ε ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl ( proj₁ identity _) ) grefl ⟩
|
|
95 g ⁻¹ ∙ g ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (proj₁ inverse _) grefl ⟩
|
|
96 ε ∙ (f ∙ g) ⁻¹ ≈⟨ proj₁ identity _ ⟩
|
|
97 (f ∙ g) ⁻¹
|
|
98 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
6
|
99
|
8
|
100 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
|
|
101 lemma4 g h = begin
|
|
102 [ h , g ] ≈⟨ grefl ⟩
|
|
103 (h ⁻¹ ∙ g ⁻¹ ∙ h ) ∙ g ≈⟨ assoc _ _ _ ⟩
|
|
104 h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6)) ⟩
|
|
105 h ⁻¹ ∙ g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 _ _ ) ⟩
|
|
106 h ⁻¹ ∙ g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹ ≈⟨ assoc _ _ _ ⟩
|
|
107 h ⁻¹ ∙ (g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
|
|
108 h ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹ ∙ g) ⁻¹ ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
|
|
109 (g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h) ⁻¹ ≈⟨ grefl ⟩
|
|
110 [ g , h ] ⁻¹
|
|
111 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
6
|
112
|
|
113 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y )
|
|
114 deriving-mul {zero} {x} {y} _ _ = lift tt
|
|
115 deriving-mul {suc i} {x} {y} ix iy = gen ix iy
|
|
116
|
|
117 deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ )
|
|
118 deriving-inv {zero} {x} (lift tt) = lift tt
|
|
119 deriving-inv {suc i} {ε} uni = ccong lemma3 uni
|
|
120 deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) where
|
|
121 deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
|
|
122 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
|
|
123
|