comparison 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
comparison
equal deleted inserted replaced
281:803f909fdd17 282:b70cc2534d2f
9 open import Algebra.Definitions 9 open import Algebra.Definitions
10 open import Algebra.Core 10 open import Algebra.Core
11 open import Algebra.Bundles 11 open import Algebra.Bundles
12 12
13 open import Data.Product 13 open import Data.Product
14 open import Relation.Binary.PropositionalEquality 14 open import Relation.Binary.PropositionalEquality
15 open import Gutil0 15 open import Gutil0
16 import Gutil 16 import Gutil
17 import Function.Definitions as FunctionDefinitions 17 import Function.Definitions as FunctionDefinitions
18 18
19 import Algebra.Morphism.Definitions as MorphismDefinitions 19 import Algebra.Morphism.Definitions as MorphismDefinitions
20 open import Algebra.Morphism.Structures 20 open import Algebra.Morphism.Structures
21 21
22 open import Tactic.MonoidSolver using (solve; solve-macro) 22 open import Tactic.MonoidSolver using (solve; solve-macro)
23 23
24 -- 24 --
25 -- Given two groups G and H and a group homomorphism f : G → H, 25 -- Given two groups G and H and a group homomorphism f : G → H,
39 import Relation.Binary.Reasoning.Setoid as EqReasoning 39 import Relation.Binary.Reasoning.Setoid as EqReasoning
40 40
41 _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m 41 _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m
42 m < x ∙ y > = Group._∙_ m x y 42 m < x ∙ y > = Group._∙_ m x y
43 43
44 _<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c 44 _<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c
45 m < x ≈ y > = Group._≈_ m x y 45 m < x ≈ y > = Group._≈_ m x y
46 46
47 infixr 9 _<_∙_> 47 infixr 9 _<_∙_>
48 48
49 -- 49 --
57 open import Tactic.MonoidSolver using (solve; solve-macro) 57 open import Tactic.MonoidSolver using (solve; solve-macro)
58 58
59 59
60 record NormalSubGroup (A : Group c c ) : Set c where 60 record NormalSubGroup (A : Group c c ) : Set c where
61 open Group A 61 open Group A
62 field 62 field
63 ⟦_⟧ : Group.Carrier A → Group.Carrier A 63 ⟦_⟧ : Group.Carrier A → Group.Carrier A
64 normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧ 64 normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧
65 comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b 65 comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b
66 -- 66 --
67 factor : (a b : Carrier) → Carrier 67 factor : (a b : Carrier) → Carrier
68 is-factor : (a b : Carrier) → b ∙ ⟦ factor a b ⟧ ≈ a 68 is-factor : (a b : Carrier) → b ∙ ⟦ factor a b ⟧ ≈ a
69 69
70 -- Set of a ∙ ∃ n ∈ N 70 -- Set of a ∙ ∃ n ∈ N
71 -- 71 --
72 record aN {A : Group c c } (N : NormalSubGroup A ) (x : Group.Carrier A ) : Set c where 72 record an {A : Group c c } (N : NormalSubGroup A ) (n x : Group.Carrier A ) : Set c where
73 open Group A 73 open Group A
74 open NormalSubGroup N 74 open NormalSubGroup N
75 field 75 field
76 a n : Group.Carrier A 76 a : Group.Carrier A
77 aN=x : a ∙ ⟦ n ⟧ ≈ x 77 aN=x : a ∙ ⟦ n ⟧ ≈ x
78
79 record aN {A : Group c c } (N : NormalSubGroup A ) : Set c where
80 field
81 n : Group.Carrier A
82 is-an : (x : Group.Carrier A) → an N n x
83
84 qid : {A : Group c c } (N : NormalSubGroup A ) → aN N
85 qid {A} N = record { n = ε ; is-an = λ x → record { a = x ; aN=x = ? } } where
86 open Group A
87 open NormalSubGroup N
78 88
79 _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c 89 _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c
80 _/_ A N = record { 90 _/_ A N = record {
81 Carrier = (x : Group.Carrier A) → aN N x 91 Carrier = aN N
82 ; _≈_ = _=n=_ 92 ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
83 ; _∙_ = qadd 93 ; _∙_ = qadd
84 ; ε = qid 94 ; ε = qid N
85 ; _⁻¹ = qinv 95 ; _⁻¹ = ?
86 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { 96 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
87 isEquivalence = record {refl = ? ; trans = ? ; sym = ? } 97 isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
88 ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} } 98 ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
89 ; assoc = ? } 99 ; assoc = ? }
90 ; identity = idL , (λ q → ? ) } 100 ; identity = ? , (λ q → ? ) }
91 ; inverse = ( (λ x → ? ) , (λ x → ? )) 101 ; inverse = ( (λ x → ? ) , (λ x → ? ))
92 ; ⁻¹-cong = λ i=j → ? 102 ; ⁻¹-cong = λ i=j → ?
93 } 103 }
94 } where 104 } where
95 open Group A 105 open Group A
96 open aN 106 open aN
107 open an
97 open NormalSubGroup N 108 open NormalSubGroup N
98 open IsGroupHomomorphism normal 109 open IsGroupHomomorphism normal
99 open EqReasoning (Algebra.Group.setoid A) 110 open EqReasoning (Algebra.Group.setoid A)
100 open Gutil A 111 open Gutil A
101 _=n=_ : (f g : (x : Group.Carrier A ) → aN N x ) → Set c 112 qadd : (f g : aN N) → aN N
102 f =n= g = {x y : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ 113 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
103 qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x 114 qadd0 : {x : Carrier} → x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x
104 qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where 115 qadd0 {x} = begin
105 q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x 116 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ ? ⟩
106 q00 = begin 117 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩
107 ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩ 118 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧ ∙ ⟦ n g ⟧ )) ≈⟨ ? ⟩
108 x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩ 119 x ⁻¹ ∙ (a (is-an f x) ∙ ( a (is-an g x) ∙ ⟦ n f ⟧) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩
109 x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl ) (∙-cong (grefl ) (∙-cong comm (grefl ) )) ⟩ 120 x ⁻¹ ∙ (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) ) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩
110 x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩ 121 x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩
111 x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl ) (aN=x (g x) ) ⟩ 122 x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩
112 x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl ) (aN=x (f x))) (grefl ) ⟩ 123 x ⁻¹ ∙ (x ∙ x) ≈⟨ ? ⟩
113 (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl ) ⟩ 124 x ∎
114 ε ∙ x ≈⟨ solve monoid ⟩
115 x ∎
116 qid : ( x : Carrier ) → aN N x
117 qid x = record { a = x ; n = ε ; aN=x = qid1 } where
118 qid1 : x ∙ ⟦ ε ⟧ ≈ x
119 qid1 = begin
120 x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
121 x ∙ ε ≈⟨ solve monoid ⟩
122 x ∎
123 qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x
124 qinv f x = record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; aN=x = qinv1 } where
125 qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x
126 qinv1 = begin
127 x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
128 x ∙ ⟦ (n (f x)) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
129 x ∙ ⟦ ((n (f x)) ⁻¹ ) ∙ n (f x) ⟧ ≈⟨ ? ⟩
130 x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
131 x ∙ ε ≈⟨ solve monoid ⟩
132 x ∎
133 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
134 qcong {x} {y} {u} {v} x=y u=v {w} {z} = begin
135 ⟦ n (x w) ∙ n (u w) ⟧ ≈⟨ homo _ _ ⟩
136 ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧ ≈⟨ ∙-cong x=y u=v ⟩
137 ⟦ n (y z) ⟧ ∙ ⟦ n (v z) ⟧ ≈⟨ gsym (homo _ _ ) ⟩
138 ⟦ n (y z) ∙ n (v z) ⟧ ∎
139 idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f
140 idL f = ?
141 125
142 -- K ⊂ ker(f) 126 -- K ⊂ ker(f)
143 K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c 127 K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
144 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where 128 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where
145 open Group H 129 open Group H
149 open import Function.Equality 133 open import Function.Equality
150 134
151 module _ (G : Group c c) (K : NormalSubGroup G) where 135 module _ (G : Group c c) (K : NormalSubGroup G) where
152 open Group G 136 open Group G
153 open aN 137 open aN
138 open an
154 open NormalSubGroup K 139 open NormalSubGroup K
155 open IsGroupHomomorphism normal 140 open IsGroupHomomorphism normal
156 open EqReasoning (Algebra.Group.setoid G) 141 open EqReasoning (Algebra.Group.setoid G)
157 open Gutil G 142 open Gutil G
158 143
159 φ : Group.Carrier G → Group.Carrier (G / K ) 144 φ : Group.Carrier G → Group.Carrier (G / K )
160 φ g x = record { a = g ; n = factor x g ; aN=x = is-factor x g } 145 φ g = record { n = factor ε g ; is-an = λ x → record { a = x ∙ ( ⟦ factor ε g ⟧ ⁻¹) ; aN=x = ? } }
161 146
162 φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ 147 φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
163 φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = 148 φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
164 record { cong = ? } }}} 149 record { cong = ? } }}}
165 150
166 φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) 151 φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K))
167 φe = record { _⟨$⟩_ = φ ; cong = ? } where 152 φe = record { _⟨$⟩_ = φ ; cong = ? } where
168 φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ 153 φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧
169 φ-cong = ? 154 φ-cong = ?
170 155
171 -- inverse ofφ 156 -- inverse ofφ
172 -- f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧ ) = (af)K , fn ≡ factor x af , af ≡ a (f x) 157 -- f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧ ) = (af)K , fn ≡ factor x af , af ≡ a (f x)
173 -- (inv-φ f)K ≡ (af)K 158 -- (inv-φ f)K ≡ (af)K
174 -- φ (inv-φ f) x → f (h0 x) 159 -- φ (inv-φ f) x → f (h0 x)
175 -- f x → φ (inv-φ f) (h1 x) 160 -- f x → φ (inv-φ f) (h1 x)
176 161
177 inv-φ : Group.Carrier (G / K ) → Group.Carrier G 162 inv-φ : Group.Carrier (G / K ) → Group.Carrier G
178 inv-φ f = ⟦ n (f ε) ⟧ ⁻¹ 163 inv-φ f = ⟦ n f ⟧ ⁻¹
179 164
180 an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹ 165
181 an02 f {x} = begin 166 cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
182 a (f x ) ≈⟨ gsym ( proj₂ identity _) ⟩
183 a (f x ) ∙ ε ≈⟨ ∙-cong (grefl ) (gsym (proj₂ inverse _)) ⟩
184 a (f x ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹) ≈⟨ solve monoid ⟩
185 (a (f x ) ∙ ⟦ n (f x) ⟧) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ∙-cong (aN=x (f x)) (grefl ) ⟩
186 x ∙ ⟦ n (f x) ⟧ ⁻¹ ∎
187
188 aNeqε : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g >
189 → {x : Carrier } → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
190 aNeqε {f} {g} f=g {x} = begin
191 ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
192 ε ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
193 (a (f x) ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ solve monoid ⟩
194 a (f x) ⁻¹ ∙ (a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ≈⟨ ? ⟩
195 a (f x) ⁻¹ ∙ a (g x) ≈⟨ ∙-cong (⁻¹-cong (an02 f) ) (an02 g) ⟩
196 (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (g x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
197 (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
198 ( ⟦ n (f x) ⟧ ∙ x ⁻¹ ) ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
199 ⟦ n (f x) ⟧ ∙ ( x ⁻¹ ∙ x ) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ? ⟩
200 ⟦ n (f x) ⟧ ∙ ε ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ solve monoid ⟩
201 ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ proj₂ inverse _ ⟩
202 ε ∎ where
203 an01 : a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ a (g x)
204 an01 = is-factor (a (g x)) (a (f x))
205 an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧
206 an03 = ?
207
208 cong-i : {f g : Group.Carrier (G / K ) } → ({x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ ) → inv-φ f ≈ inv-φ g
209 cong-i = ? 167 cong-i = ?
210 168
211 factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧ 169 is-inverse : (f : aN K ) → ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
212 factor=nf f {y} with f y 170 is-inverse f = begin
213 ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin 171 ⟦ n (φ (inv-φ f) ) ⟧ ≈⟨ grefl ⟩
214 ⟦ factor y z ⟧ ≈⟨ ? ⟩ 172 ⟦ n (φ (⟦ n f ⟧ ⁻¹) ) ⟧ ≈⟨ grefl ⟩
215 z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ 173 ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
216 z ⁻¹ ∙ y ≈⟨ ∙-cong (grefl ) (gsym faN=x ) ⟩ 174 ( ⟦ n f ⟧ ∙ ⟦ n f ⟧ ⁻¹) ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
217 z ⁻¹ ∙ ( fa ∙ ⟦ fn ⟧ ) ≈⟨ ? ⟩ 175 ⟦ n f ⟧ ∙ ( ⟦ n f ⟧ ⁻¹ ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
218 (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧ ≈⟨ ? ⟩ 176 ⟦ n f ⟧ ∙ ε ≈⟨ ? ⟩
219 ε ∙ ⟦ fn ⟧ ≈⟨ solve monoid ⟩ 177 ⟦ n f ⟧ ∎
220 ⟦ fn ⟧ ∎ where 178
221 z = fa ⁻¹ 179 φ-surjective : Surjective φe
222 180 φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse }
223 φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ 181
224 φ-factor f {x} {y} = begin
225 ⟦ n (f x) ⟧ ≈⟨ ? ⟩
226 ⟦ n (f x) ⟧ ∙ ε ≈⟨ ? ⟩
227 ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ⟦ n (f y) ⟧ ⁻¹ ) ≈⟨ cdr ( cdr an07 ) ⟩
228 ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ( ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ )) ≈⟨ ? ⟩
229 ⟦ n (f y) ⟧ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
230 ⟦ n (f y) ⟧ ∙ ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩
231 ⟦ n (f y) ⟧ ∙ ε ≈⟨ ? ⟩
232 ⟦ n (f y) ⟧ ∎ where
233 fxy = ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f y) ⟧
234
235 fa11 : a (f (x ∙ y ⁻¹ )) ∙ ⟦ n (f (x ∙ y ⁻¹)) ⟧ ≈ x ∙ y ⁻¹
236 fa11 = aN=x ( f ( x ∙ y ⁻¹ ))
237
238 fa21 : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
239 fa21 = aN=x ( f ε)
240
241 fa22 : {x : Carrier } → a (f (x ⁻¹)) ∙ ⟦ n (f (x ⁻¹)) ⟧ ≈ x ⁻¹
242 fa22 {x} = aN=x ( f (x ⁻¹))
243
244 fa14 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x
245 fa14 = aN=x ( f x)
246
247 fa13 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y
248 fa13 = aN=x ( f y)
249
250 fa12 : aN K ( x ∙ y ⁻¹ )
251 fa12 = f (x ∙ y ⁻¹ )
252 an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x)
253 an01 y = is-factor (a (f x)) y
254 an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x)
255 an04 = is-factor (a (f x)) (a (f y))
256 an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧
257 an07 {z} {w} = gsym ( is-factor z w )
258 an10 : ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈ ε
259 an10 = begin
260 ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩
261 ( a (f x) ∙ x ⁻¹ ) ⁻¹ ∙ (a (f y) ∙ y ⁻¹) ≈⟨ ? ⟩
262 x ∙ a (f x) ⁻¹ ∙ a (f y) ∙ y ⁻¹ ≈⟨ ? ⟩
263 ε ∎
264 an08 : ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈ ε
265 an08 = begin
266 ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
267 ε ∎
268 an05 : {z : Carrier} → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧
269 an05 {z} = begin
270 ⟦ n (f z) ⟧ ≈⟨ ? ⟩
271 ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧ ≈⟨ ? ⟩
272 (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧) ≈⟨ ∙-cong grefl (aN=x (f z)) ⟩
273 (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z)))) ⟩
274 (a (f z) ⁻¹) ∙ (a (f z) ∙ ⟦ factor z (a (f z)) ⟧ ) ≈⟨ ? ⟩
275 ⟦ factor z ( a ( f z)) ⟧ ∎
276 an06 : {z : Carrier} → ⟦ factor z z ⟧ ≈ ε
277 an06 {z} = begin
278 ⟦ factor z z ⟧ ≈⟨ ? ⟩
279 (z ⁻¹ ∙ z ) ∙ ⟦ factor z z ⟧ ≈⟨ ? ⟩
280 z ⁻¹ ∙ ( z ∙ ⟦ factor z z ⟧ ) ≈⟨ ∙-cong grefl (is-factor z z) ⟩
281 z ⁻¹ ∙ z ≈⟨ ? ⟩
282 ε ∎
283 an03 : ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈ ε
284 an03 = begin
285 ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈⟨ ? ⟩
286 ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x (a (f x)) ⟧ ≈⟨ ? ⟩
287 ⟦ factor y (a (f y)) ⟧ ⁻¹ ∙ ⟦ factor x ( x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⟧ ≈⟨ ? ⟩
288 ⟦ n (f (y ⁻¹ ∙ x)) ⟧ ≈⟨ ? ⟩
289 ⟦ factor (y ⁻¹ ∙ x) (a (f (y ⁻¹ ∙ x))) ⟧ ≈⟨ ? ⟩
290 ⟦ n (f ⟦ ε ⟧ ) ⟧ ≈⟨ ? ⟩
291 ⟦ ε ⟧ ≈⟨ ? ⟩ -- ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
292 ε ∎
293
294 is-inverse : (f : (x : Carrier) → aN K x ) → {x y : Carrier} → ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f y) ⟧
295 is-inverse f {x} {y} = begin
296 ⟦ n (φ (inv-φ f) x) ⟧ ≈⟨ grefl ⟩
297 ⟦ n (φ (⟦ n (f ε) ⟧ ⁻¹) x) ⟧ ≈⟨ grefl ⟩
298 ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
299 ε ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
300 (x ∙ x ⁻¹ ) ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
301 x ∙ ( x ⁻¹ ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ) ≈⟨ ? ⟩
302 x ∙ ⟦ n (f ε) ⟧ ⁻¹ ≈⟨ ? ⟩
303 y ∙ ⟦ n (f y) ⟧ ⁻¹ ≈⟨ ? ⟩
304 ⟦ n (f y) ⟧ ∎ where
305 afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
306 afn = aN=x (f ε)
307 afn' = (a (f y)) ⁻¹
308 f00 : ⟦ n (f ε) ⟧ ≈ (a (f y)) ⁻¹
309 f00 = begin
310 ⟦ n (f ε) ⟧ ≈⟨ ? ⟩
311 (a (f ε)) ⁻¹ ∙ a (f ε) ∙ ⟦ n (f ε) ⟧ ≈⟨ ? ⟩
312 (a (f ε)) ⁻¹ ∙ ε ≈⟨ ? ⟩
313 ⟦ n (f y) ⟧ ∙ y ⁻¹ ≈⟨ ? ⟩
314 (a (f y)) ⁻¹ ∙ ( a (f y) ∙ ⟦ n (f y) ⟧ ∙ y ⁻¹ ) ≈⟨ ? ⟩
315 (a (f y)) ⁻¹ ∎
316
317 φ-surjective : Surjective φe
318 φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = ? }
319
320 record FundamentalHomomorphism (G H : Group c c ) 182 record FundamentalHomomorphism (G H : Group c c )
321 (f : Group.Carrier G → Group.Carrier H ) 183 (f : Group.Carrier G → Group.Carrier H )
322 (homo : IsGroupHomomorphism (GR G) (GR H) f ) 184 (homo : IsGroupHomomorphism (GR G) (GR H) f )
323 (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where 185 (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where
324 open Group H 186 open Group H
325 field 187 field
326 h : Group.Carrier (G / K ) → Group.Carrier H 188 h : Group.Carrier (G / K ) → Group.Carrier H
327 h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h 189 h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h
328 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x ) 190 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x )
329 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → 191 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) →
330 ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) 192 ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
331 193
332 FundamentalHomomorphismTheorm : (G H : Group c c) 194 FundamentalHomomorphismTheorm : (G H : Group c c)
333 (f : Group.Carrier G → Group.Carrier H ) 195 (f : Group.Carrier G → Group.Carrier H )
334 (homo : IsGroupHomomorphism (GR G) (GR H) f ) 196 (homo : IsGroupHomomorphism (GR G) (GR H) f )
339 ; is-solution = is-solution 201 ; is-solution = is-solution
340 ; unique = unique 202 ; unique = unique
341 } where 203 } where
342 open Group H 204 open Group H
343 h : Group.Carrier (G / K ) → Group.Carrier H 205 h : Group.Carrier (G / K ) → Group.Carrier H
344 h r = f ( aN.n (r (Group.ε G ) )) 206 h r = f ( aN.n ? )
345 h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y 207 h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
346 h03 x y = {!!} 208 h03 x y = {!!}
347 h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h 209 h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h
348 h-homo = record { 210 h-homo = record {
349 isMonoidHomomorphism = record { 211 isMonoidHomomorphism = record {
350 isMagmaHomomorphism = record { 212 isMagmaHomomorphism = record {
351 isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 213 isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} }
352 ; homo = h03 } 214 ; homo = h03 }
353 ; ε-homo = {!!} } 215 ; ε-homo = {!!} }
354 ; ⁻¹-homo = {!!} } 216 ; ⁻¹-homo = {!!} }
355 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x ) 217 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x )
356 is-solution x = begin 218 is-solution x = begin
357 f x ≈⟨ ? ⟩ 219 f x ≈⟨ ? ⟩
358 ? ≈⟨ ? ⟩ 220 ? ≈⟨ ? ⟩
359 f ( aN.n (( φ G K x ) (Group.ε G ) )) ≈⟨ ? ⟩ 221 f ( aN.n (( φ G K ) (Group.ε G ) )) ≈⟨ ? ⟩
360 h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H ) 222 h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
361 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → 223 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) →
362 ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) 224 ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
363 unique = ? 225 unique = ?
364 226
365 227
366 228
367 229
230
231