|
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
|
|
14
|
16 open import Gutil G
|
|
0
|
17
|
|
4
|
18 [_,_] : Carrier → Carrier → Carrier
|
|
|
19 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h
|
|
0
|
20
|
|
5
|
21 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
|
|
6
|
22 uni : Commutator P ε
|
|
|
23 comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ]
|
|
|
24 gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g )
|
|
|
25 ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
|
|
5
|
26
|
|
|
27 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
|
|
|
28 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
|
|
|
29 deriving (suc i) x = Commutator (deriving i) x
|
|
|
30
|
|
4
|
31 record Solvable : Set (Level.suc n ⊔ m) where
|
|
|
32 field
|
|
|
33 dervied-length : ℕ
|
|
|
34 end : (x : Carrier ) → deriving dervied-length x → x ≈ ε
|
|
6
|
35
|
|
|
36 -- deriving stage is closed on multiplication and inversion
|
|
|
37
|
|
|
38 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
39
|
|
8
|
40 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
|
|
|
41 lemma4 g h = begin
|
|
|
42 [ h , g ] ≈⟨ grefl ⟩
|
|
|
43 (h ⁻¹ ∙ g ⁻¹ ∙ h ) ∙ g ≈⟨ assoc _ _ _ ⟩
|
|
|
44 h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6)) ⟩
|
|
|
45 h ⁻¹ ∙ g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 _ _ ) ⟩
|
|
|
46 h ⁻¹ ∙ g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹ ≈⟨ assoc _ _ _ ⟩
|
|
|
47 h ⁻¹ ∙ (g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
|
|
|
48 h ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹ ∙ g) ⁻¹ ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
|
|
|
49 (g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h) ⁻¹ ≈⟨ grefl ⟩
|
|
|
50 [ g , h ] ⁻¹
|
|
|
51 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
6
|
52
|
|
|
53 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y )
|
|
|
54 deriving-mul {zero} {x} {y} _ _ = lift tt
|
|
|
55 deriving-mul {suc i} {x} {y} ix iy = gen ix iy
|
|
|
56
|
|
|
57 deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ )
|
|
|
58 deriving-inv {zero} {x} (lift tt) = lift tt
|
|
|
59 deriving-inv {suc i} {ε} uni = ccong lemma3 uni
|
|
|
60 deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) where
|
|
|
61 deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
|
|
|
62 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
|
|
|
63
|
