Mercurial > hg > Members > kono > Proof > galois

changeset 295:cc81d3b1a82a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Sep 2023 16:44:24 +0900
parents e153b9a96665
children 7c1e3e0be315
files src/Solvable.agda
diffstat 1 files changed, 27 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/Solvable.agda	Sat Sep 02 14:44:32 2023 +0900
+++ b/src/Solvable.agda	Sat Sep 02 16:44:24 2023 +0900
@@ -139,8 +139,10 @@
 -- so we have to use finite products of commutators
 
 data iCommutator (i : ℕ) : (j : ℕ) → Carrier → Set (Level.suc n ⊔ m) where
-  iunit : (a : Carrier) → deriving i a  →  iCommutator i zero a
-  icom : (j : ℕ) → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (a ∙ b)
+  iunit : {a : Carrier} → deriving i a  →  iCommutator i zero a
+  icoml : {j : ℕ} → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (a ∙ b)
+  icomr : {j : ℕ} → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (b ∙ a)
+  iccong : {j : ℕ} → {a b : Carrier} → a ≈ b → iCommutator i j b → iCommutator i j a
 
 record IC (i : ℕ ) (ica : Carrier) : Set (Level.suc n ⊔ m) where
   field 
@@ -150,10 +152,27 @@
 CommGroup : (i : ℕ) → NormalSubGroup G 
 CommGroup i = record {
      P = IC i
-   ; Pε = record { icn = 0; icc = iunit ε ? }
-   ; P⁻¹ =  λ a pa → ?
-   ; P≈ = ?
-   ; P∙ = ?
-   ; Pcomm = ?
- } 
+   ; Pε = record { icn = 0; icc = iunit deriving-ε }
+   ; P⁻¹ =  cg00
+   ; P≈ = λ b=a ic → record { icn = icn ic ; icc = iccong (sym b=a) (icc ic) }
+   ; P∙ = cg01
+   ; Pcomm = cg02
+ }  where
+     open IC
+     cg00 :  (a : Carrier) → IC i a → IC i (a ⁻¹)
+     cg00 a record { icn = .zero ; icc = iunit  x } = record { icn = 0 ; icc = iunit (deriving-inv x) }
+     cg00 .((G Group.∙ _) _) record { icn = suc j ; icc = icoml ia icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } 
+     ... | ib = record { icn = suc (icn ib) ; icc = iccong (sym (lemma5 _ _ )) ( icomr (deriving-inv ia) (icc ib)) }
+     cg00 .((G Group.∙ _) _) record { icn = suc j ; icc = icomr ia icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } 
+     ... | ib = record { icn = suc (icn ib) ; icc = iccong (sym (lemma5 _ _ )) ( icoml (deriving-inv ia) (icc ib)) }
+     cg00 _ record { icn = j ; icc = iccong eq icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } 
+     ... | ib = record { icn = icn ib ; icc = iccong (⁻¹-cong eq) (icc ib) }
+     cg01 : {a b : Carrier} → IC i a → IC i b → IC i (a ∙ b)
+     cg01 {a} {b} record { icn = .zero ; icc = (iunit x) } ib = ?
+     cg01 {.((G Group.∙ _) _)} {b} record { icn = .(suc _) ; icc = (icoml x icc₁) } ib = ?
+     cg01 {.((G Group.∙ _) _)} {b} record { icn = .(suc _) ; icc = (icomr x icc₁) } ib = ?
+     cg01 {a} {b} record { icn = icn ; icc = (iccong x icc₁) } ib = ?
+     cg02 :  {a b : Carrier} → IC i a → IC i (b ∙ (a ∙ b ⁻¹))
+     cg02 = ?
 
+