Mercurial > hg > Members > kono > Proof > galois

changeset 258:ea5087692f7e

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 Sun, 29 May 2022 12:36:07 +0900
parents d500309866da
children b53eedf6dfb1
files src/FundamentalHomomorphism.agda src/fundamental.agda
diffstat 2 files changed, 91 insertions(+), 82 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FundamentalHomomorphism.agda	Sun May 29 12:36:07 2022 +0900
@@ -0,0 +1,91 @@
+-- fundamental homomorphism theorem
+--
+
+open import Level hiding ( suc ; zero )
+module FundamentalHomomorphism (c l : Level) where
+
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+-- open import Function hiding (id ; flip)
+-- open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+-- open import Function.LeftInverse  using ( _LeftInverseOf_ )
+-- open import Function.Equality using (Π)
+open import Relation.Binary.PropositionalEquality 
+open import Algebra.Morphism.Structures
+open GroupMorphisms
+
+Group→Raw : {c l : Level } → Group c l → RawGroup c l
+Group→Raw G = record {
+     Carrier        = Carrier G
+     ; _≈_          = _≈_ G
+     ; _∙_          = _∙_ G
+     ; ε            = ε G
+     ; _⁻¹          = _⁻¹ G
+  } where open Group
+
+record NormalSubGroup ( G : Group c l ) : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     sub : Carrier → Carrier 
+     subgroup  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
+     normal : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
+
+data Coset (G : Group c l)  (K : NormalSubGroup G) :  Group.Carrier G → Set ( c  Level.⊔  l ) where
+    coset : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) )
+    cscong : {a b : Group.Carrier G } → Group._≈_ G a b → Coset G K a → Coset G K b
+
+record CosetCarrier (G : Group c l)  (K : NormalSubGroup G) :  Set ( c  Level.⊔  l ) where  
+  field
+    r :  Group.Carrier G
+    isCoset : Coset G K r
+
+φ :   {G : Group c l} →  {K : NormalSubGroup G} → Group.Carrier G → CosetCarrier G K
+φ {G} {K} x = record { r = NormalSubGroup.sub K x ; isCoset = p1 } where
+   p1 :  Coset G K (NormalSubGroup.sub K x)
+   p1 = cscong (proj₁ (Group.identity G) (NormalSubGroup.sub K x ) ) (coset (Group.ε G) x )
+
+-- G / K : Quotient
+_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
+G / K = record {
+     Carrier        = CosetCarrier G K
+     ; _≈_          = λ x y → r x ≈ r y
+     ; _∙_          = λ x y → record { r =  r x ∙ r y ; isCoset = ? }
+     ; ε            = record { r =  ε ; isCoset = {!!} }
+     ; _⁻¹          = λ x → record { r = (r x) ⁻¹  ; isCoset = {!!} }
+     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = {!!}
+       ; ∙-cong = {!!} }
+       ; assoc = {!!} }
+       ; identity = {!!} }
+       ; inverse   = {!!} 
+       ; ⁻¹-cong   = {!!}
+      } 
+   } where 
+      open Group G
+      open CosetCarrier 
+
+-- K ⊂ ker(f)
+K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
+K⊆ker G H K f = (k : CosetCarrier G K ) → f (CosetCarrier.r k ) ≈ ε   where
+  open Group H
+
+record FundamentalHomomorphism (G H : Group c l)  
+    (f : Group.Carrier G → Group.Carrier H ) 
+    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f ) 
+    (K : NormalSubGroup G ) :  Set ( c  Level.⊔  l ) where
+  open Group H
+  field
+    h : K⊆ker G H K f → CosetCarrier G K → Group.Carrier H
+    h-homo : (kf : K⊆ker G H K f ) → IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) (h kf)
+    uniqune : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ x )
+
+FundamentalHomomorphismTheorm : (G H : Group c l)
+    (f : Group.Carrier G → Group.Carrier H )
+    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f )
+    (K : NormalSubGroup G ) → FundamentalHomomorphism G H f homo K
+FundamentalHomomorphismTheorm G H f homo K = {!!}
+
+
+
--- a/src/fundamental.agda	Sun May 29 10:09:02 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
--- fundamental homomorphism theorem
---
-
-open import Level hiding ( suc ; zero )
-module fundamental (c l : Level) where
-
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Definitions
-open import Data.Product
--- open import Function hiding (id ; flip)
--- open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
--- open import Function.LeftInverse  using ( _LeftInverseOf_ )
--- open import Function.Equality using (Π)
-open import Relation.Binary.PropositionalEquality 
-open import Algebra.Morphism.Structures
-open GroupMorphisms
-
-Group→Raw : Group c l → RawGroup c l
-Group→Raw G = record {
-     Carrier        = Carrier G
-     ; _≈_          = _≈_ G
-     ; _∙_          = _∙_ G
-     ; ε            = ε G
-     ; _⁻¹          = _⁻¹ G
-  } where open Group
-
--- record Kernel {G H : Group } (f : Carrier G → Carrier H ) : Set ( c Level.⊔ l ) where
---   field
---      kernel :  Carrier H → Carrier G
---      isKernel : (x : Carrier H ) → kernel x ∙
-
-record NormalSubGroup ( G : Group c l ) : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     sub : Carrier → Carrier 
-     subgroup  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
-     normal : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
-
--- open RawGroup G₁ renaming
---     (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
--- open RawGroup G₂ renaming
---     (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
-
-data Coset (G : Group c l)  (NS : NormalSubGroup G) :  Group.Carrier G → Set c where
-    coset : (a b : Group.Carrier G ) → Coset G NS ( Group._∙_ G a (NormalSubGroup.sub NS b) )
-
-record CosetCarrier (G : Group c l)  (NS : NormalSubGroup G) :  Set ( c  Level.⊔  l ) where  
-  field
-    r :  Group.Carrier G
-    isCoset : Coset G NS r
-
-φ :   {G : Group c l} →  {NS : NormalSubGroup G} → Group.Carrier G → CosetCarrier G NS
-φ {G} {NS} x = record { r = NormalSubGroup.sub NS x ; isCoset = p1 } where
-   p1 :  Coset G NS (NormalSubGroup.sub NS x)
-   p1 = subst (λ k →  Coset G NS k ) {!!} (coset {!!} {!!} )
-
-Quotient : (G : Group c l)  (NS : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
-Quotient G NS = record {
-     Carrier        = CosetCarrier G NS
-     ; _≈_          = {!!}
-     ; _∙_          = {!!}
-     ; ε            = {!!}
-     ; _⁻¹          = {!!}
-     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = {!!}
-       ; ∙-cong = {!!} }
-       ; assoc = {!!} }
-       ; identity = {!!} }
-       ; inverse   = {!!} 
-       ; ⁻¹-cong   = {!!}
-      } 
-   } where 
-      open Group G
-
-record Fundamental (G H : Group c l)  
-    (f : Group.Carrier G → Group.Carrier H ) 
-    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f ) 
-    (N : NormalSubGroup G ) :  Set ( c  Level.⊔  l ) where
-  field
-    h : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f 
-