Mercurial > hg > Members > kono > Proof > galois

changeset 289:7bbc5e5b208d

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 Jan 2023 20:31:03 +0900
parents d08663bae245
children c870095531ef
files src/FundamentalHomorphism.agda
diffstat 1 files changed, 5 insertions(+), 49 deletions(-) [+]
line wrap: on
line diff
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 19:58:30 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 20:31:03 2023 +0900
@@ -64,9 +64,6 @@
        ⟦_⟧ : Group.Carrier A → Group.Carrier A
        normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
        comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b
-       -- because of ¬ ¬ Factor
-       factor : (a b : Carrier) → Carrier
-       is-factor : (a b : Carrier) →  b ∙ ⟦ factor a b ⟧ ≈ a
 
 -- Set of a ∙ ∃ n ∈ N
 --
@@ -89,28 +86,6 @@
    open NormalSubGroup N
    open IsGroupHomomorphism normal
 
-record Factor (A : Group c c ) (N : NormalSubGroup A) (a b : Group.Carrier A)  : Set c  where
-   open Group A
-   open NormalSubGroup N
-   open IsGroupHomomorphism normal
-   field
-       factor :  Carrier
-       is-factor :  b ∙ ⟦ factor ⟧ ≈ a
-
-¬¬Factor : (A : Group c c ) (N : NormalSubGroup A) → ¬ ( ( x y : Group.Carrier A) →  ¬ Factor A N  x y )
-¬¬Factor A N  neg = ⊥-elim ( fa (f0 N) )  where
-   open Group A
-   open NormalSubGroup N
-   open IsGroupHomomorphism normal
-   open EqReasoning (Algebra.Group.setoid A)
-   open Gutil A
-   open aN
-   open an
-
-   fa : ¬ ( (x y : Group.Carrier A) → an N x y )
-   fa f = neg ε (a (f ε ε)) record { factor = ε ; is-factor = aN=x (f ε ε)  }
-   -- λ x y → record { factor = ? ; is-factor = ? } )
-             
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
@@ -177,7 +152,7 @@
     open Gutil G
 
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g = record { n = factor ε g ; is-an = λ x → record { a = x ∙ ( ⟦ factor ε g ⟧ ⁻¹)   ; aN=x = ?  } }
+    φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹)   ; aN=x = ?  } }
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
     φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
@@ -195,7 +170,7 @@
     --           f x → φ (inv-φ f) (h1 x)
 
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f = ⟦ n f ⟧ ⁻¹
+    inv-φ f =  n f  
 
 
     cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
@@ -204,33 +179,15 @@
     is-inverse : (f : aN K  ) →  ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
     is-inverse f = begin
        ⟦ n (φ (inv-φ f) ) ⟧  ≈⟨ grefl  ⟩
-       ⟦ n (φ (⟦ n f  ⟧ ⁻¹) ) ⟧  ≈⟨ grefl  ⟩
-       ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
-       ε ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
-       ( ⟦ n f ⟧ ∙ ⟦ n f  ⟧ ⁻¹) ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
-       ⟦ n f ⟧ ∙ ( ⟦ n f  ⟧ ⁻¹ ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
-       ⟦ n f ⟧ ∙ ε  ≈⟨ ? ⟩
+       ⟦ n (φ ( n f  ) ) ⟧  ≈⟨ grefl  ⟩
        ⟦ n f ⟧ ∎
 
     φ-surjective : Surjective φe
     φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse }
 
-    gk00 : {x : Carrier } → ⟦ factor ε x ⟧ ⁻¹ ≈ x
-    gk00 {x} = begin
-        ⟦ factor ε x ⟧ ⁻¹ ≈⟨ ? ⟩ 
-        (ε ∙ ⟦ factor ε x ⟧)  ⁻¹ ≈⟨ ? ⟩ 
-        ( ( x ⁻¹ ∙   x ) ∙ ⟦ factor ε x ⟧ ) ⁻¹ ≈⟨ ? ⟩ 
-        ( x ⁻¹ ∙ ( x   ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x))  ⟩ 
-        ( x ⁻¹ ∙ ε ) ⁻¹ ≈⟨ ? ⟩ 
-        ( x ⁻¹  ) ⁻¹ ≈⟨ ? ⟩ 
-        x ∎
-
     gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >
     gk01 x = begin
-        ⟦ factor ε ( inv-φ x) ⟧  ≈⟨ ? ⟩ 
-        ( inv-φ x ) ⁻¹ ∙ ( inv-φ x ∙ ⟦ factor ε ( inv-φ x) ⟧)  ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩ 
-        ( inv-φ x ) ⁻¹ ∙ ε  ≈⟨ ? ⟩ 
-        ( ⟦ n x ⟧  ⁻¹) ⁻¹   ≈⟨ ? ⟩ 
+        ⟦ inv-φ x ⟧  ≈⟨ grefl ⟩ 
         ⟦ n x ⟧ ∎
 
 
@@ -278,8 +235,7 @@
     open EqReasoning (Algebra.Group.setoid H)
     is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
     is-solution x = begin
-         f x ≈⟨ gsym ( ⟦⟧-cong (gk00 ))  ⟩
-         f ( Group._⁻¹ G  ⟦ factor (Group.ε G) x  ⟧   ) ≈⟨ grefl  ⟩
+         f x ≈⟨ grefl  ⟩
          h ( φ x ) ∎ 
     unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
        → ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )