Mercurial > hg > Members > kono > Proof > galois
changeset 296:7c1e3e0be315
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 03 Sep 2023 18:29:54 +0900 |
| parents | cc81d3b1a82a |
| children | c9fbb0096224 |
| files | src/Gutil0.agda src/Solvable.agda src/homomorphism.agda |
| diffstat | 3 files changed, 66 insertions(+), 232 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Gutil0.agda Sat Sep 02 16:44:24 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level hiding ( suc ; zero ) -module Gutil0 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 _<_∙_> - --- assuming Homomorphism is too strong --- -record NormalSubGroup {c d : Level} (A : Group c d ) : Set (Level.suc (Level.suc (c Level.⊔ d))) where - open Group A - field - P : Carrier → Set (Level.suc c ⊔ d) - 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 ) - -- gN ≈ Ng - Pcomm : {a b : Carrier } → P a → P ( b ∙ ( a ∙ b ⁻¹ ) ) - -import Relation.Binary.Reasoning.Setoid as EqReasoning - -record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup A) : Set (Level.suc c ⊔ d) where - open Group A - open NormalSubGroup n - field - elm : Carrier - Pelm : P elm - -NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group (Level.suc c ⊔ d) d -NGroup {_} {_} {A} n = record { - Carrier = Nelm 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 NormalSubGroup n - open Nelm - ga = Group.isGroup A - -
--- a/src/Solvable.agda Sat Sep 02 16:44:24 2023 +0900 +++ b/src/Solvable.agda Sun Sep 03 18:29:54 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import Level hiding ( suc ; zero ) open import Algebra module Solvable {n m : Level} (G : Group n m ) where @@ -103,7 +104,7 @@ comm-resp : {g h g1 h1 : Carrier } → g ≈ g1 → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] comm-resp {g} {h} {g1} {h1} g=g1 h=h1 = ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1 -open import Gutil0 +open import NormalSubgroup import Algebra.Morphism.Definitions as MorphismDefinitions open import Algebra.Morphism.Structures
--- a/src/homomorphism.agda Sat Sep 02 16:44:24 2023 +0900 +++ b/src/homomorphism.agda Sun Sep 03 18:29:54 2023 +0900 @@ -12,7 +12,7 @@ open import Data.Product open import Relation.Binary.PropositionalEquality -open import Gutil0 +open import NormalSubgroup import Gutil import Function.Definitions as FunctionDefinitions @@ -38,18 +38,6 @@ import Relation.Binary.Reasoning.Setoid as EqReasoning --- _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m --- m < x ∙ y > = Group._∙_ m x y - --- _<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c --- m < x ≈ y > = Group._≈_ m x y - --- infixr 9 _<_∙_> - --- --- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n } --- - open GroupMorphisms -- import Axiom.Extensionality.Propositional @@ -60,167 +48,114 @@ -- Set of a ∙ ∃ n ∈ N -- -record an {A : Group c c } (N : NormalSubGroup A ? ) (n x : Group.Carrier A ) : Set c where + +data IsaN {A : Group c d } (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where + an : (n : Group.Carrier A ) → (pn : NormalSubGroup.P N n) → IsaN N a (A < a ∙ n > ) + +record aNeq {A : Group c d } (N : NormalSubGroup A ) (a b : Group.Carrier A) : Set (Level.suc c ⊔ d) where + field + eq→ : {x : Group.Carrier A} → IsaN N a x → IsaN N b x + eq← : {x : Group.Carrier A} → IsaN N b x → IsaN N a x + +module AN (A : Group c d) (N : NormalSubGroup A ) where open Group A open NormalSubGroup N - field - a : Carrier - aN=x : a ∙ ⟦ n ⟧ ≈ x - -record aN {A : Group c c } (N : NormalSubGroup A ? ) : Set c where - open Group A - field - n : Carrier - is-an : (x : Carrier) → an N n x + open EqReasoning (Algebra.Group.setoid A) + open Gutil A -f0 : {A : Group c c } (N : NormalSubGroup A ? ) (x y : Group.Carrier A) → an N x y -f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = gk02 } where - open Group A - open NormalSubGroup N - open IsGroupHomomorphism normal - open EqReasoning (Algebra.Group.setoid A) - open Gutil A - gk02 : {x g : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x - gk02 {x} {g} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ - x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ - -_/_ : (A : Group c c ) (N : NormalSubGroup A ? ) → Group c c +_/_ : (A : Group c d ) (N : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) _/_ A N = record { - Carrier = aN N - ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧ - ; _∙_ = qadd - ; ε = qid - ; _⁻¹ = λ f → record { n = n f ⁻¹ ; is-an = λ x → record { a = an.a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧ ; aN=x = qinv0 f x } } + Carrier = Group.Carrier A + ; _≈_ = aNeq N + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = λ x → x ⁻¹ ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym } - ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gtrans (homo _ _) ( gtrans (∙-cong x=y u=v) (gsym (homo _ _) )) } - ; assoc = qassoc } - ; identity = (λ q → ⟦⟧-cong (proj₁ identity _) ) , (λ q → ⟦⟧-cong (proj₂ identity _) ) } - ; inverse = (λ x → ⟦⟧-cong (proj₁ inverse _ )) , (λ x → ⟦⟧-cong (proj₂ inverse _ ) ) - ; ⁻¹-cong = λ {x} {y} → i-conv {x} {y} + isEquivalence = record {refl = nrefl + ; trans = ? ; sym = λ a=b → ? + } + ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? } + ; assoc = ? } + ; identity = ? } + ; inverse = (λ x → ? ) , (λ x → ? ) + ; ⁻¹-cong = ? } } where + _=n=_ = aNeq N open Group A - open aN - open an open NormalSubGroup N - open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid A) open Gutil A - qadd : (f g : aN N) → aN N - qadd f g = record { n = n f ∙ n g ; is-an = λ x → record { a = x ⁻¹ ∙ ( a (is-an f x) ∙ a (is-an g x)) ; aN=x = qadd0 } } where - qadd0 : {x : Carrier} → x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x - qadd0 {x} = begin - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧ ∙ ⟦ n g ⟧ )) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ ( a (is-an g x) ∙ ⟦ n f ⟧) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) ) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩ - x ⁻¹ ∙ (x ∙ x) ≈⟨ solve monoid ⟩ - (x ⁻¹ ∙ x ) ∙ x ≈⟨ ? ⟩ - ε ∙ x ≈⟨ solve monoid ⟩ - x ∎ - qinv0 : (f : aN N) → (x : Carrier ) → (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈ x - qinv0 f x = begin - (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈⟨ ? ⟩ - a (is-an f x) ∙ ⟦ n f ⟧ ≈⟨ an.aN=x (is-an f x) ⟩ - x ∎ - qid : aN N - qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where - qid1 : {x : Carrier } → x ∙ ⟦ ε ⟧ ≈ x - qid1 {x} = begin - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ - qassoc : (f g h : aN N) → ⟦ n ( qadd (qadd f g) h) ⟧ ≈ ⟦ n( qadd f (qadd g h)) ⟧ - qassoc f g h = ⟦⟧-cong (assoc _ _ _ ) - i-conv : {x y : aN N} → ⟦ n x ⟧ ≈ ⟦ n y ⟧ → ⟦ n x ⁻¹ ⟧ ≈ ⟦ n y ⁻¹ ⟧ - i-conv {x} {y} nx=ny = begin - ⟦ n x ⁻¹ ⟧ ≈⟨ ⁻¹-homo _ ⟩ - ⟦ n x ⟧ ⁻¹ ≈⟨ ⁻¹-cong nx=ny ⟩ - ⟦ n y ⟧ ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ - ⟦ n y ⁻¹ ⟧ ∎ + open AN A N + nrefl : {x : Carrier} → x =n= x + nrefl = ? -- K ⊂ ker(f) -K⊆ker : (G H : Group c c) (K : NormalSubGroup G ?) (f : Group.Carrier G → Group.Carrier H ) → Set c -K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where +K⊆ker : (G H : Group c d) (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) + → Set (Level.suc c ⊔ d) +K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where open Group H open NormalSubGroup K open import Function.Surjection open import Function.Equality -module GK (G : Group c c) (K : NormalSubGroup G ? ) where +module GK (G : Group c d) (K : NormalSubGroup G ) where open Group G - open aN - open an open NormalSubGroup K - open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid G) open Gutil G + gkε : ? + gkε = ? -- record { a = ε ; n = ε ; pn = Pε } + φ : Group.Carrier G → Group.Carrier (G / K ) - φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹) ; aN=x = gk02 } } where - gk02 : {x : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x - gk02 {x} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ - x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ + φ g = ? φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ - φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = - record { cong = ? } }}} + φ-homo = record {⁻¹-homo = ? ; isMonoidHomomorphism = record { ε-homo = ? + ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = + record { cong = ? } }}} where - -- gk03 : {f : Group.Carrier (G / K) } → ⟦ n f ⟧ ≈ ⟦ ⟦ n f ⟧ ⟧ -- a (is-an f x) ∙ ⟦ n f ⟧ ≡ x - -- gk03 {x} = ? -- φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) - φe = record { _⟨$⟩_ = φ ; cong = ? } where - φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧ - φ-cong = ? - - inv-φ : Group.Carrier (G / K ) → Group.Carrier G - inv-φ f = n f -- ⟦ n f ⟧ ( if we have gk03 ) + φe = record { _⟨$⟩_ = φ ; cong = gk40 } where + gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j > + gk40 {i} {j} i=j = ? - cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g - cong-i {f} {g} nf=ng = ? - - is-inverse : (f : aN K ) → ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧ - is-inverse f = begin - ⟦ n (φ (inv-φ f) ) ⟧ ≈⟨ grefl ⟩ - ⟦ n (φ ( n f ) ) ⟧ ≈⟨ grefl ⟩ - ⟦ n f ⟧ ∎ + inv-φ : Group.Carrier (G / K ) → Carrier + inv-φ = ? -- record { a = a ; n = n ; pn = pn } = a ∙ n φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → ? } + ; right-inverse-of = ? } where + gk50 : (f g : Group.Carrier (G / K)) → ? ≈ ? → inv-φ f ≈ inv-φ g + gk50 = ? + gk60 : (x : Group.Carrier (G / K )) → inv-φ x ∙ ε ≈ ? + gk60 = ? gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x > - gk01 x = begin - ⟦ inv-φ x ⟧ ≈⟨ grefl ⟩ - ⟦ n x ⟧ ∎ + gk01 = ? -record FundamentalHomomorphism (G H : Group c c ) +record FundamentalHomomorphism (G H : Group c d ) (f : Group.Carrier G → Group.Carrier H ) (homo : IsGroupHomomorphism (GR G) (GR H) f ) - (K : NormalSubGroup G ? ) (kf : K⊆ker G H K f) : Set c where + (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set (Level.suc c ⊔ d) where open Group H -- open GK G K field h : Group.Carrier (G / K ) → Group.Carrier H h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h - is-solution : (x : Group.Carrier G) → f x ≈ h ? -- ( GK.φ ? x ) + is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ G K x ) unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) - → ( (x : Group.Carrier G) → f x ≈ h1 ? ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + → ( (x : Group.Carrier G) → f x ≈ h1 ( GK.φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) -FundamentalHomomorphismTheorm : (G H : Group c c) +FundamentalHomomorphismTheorm : (G H : Group c d) (f : Group.Carrier G → Group.Carrier H ) (homo : IsGroupHomomorphism (GR G) (GR H) f ) - (K : NormalSubGroup G ? ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf + (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf FundamentalHomomorphismTheorm G H f homo K kf = record { h = h ; h-homo = h-homo @@ -232,11 +167,11 @@ open Gutil H -- open NormalSubGroup K ? open IsGroupHomomorphism homo - open aN + open EqReasoning (Algebra.Group.setoid H) h : Group.Carrier (G / K ) → Group.Carrier H - h r = f ( GK.inv-φ ? ? ? ) + h r = f ( GK.inv-φ G K r ) h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y - h03 x y = {!!} + h03 = ? h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h h-homo = record { isMonoidHomomorphism = record { @@ -245,10 +180,9 @@ ; homo = h03 } ; ε-homo = {!!} } ; ⁻¹-homo = {!!} } - open EqReasoning (Algebra.Group.setoid H) is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ ? ? x ) is-solution x = begin - f x ≈⟨ grefl ⟩ + f x ≈⟨ ? ⟩ h ( GK.φ ? ? 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 ( GK.φ ? ? x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )