Mercurial > hg > Members > kono > Proof > galois
diff src/Fundamental.agda @ 282:b70cc2534d2f
double record on quontient group
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 29 Jan 2023 10:47:09 +0900 |
parents | 803f909fdd17 |
children | b89af4300407 |
line wrap: on
line diff
--- a/src/Fundamental.agda Sun Jan 29 08:19:19 2023 +0900 +++ b/src/Fundamental.agda Sun Jan 29 10:47:09 2023 +0900 @@ -11,13 +11,13 @@ open import Algebra.Bundles open import Data.Product -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality open import Gutil0 import Gutil import Function.Definitions as FunctionDefinitions import Algebra.Morphism.Definitions as MorphismDefinitions -open import Algebra.Morphism.Structures +open import Algebra.Morphism.Structures open import Tactic.MonoidSolver using (solve; solve-macro) @@ -41,7 +41,7 @@ _<_∙_> : (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 : Group c c ) → (f g : Group.Carrier m ) → Set c m < x ≈ y > = Group._≈_ m x y infixr 9 _<_∙_> @@ -59,85 +59,69 @@ record NormalSubGroup (A : Group c c ) : Set c where open Group A - field - ⟦_⟧ : Group.Carrier A → Group.Carrier A + field + ⟦_⟧ : Group.Carrier A → Group.Carrier A normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧ - comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b - -- + comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b + -- factor : (a b : Carrier) → Carrier is-factor : (a b : Carrier) → b ∙ ⟦ factor a b ⟧ ≈ a -- Set of a ∙ ∃ n ∈ N -- -record aN {A : Group c c } (N : NormalSubGroup A ) (x : Group.Carrier A ) : Set c where +record an {A : Group c c } (N : NormalSubGroup A ) (n x : Group.Carrier A ) : Set c where open Group A open NormalSubGroup N - field - a n : Group.Carrier A + field + a : Group.Carrier A aN=x : a ∙ ⟦ n ⟧ ≈ x +record aN {A : Group c c } (N : NormalSubGroup A ) : Set c where + field + n : Group.Carrier A + is-an : (x : Group.Carrier A) → an N n x + +qid : {A : Group c c } (N : NormalSubGroup A ) → aN N +qid {A} N = record { n = ε ; is-an = λ x → record { a = x ; aN=x = ? } } where + open Group A + open NormalSubGroup N + _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c _/_ A N = record { - Carrier = (x : Group.Carrier A) → aN N x - ; _≈_ = _=n=_ - ; _∙_ = qadd - ; ε = qid - ; _⁻¹ = qinv + Carrier = aN N + ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧ + ; _∙_ = qadd + ; ε = qid N + ; _⁻¹ = ? ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = ? ; trans = ? ; sym = ? } - ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} } + isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym } + ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? } ; assoc = ? } - ; identity = idL , (λ q → ? ) } - ; inverse = ( (λ x → ? ) , (λ x → ? )) + ; identity = ? , (λ q → ? ) } + ; inverse = ( (λ x → ? ) , (λ x → ? )) ; ⁻¹-cong = λ i=j → ? } } where open Group A open aN + open an open NormalSubGroup N - open IsGroupHomomorphism normal + open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid A) open Gutil A - _=n=_ : (f g : (x : Group.Carrier A ) → aN N x ) → Set c - f =n= g = {x y : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ - qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x - qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where - q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x - q00 = begin - ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩ - x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl ) (∙-cong (grefl ) (∙-cong comm (grefl ) )) ⟩ - x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl ) (aN=x (g x) ) ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl ) (aN=x (f x))) (grefl ) ⟩ - (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl ) ⟩ - ε ∙ x ≈⟨ solve monoid ⟩ - x ∎ - qid : ( x : Carrier ) → aN N x - qid x = record { a = x ; n = ε ; aN=x = qid1 } where - qid1 : x ∙ ⟦ ε ⟧ ≈ x - qid1 = begin - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩ - x ∙ ε ≈⟨ solve monoid ⟩ - x ∎ - qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x - qinv f x = record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; aN=x = qinv1 } where - qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x - qinv1 = begin - x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ - x ∙ ⟦ (n (f x)) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ - x ∙ ⟦ ((n (f x)) ⁻¹ ) ∙ n (f x) ⟧ ≈⟨ ? ⟩ - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩ - x ∙ ε ≈⟨ solve monoid ⟩ - x ∎ - qcong : { x y u v : (x₁ : Carrier) → aN N x₁ } → (x=y : x =n= y) ( u=v : u =n= v ) → qadd x u =n= qadd y v - qcong {x} {y} {u} {v} x=y u=v {w} {z} = begin - ⟦ n (x w) ∙ n (u w) ⟧ ≈⟨ homo _ _ ⟩ - ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧ ≈⟨ ∙-cong x=y u=v ⟩ - ⟦ n (y z) ⟧ ∙ ⟦ n (v z) ⟧ ≈⟨ gsym (homo _ _ ) ⟩ - ⟦ n (y z) ∙ n (v z) ⟧ ∎ - idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f - idL f = ? + 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 ⟧ ≈⟨ ? ⟩ + 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 ⟧ )) ≈⟨ ? ⟩ + 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 ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩ + x ⁻¹ ∙ (x ∙ x) ≈⟨ ? ⟩ + x ∎ -- K ⊂ ker(f) K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c @@ -151,21 +135,22 @@ module _ (G : Group c c) (K : NormalSubGroup G) where open Group G open aN + open an open NormalSubGroup K - open IsGroupHomomorphism normal + open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid G) open Gutil G φ : Group.Carrier G → Group.Carrier (G / K ) - φ g x = record { a = g ; n = factor x g ; aN=x = is-factor x g } + φ g = record { n = factor ε g ; is-an = λ x → record { a = x ∙ ( ⟦ factor ε g ⟧ ⁻¹) ; aN=x = ? } } - φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ + φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = record { cong = ? } }}} φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) φe = record { _⟨$⟩_ = φ ; cong = ? } where - φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ + φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧ φ-cong = ? -- inverse ofφ @@ -175,158 +160,35 @@ -- f x → φ (inv-φ f) (h1 x) inv-φ : Group.Carrier (G / K ) → Group.Carrier G - inv-φ f = ⟦ n (f ε) ⟧ ⁻¹ - - an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹ - an02 f {x} = begin - a (f x ) ≈⟨ gsym ( proj₂ identity _) ⟩ - a (f x ) ∙ ε ≈⟨ ∙-cong (grefl ) (gsym (proj₂ inverse _)) ⟩ - a (f x ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹) ≈⟨ solve monoid ⟩ - (a (f x ) ∙ ⟦ n (f x) ⟧) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ∙-cong (aN=x (f x)) (grefl ) ⟩ - x ∙ ⟦ n (f x) ⟧ ⁻¹ ∎ + inv-φ f = ⟦ n f ⟧ ⁻¹ - aNeqε : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g > - → {x : Carrier } → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε - aNeqε {f} {g} f=g {x} = begin - ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩ - ε ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩ - (a (f x) ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ solve monoid ⟩ - a (f x) ⁻¹ ∙ (a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ≈⟨ ? ⟩ - a (f x) ⁻¹ ∙ a (g x) ≈⟨ ∙-cong (⁻¹-cong (an02 f) ) (an02 g) ⟩ - (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (g x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ - (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ - ( ⟦ n (f x) ⟧ ∙ x ⁻¹ ) ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ - ⟦ n (f x) ⟧ ∙ ( x ⁻¹ ∙ x ) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ? ⟩ - ⟦ n (f x) ⟧ ∙ ε ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ solve monoid ⟩ - ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ proj₂ inverse _ ⟩ - ε ∎ where - an01 : a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ a (g x) - an01 = is-factor (a (g x)) (a (f x)) - an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧ - an03 = ? - cong-i : {f g : Group.Carrier (G / K ) } → ({x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ ) → inv-φ f ≈ inv-φ g + cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g cong-i = ? - factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧ - factor=nf f {y} with f y - ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin - ⟦ factor y z ⟧ ≈⟨ ? ⟩ - z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ - z ⁻¹ ∙ y ≈⟨ ∙-cong (grefl ) (gsym faN=x ) ⟩ - z ⁻¹ ∙ ( fa ∙ ⟦ fn ⟧ ) ≈⟨ ? ⟩ - (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧ ≈⟨ ? ⟩ - ε ∙ ⟦ fn ⟧ ≈⟨ solve monoid ⟩ - ⟦ fn ⟧ ∎ where - z = fa ⁻¹ - - φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ - φ-factor f {x} {y} = begin - ⟦ n (f x) ⟧ ≈⟨ ? ⟩ - ⟦ n (f x) ⟧ ∙ ε ≈⟨ ? ⟩ - ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ⟦ n (f y) ⟧ ⁻¹ ) ≈⟨ cdr ( cdr an07 ) ⟩ - ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ( ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ )) ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∙ ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∙ ε ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∎ where - fxy = ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f y) ⟧ - - fa11 : a (f (x ∙ y ⁻¹ )) ∙ ⟦ n (f (x ∙ y ⁻¹)) ⟧ ≈ x ∙ y ⁻¹ - fa11 = aN=x ( f ( x ∙ y ⁻¹ )) - - fa21 : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε - fa21 = aN=x ( f ε) - - fa22 : {x : Carrier } → a (f (x ⁻¹)) ∙ ⟦ n (f (x ⁻¹)) ⟧ ≈ x ⁻¹ - fa22 {x} = aN=x ( f (x ⁻¹)) - - fa14 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x - fa14 = aN=x ( f x) - - fa13 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y - fa13 = aN=x ( f y) + 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 ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + ( ⟦ n f ⟧ ∙ ⟦ n f ⟧ ⁻¹) ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + ⟦ n f ⟧ ∙ ( ⟦ n f ⟧ ⁻¹ ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩ + ⟦ n f ⟧ ∙ ε ≈⟨ ? ⟩ + ⟦ n f ⟧ ∎ - fa12 : aN K ( x ∙ y ⁻¹ ) - fa12 = f (x ∙ y ⁻¹ ) - an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x) - an01 y = is-factor (a (f x)) y - an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x) - an04 = is-factor (a (f x)) (a (f y)) - an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧ - an07 {z} {w} = gsym ( is-factor z w ) - an10 : ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈ ε - an10 = begin - ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ - ( a (f x) ∙ x ⁻¹ ) ⁻¹ ∙ (a (f y) ∙ y ⁻¹) ≈⟨ ? ⟩ - x ∙ a (f x) ⁻¹ ∙ a (f y) ∙ y ⁻¹ ≈⟨ ? ⟩ - ε ∎ - an08 : ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈ ε - an08 = begin - ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ - ε ∎ - an05 : {z : Carrier} → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧ - an05 {z} = begin - ⟦ n (f z) ⟧ ≈⟨ ? ⟩ - ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧ ≈⟨ ? ⟩ - (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧) ≈⟨ ∙-cong grefl (aN=x (f z)) ⟩ - (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z)))) ⟩ - (a (f z) ⁻¹) ∙ (a (f z) ∙ ⟦ factor z (a (f z)) ⟧ ) ≈⟨ ? ⟩ - ⟦ factor z ( a ( f z)) ⟧ ∎ - an06 : {z : Carrier} → ⟦ factor z z ⟧ ≈ ε - an06 {z} = begin - ⟦ factor z z ⟧ ≈⟨ ? ⟩ - (z ⁻¹ ∙ z ) ∙ ⟦ factor z z ⟧ ≈⟨ ? ⟩ - z ⁻¹ ∙ ( z ∙ ⟦ factor z z ⟧ ) ≈⟨ ∙-cong grefl (is-factor z z) ⟩ - z ⁻¹ ∙ z ≈⟨ ? ⟩ - ε ∎ - an03 : ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈ ε - an03 = begin - ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈⟨ ? ⟩ - ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x (a (f x)) ⟧ ≈⟨ ? ⟩ - ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x ( x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⟧ ≈⟨ ? ⟩ - ⟦ n (f (y ⁻¹ ∙ x)) ⟧ ≈⟨ ? ⟩ - ⟦ factor (y ⁻¹ ∙ x) (a (f (y ⁻¹ ∙ x))) ⟧ ≈⟨ ? ⟩ - ⟦ n (f ⟦ ε ⟧ ) ⟧ ≈⟨ ? ⟩ - ⟦ ε ⟧ ≈⟨ ? ⟩ -- ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε - ε ∎ + φ-surjective : Surjective φe + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } - is-inverse : (f : (x : Carrier) → aN K x ) → {x y : Carrier} → ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f y) ⟧ - is-inverse f {x} {y} = begin - ⟦ n (φ (inv-φ f) x) ⟧ ≈⟨ grefl ⟩ - ⟦ n (φ (⟦ n (f ε) ⟧ ⁻¹) x) ⟧ ≈⟨ grefl ⟩ - ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ - ε ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ - (x ∙ x ⁻¹ ) ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ - x ∙ ( x ⁻¹ ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ) ≈⟨ ? ⟩ - x ∙ ⟦ n (f ε) ⟧ ⁻¹ ≈⟨ ? ⟩ - y ∙ ⟦ n (f y) ⟧ ⁻¹ ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∎ where - afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε - afn = aN=x (f ε) - afn' = (a (f y)) ⁻¹ - f00 : ⟦ n (f ε) ⟧ ≈ (a (f y)) ⁻¹ - f00 = begin - ⟦ n (f ε) ⟧ ≈⟨ ? ⟩ - (a (f ε)) ⁻¹ ∙ a (f ε) ∙ ⟦ n (f ε) ⟧ ≈⟨ ? ⟩ - (a (f ε)) ⁻¹ ∙ ε ≈⟨ ? ⟩ - ⟦ n (f y) ⟧ ∙ y ⁻¹ ≈⟨ ? ⟩ - (a (f y)) ⁻¹ ∙ ( a (f y) ∙ ⟦ n (f y) ⟧ ∙ y ⁻¹ ) ≈⟨ ? ⟩ - (a (f y)) ⁻¹ ∎ - - φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = ? } - record FundamentalHomomorphism (G H : Group c c ) - (f : Group.Carrier G → Group.Carrier H ) - (homo : IsGroupHomomorphism (GR G) (GR H) f ) + (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 open Group H 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 ( φ G K x ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) FundamentalHomomorphismTheorm : (G H : Group c c) @@ -341,14 +203,14 @@ } where open Group H h : Group.Carrier (G / K ) → Group.Carrier H - h r = f ( aN.n (r (Group.ε G ) )) + h r = f ( aN.n ? ) h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y h03 x y = {!!} h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h h-homo = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { - isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } + isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } ; homo = h03 } ; ε-homo = {!!} } ; ⁻¹-homo = {!!} } @@ -356,12 +218,14 @@ is-solution x = begin f x ≈⟨ ? ⟩ ? ≈⟨ ? ⟩ - f ( aN.n (( φ G K x ) (Group.ε G ) )) ≈⟨ ? ⟩ + f ( aN.n (( φ G K ) (Group.ε G ) )) ≈⟨ ? ⟩ h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) unique = ? + +