Mercurial > hg > Members > kono > Proof > galois

changeset 309:4dd130b93b21

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 Thu, 14 Sep 2023 13:03:17 +0900
parents 76c80a6ad4e6
children b4a3ed9301cb
files src/Homomorphism.agda src/NormalSubGroup.agda src/NormalSubgroup.agda src/Solvable.agda
diffstat 4 files changed, 154 insertions(+), 157 deletions(-) [+]
line wrap: on
line diff
--- a/src/Homomorphism.agda	Mon Sep 11 16:08:09 2023 +0900
+++ b/src/Homomorphism.agda	Thu Sep 14 13:03:17 2023 +0900
@@ -32,7 +32,7 @@
 --
 --       f
 --    G --→ H
---    |   /
+--    |   ↗ 
 --  φ |  / h
 --    ↓ /
 --    G/K
@@ -61,8 +61,7 @@
     open NormalSubGroup N
     open EqReasoning (Algebra.Group.setoid A)
     open Gutil A
-    open aNeq
-    --
+    open aNeq --
     -- (aN)(bN) = a(Nb)N = a(bN)N = (ab)NN = (ab)N.
     --
     -- a =n= b ↔ a . b ⁻¹ ∈ N
@@ -108,7 +107,7 @@
            b ∙ n ≈⟨ car (gsym eq) ⟩
            a ∙ n ≈⟨ eq1 ⟩
            x ∎
-    aneq : {a b : Carrier } → a ≈ b → aNeq N a b
+    aneq : {a b : Carrier } → a ≈ b → aNeq N a b  -- a ≈ b → aN ≈ bN
     aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt }   
     _=n=_ = aNeq N
 
@@ -120,6 +119,9 @@
     ntrans {x} {y} {z} x=y y=z = record { eq→ = λ {lt} ix → eq→ y=z (eq→ x=y ix) 
          ; eq← =  λ {lt} ix → eq← x=y (eq← y=z ix) }
 
+-- factor group has the same carrier as the original group
+--     so h = f 
+
 _/_ : {c d : Level} (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
     Carrier  = Group.Carrier A
@@ -132,8 +134,7 @@
            ; trans = ntrans ; sym = λ a=b → nsym a=b 
           }
        ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v }
-       ; assoc = gkassoc }
-       ; identity =  (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) )  }
+       ; assoc = gkassoc } ; identity =  (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) )  }
        ; inverse   =  (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) 
        ; ⁻¹-cong   = gkcong⁻¹
       }
--- a/src/NormalSubGroup.agda	Mon Sep 11 16:08:09 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-open import Level hiding ( suc ; zero )
-module NormalSubgroup  where
-
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Definitions
-open import Data.Product
-open import Relation.Binary.PropositionalEquality 
-open import Algebra.Morphism.Structures
-open import Data.Empty
-open import Relation.Nullary
-
-open GroupMorphisms
-
-GR : {c l : Level } → Group c l → RawGroup c l
-GR G = record {
-     Carrier        = Carrier G
-     ; _≈_          = _≈_ G
-     ; _∙_          = _∙_ G
-     ; ε            = ε G
-     ; _⁻¹          = _⁻¹ G
-  } where open Group
-
-record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
-     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
-     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
-     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
-     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
-
-GA : {c l : Level } → (G : Group c l) → GAxiom G
-GA G = record {
-        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
-     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
-     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
-     ;  inverse   = IsGroup.inverse isGroup
-     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
-   } where open Group G
-
-open import Relation.Binary.Structures
-
-Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
-Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
-             (IsGroup.isMonoid (Group.isGroup G ))) )
-
-_<_∙_> : {c d : Level} (m : Group c d )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
-m < x ∙ y > =  Group._∙_ m x y
-
-_<_≈_> : {c d : Level} (m : Group c d )  →    (f  g : Group.Carrier m ) → Set d
-m < x ≈ y > =  Group._≈_ m x y
-
-infixr 9 _<_∙_>
-
-record SubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
-   open Group A
-   field                           
-       P : Carrier  → Set l
-       Pε : P ε
-       P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
-       P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
-       P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
-
--- assuming Homomorphism is too strong
---
-record NormalSubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
-   open Group A
-   field                           
-       Psub : SubGroup {l} A
-       -- gN ≈ Ng
-       Pcomm : {a b : Carrier  }  → SubGroup.P Psub a  →  SubGroup.P Psub ( b ∙  ( a  ∙ b ⁻¹ ) )
-   P : Carrier  → Set l
-   P = SubGroup.P Psub
-   Pε : P ε
-   Pε = SubGroup.Pε Psub
-   P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
-   P⁻¹ = SubGroup.P⁻¹ Psub
-   P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
-   P≈ = SubGroup.P≈ Psub
-   P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
-   P∙ = SubGroup.P∙ Psub
-
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-
-record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set  (Level.suc e ⊔ (Level.suc c ⊔ d))  where
-   open Group A
-   open SubGroup n 
-   field                           
-       elm : Carrier
-       Pelm : P elm
-
-SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group  (Level.suc e ⊔ (Level.suc c ⊔ d))  d
-SGroup {_} {_} {_} A n = record {
-      Carrier        = Nelm A n
-    ; _≈_            = λ x y → elm x ≈ elm y
-    ; _∙_            = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
-    ; ε              = record { elm = ε ; Pelm = Pε }
-    ; _⁻¹            = λ x → record { elm = (elm x) ⁻¹  ; Pelm = P⁻¹ (elm x) (Pelm x) }
-    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) 
-          ; sym =  IsEquivalence.sym (IsGroup.isEquivalence ga) 
-          ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga)  }
-       ; ∙-cong = IsGroup.∙-cong ga }
-       ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
-       ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
-       ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) 
-       ; ⁻¹-cong   = IsGroup.⁻¹-cong ga }
-   }  where
-       open Group A
-       open SubGroup n 
-       open Nelm 
-       ga = Group.isGroup A
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/NormalSubgroup.agda	Thu Sep 14 13:03:17 2023 +0900
@@ -0,0 +1,116 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Level hiding ( suc ; zero )
+module NormalSubgroup  where
+
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+open import Relation.Binary.PropositionalEquality 
+open import Algebra.Morphism.Structures
+open import Data.Empty
+open import Relation.Nullary
+
+open GroupMorphisms
+
+GR : {c l : Level } → Group c l → RawGroup c l
+GR G = record {
+     Carrier        = Carrier G
+     ; _≈_          = _≈_ G
+     ; _∙_          = _∙_ G
+     ; ε            = ε G
+     ; _⁻¹          = _⁻¹ G
+  } where open Group
+
+record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
+     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
+     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
+     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
+     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
+
+GA : {c l : Level } → (G : Group c l) → GAxiom G
+GA G = record {
+        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
+     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
+     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
+     ;  inverse   = IsGroup.inverse isGroup
+     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
+   } where open Group G
+
+open import Relation.Binary.Structures
+
+Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
+Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid (Group.isGroup G ))) )
+
+_<_∙_> : {c d : Level} (m : Group c d )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
+m < x ∙ y > =  Group._∙_ m x y
+
+_<_≈_> : {c d : Level} (m : Group c d )  →    (f  g : Group.Carrier m ) → Set d
+m < x ≈ y > =  Group._≈_ m x y
+
+infixr 9 _<_∙_>
+
+record SubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
+   open Group A
+   field                           
+       P : Carrier  → Set l
+       Pε : P ε
+       P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
+       P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
+       P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
+
+-- assuming Homomorphism is too strong
+--
+record NormalSubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
+   open Group A
+   field                           
+       Psub : SubGroup {l} A
+       -- gN ≈ Ng
+       Pcomm : {a b : Carrier  }  → SubGroup.P Psub a  →  SubGroup.P Psub ( b ∙  ( a  ∙ b ⁻¹ ) )
+   P : Carrier  → Set l
+   P = SubGroup.P Psub
+   Pε : P ε
+   Pε = SubGroup.Pε Psub
+   P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
+   P⁻¹ = SubGroup.P⁻¹ Psub
+   P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
+   P≈ = SubGroup.P≈ Psub
+   P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
+   P∙ = SubGroup.P∙ Psub
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set  (Level.suc e ⊔ (Level.suc c ⊔ d))  where
+   open Group A
+   open SubGroup n 
+   field                           
+       elm : Carrier
+       Pelm : P elm
+
+SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group  (Level.suc e ⊔ (Level.suc c ⊔ d))  d
+SGroup {_} {_} {_} A n = record {
+      Carrier        = Nelm A n
+    ; _≈_            = λ x y → elm x ≈ elm y
+    ; _∙_            = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
+    ; ε              = record { elm = ε ; Pelm = Pε }
+    ; _⁻¹            = λ x → record { elm = (elm x) ⁻¹  ; Pelm = P⁻¹ (elm x) (Pelm x) }
+    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) 
+          ; sym =  IsEquivalence.sym (IsGroup.isEquivalence ga) 
+          ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga)  }
+       ; ∙-cong = IsGroup.∙-cong ga }
+       ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
+       ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
+       ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) 
+       ; ⁻¹-cong   = IsGroup.⁻¹-cong ga }
+   }  where
+       open Group A
+       open SubGroup n 
+       open Nelm 
+       ga = Group.isGroup A
+
+
--- a/src/Solvable.agda	Mon Sep 11 16:08:09 2023 +0900
+++ b/src/Solvable.agda	Thu Sep 14 13:03:17 2023 +0900
@@ -108,8 +108,6 @@
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Algebra.Morphism.Structures
 
--- Commutator is normal subgroup of G
-
 Pcomm : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i (b ∙ (a ∙ b ⁻¹ ))
 Pcomm {a} {b} zero (lift tt) = lift tt
 Pcomm {.([ _ , _ ])} {b} (suc i) (comm {g} {h} pg ph ) = ccong cc2 (comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph)) where
@@ -136,44 +134,42 @@
     b ∙ ([ g , h ] ∙ b ⁻¹) ∎
 Pcomm {a} {b} (suc i) (ccong f=a pa) = ccong (∙-cong grefl (∙-cong f=a grefl)) (Pcomm {_} {b} (suc i) pa)
 
+-- Finitely Generated Commutator is normal subgroup of G
+
 -- a proudct of commutators may not be a commutator
 -- 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
-  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
+data iCommutator (i : ℕ) : Carrier → Set (Level.suc n ⊔ m) where
+  iunit : {a : Carrier} → deriving i a  →  iCommutator i a
+  i∙ : {a b : Carrier} → iCommutator i a → iCommutator i  b → iCommutator i  (a ∙ b)
+  iccong : {a b : Carrier} → a ≈ b → iCommutator i  b → iCommutator i  a
 
-record IC (i : ℕ ) (ica : Carrier) : Set (Level.suc n ⊔ m) where
-  field 
-     icn : ℕ
-     icc : iCommutator i icn ica
-
-CommGroup : (i : ℕ) → NormalSubGroup G 
-CommGroup i = record {
-     P = IC i
-   ; Pε = record { icn = 0; icc = iunit deriving-ε }
+CommNormal : (i : ℕ) → NormalSubGroup G 
+CommNormal i = record {
+   Psub = record {
+     P = iCommutator i
+   ; Pε = iunit deriving-ε 
    ; P⁻¹ =  cg00
-   ; P≈ = λ b=a ic → record { icn = icn ic ; icc = iccong (sym b=a) (icc ic) }
-   ; P∙ = cg01
-   ; Pcomm = cg02
+   ; P≈ = λ b=a ic → iccong (sym b=a) 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 = ?
+     cg00 :  (a : Carrier) → iCommutator i a → iCommutator i (a ⁻¹)
+     cg00 a (iunit x) = iunit (deriving-inv x)
+     cg00 .((G Group.∙ _) _) (i∙ ic ic₁) = iccong (gsym (lemma5 _ _)) ( i∙ (cg00 _ ic₁) (cg00 _ ic) )
+     cg00 a (iccong eq ic) = iccong (⁻¹-cong eq) (cg00 _ ic)
+     cg01 : {a b : Carrier} → iCommutator i a → iCommutator i b → iCommutator i (a ∙ b)
+     cg01 {a} {b} ia ib = i∙  ia ib
+     cg02 : {a b : Carrier} → iCommutator i a → iCommutator i (b ∙ (a ∙ b ⁻¹))
+     cg02 {a} {b} (iunit da) = iunit ( Pcomm i da )
+     cg02 {a} {b} (i∙ {a₁} {b₁} ia ib)  = iccong cg03 (i∙ (cg02 {a₁} {b} ia) (cg02 {b₁} {b} ib)) where
+        cg03 : b ∙ (a₁ ∙ b₁ ∙ b ⁻¹) ≈  b ∙ (a₁ ∙ b ⁻¹) ∙ (b ∙ (b₁ ∙ b ⁻¹))
+        cg03 = begin
+           b ∙ (a₁ ∙ b₁ ∙ b ⁻¹) ≈⟨ solve monoid ⟩
+           b ∙ (a₁ ∙ ε ∙ b₁ ∙ b ⁻¹) ≈⟨ cdr (car (car (cdr (gsym (proj₁ inverse _))))) ⟩
+           b ∙ (a₁ ∙ (b ⁻¹ ∙ b ) ∙ b₁ ∙ b ⁻¹) ≈⟨ solve monoid ⟩
+            b ∙ (a₁ ∙ b ⁻¹) ∙ (b ∙ (b₁ ∙ b ⁻¹)) ∎ 
+     cg02 {a} {b} (iccong eq ia) = iccong (cdr (car eq)) ( cg02 {_} {b} ia )