Mercurial > hg > Members > kono > Proof > galois
annotate Solvable.agda @ 186:3c7e8855996f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 27 Nov 2020 20:54:55 +0900 |
| parents | 61310d395c1b |
| children | c22ef5bc695a |
| rev | line source |
|---|---|
| 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 |
| 70 | 12 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) |
| 5 | 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 | |
|
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
31 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
32 |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
33 deriving-subst : { i : ℕ } → {x y : Carrier } → x ≈ y → (dx : deriving i x ) → deriving i y |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
34 deriving-subst {zero} {x} {y} x=y dx = lift tt |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
35 deriving-subst {suc i} {x} {y} x=y dx = ccong x=y dx |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
75
diff
changeset
|
36 |
| 68 | 37 record solvable : Set (Level.suc n ⊔ m) where |
| 4 | 38 field |
| 39 dervied-length : ℕ | |
| 40 end : (x : Carrier ) → deriving dervied-length x → x ≈ ε | |
| 6 | 41 |
| 42 -- deriving stage is closed on multiplication and inversion | |
| 43 | |
| 44 import Relation.Binary.Reasoning.Setoid as EqReasoning | |
| 45 | |
| 122 | 46 open EqReasoning (Algebra.Group.setoid G) |
| 47 | |
| 8 | 48 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹ |
| 49 lemma4 g h = begin | |
| 50 [ h , g ] ≈⟨ grefl ⟩ | |
| 51 (h ⁻¹ ∙ g ⁻¹ ∙ h ) ∙ g ≈⟨ assoc _ _ _ ⟩ | |
| 52 h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6)) ⟩ | |
| 53 h ⁻¹ ∙ g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 _ _ ) ⟩ | |
| 54 h ⁻¹ ∙ g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹ ≈⟨ assoc _ _ _ ⟩ | |
| 55 h ⁻¹ ∙ (g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩ | |
| 56 h ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹ ∙ g) ⁻¹ ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩ | |
| 57 (g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h) ⁻¹ ≈⟨ grefl ⟩ | |
| 58 [ g , h ] ⁻¹ | |
| 122 | 59 ∎ |
| 6 | 60 |
| 61 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y ) | |
| 62 deriving-mul {zero} {x} {y} _ _ = lift tt | |
| 63 deriving-mul {suc i} {x} {y} ix iy = gen ix iy | |
| 64 | |
| 65 deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) | |
| 66 deriving-inv {zero} {x} (lift tt) = lift tt | |
| 67 deriving-inv {suc i} {ε} uni = ccong lemma3 uni | |
| 75 | 68 deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) |
| 69 deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) | |
| 6 | 70 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) |
| 71 | |
| 70 | 72 idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε |
| 73 idcomtr g = begin | |
| 74 (g ⁻¹ ∙ ε ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (∙-cong grefl (sym lemma3 )) grefl ) grefl ⟩ | |
| 75 (g ⁻¹ ∙ ε ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (proj₂ identity _) grefl) grefl ⟩ | |
| 76 (g ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (proj₁ inverse _ ) grefl ⟩ | |
| 77 ( ε ∙ ε ) ≈⟨ proj₂ identity _ ⟩ | |
| 78 ε | |
| 122 | 79 ∎ |
| 70 | 80 |
| 81 idcomtl : (g : Carrier ) → [ ε , g ] ≈ ε | |
| 82 idcomtl g = begin | |
| 83 (ε ⁻¹ ∙ g ⁻¹ ∙ ε ∙ g ) ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩ | |
| 84 (ε ⁻¹ ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (∙-cong (sym lemma3 ) grefl ) grefl ⟩ | |
| 85 (ε ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (proj₁ identity _) grefl ⟩ | |
| 86 (g ⁻¹ ∙ g ) ≈⟨ proj₁ inverse _ ⟩ | |
| 87 ε | |
| 122 | 88 ∎ |
| 121 | 89 |
| 186 | 90 deriving-ε : { i : ℕ } → deriving i ε |
| 91 deriving-ε {zero} = lift tt | |
| 92 deriving-ε {suc i} = ccong (idcomtr ε) (comm deriving-ε deriving-ε) | |
| 93 | |
| 122 | 94 comm-refl : {f g : Carrier } → f ≈ g → [ f , g ] ≈ ε |
| 95 comm-refl {f} {g} f=g = begin | |
| 96 f ⁻¹ ∙ g ⁻¹ ∙ f ∙ g | |
| 97 ≈⟨ ∙-cong (∙-cong (∙-cong (⁻¹-cong f=g ) grefl ) f=g ) grefl ⟩ | |
| 98 g ⁻¹ ∙ g ⁻¹ ∙ g ∙ g | |
| 99 ≈⟨ ∙-cong (assoc _ _ _ ) grefl ⟩ | |
| 100 g ⁻¹ ∙ (g ⁻¹ ∙ g ) ∙ g | |
| 101 ≈⟨ ∙-cong (∙-cong grefl (proj₁ inverse _) ) grefl ⟩ | |
| 102 g ⁻¹ ∙ ε ∙ g | |
| 103 ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩ | |
| 104 g ⁻¹ ∙ g | |
| 105 ≈⟨ proj₁ inverse _ ⟩ | |
| 106 ε | |
| 107 ∎ | |
| 121 | 108 |
| 122 | 109 comm-resp : {g h g1 h1 : Carrier } → g ≈ g1 → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] |
| 110 comm-resp {g} {h} {g1} {h1} g=g1 h=h1 = ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1 | |
| 111 |