|
1102
|
1 -- Free Group and it's Universal Mapping
|
|
|
2 ---- using Sets and forgetful functor
|
|
|
3
|
|
|
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
|
5
|
|
|
6 open import Category -- https://github.com/konn/category-agda
|
|
|
7 open import Level
|
|
|
8 module group { c c₁ c₂ ℓ : Level } where
|
|
|
9
|
|
|
10 open import Category.Sets
|
|
|
11 open import Category.Cat
|
|
|
12 open import HomReasoning
|
|
|
13 open import cat-utility
|
|
|
14 open import Relation.Binary.Structures
|
|
|
15 open import universal-mapping
|
|
|
16 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
17
|
|
|
18 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeGroup.agda
|
|
|
19
|
|
1105
|
20 -- fundamental homomorphism theorem
|
|
|
21 --
|
|
|
22
|
|
1102
|
23 open import Algebra
|
|
1105
|
24 open import Algebra.Structures
|
|
|
25 open import Algebra.Definitions
|
|
1102
|
26 open import Algebra.Core
|
|
1105
|
27 open import Algebra.Bundles
|
|
|
28
|
|
1102
|
29 open import Data.Product
|
|
1105
|
30 import Function.Definitions as FunctionDefinitions
|
|
|
31
|
|
|
32 import Algebra.Morphism.Definitions as MorphismDefinitions
|
|
|
33 open import Algebra.Morphism.Structures
|
|
|
34
|
|
|
35 open import Tactic.MonoidSolver using (solve; solve-macro)
|
|
1102
|
36
|
|
1105
|
37 --
|
|
|
38 -- Given two groups G and H and a group homomorphism f : G → H,
|
|
|
39 -- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
|
|
|
40 -- (where G/K is the quotient group of G by K).
|
|
|
41 -- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
|
|
|
42 -- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
|
|
|
43 --
|
|
|
44 -- f
|
|
|
45 -- G --→ H
|
|
|
46 -- | /
|
|
|
47 -- φ | / h
|
|
|
48 -- ↓ /
|
|
|
49 -- G/K
|
|
|
50 --
|
|
1102
|
51
|
|
1105
|
52 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
53
|
|
|
54 _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m
|
|
|
55 m < x ∙ y > = Group._∙_ m x y
|
|
1102
|
56
|
|
|
57 infixr 9 _<_∙_>
|
|
|
58
|
|
1105
|
59 --
|
|
|
60 -- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n }
|
|
|
61 --
|
|
|
62
|
|
|
63
|
|
|
64 open GroupMorphisms
|
|
|
65
|
|
|
66 import Axiom.Extensionality.Propositional
|
|
|
67 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
|
|
1102
|
68
|
|
1105
|
69 GR : {c l : Level } → Group c l → RawGroup c l
|
|
|
70 GR G = record {
|
|
|
71 Carrier = Carrier G
|
|
|
72 ; _≈_ = _≈_ G
|
|
|
73 ; _∙_ = _∙_ G
|
|
|
74 ; ε = ε G
|
|
|
75 ; _⁻¹ = _⁻¹ G
|
|
|
76 } where open Group
|
|
|
77
|
|
|
78 grefl : {c l : Level } → (G : Group c l ) → {x : Group.Carrier G} → Group._≈_ G x x
|
|
|
79 grefl G = IsGroup.refl ( Group.isGroup G )
|
|
1102
|
80
|
|
1105
|
81 gsym : {c l : Level } → (G : Group c l ) → {x y : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y x
|
|
|
82 gsym G = IsGroup.sym ( Group.isGroup G )
|
|
|
83
|
|
|
84 gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z
|
|
|
85 gtrans G = IsGroup.trans ( Group.isGroup G )
|
|
|
86
|
|
|
87 record NormalSubGroup (A : Group c c ) : Set c where
|
|
|
88 open Group A
|
|
|
89 field
|
|
|
90 ⟦_⟧ : Group.Carrier A → Group.Carrier A
|
|
|
91 normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧
|
|
|
92 comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b
|
|
|
93
|
|
|
94 -- Set of a ∙ ∃ n ∈ N
|
|
|
95 --
|
|
|
96 record aN {A : Group c c } (N : NormalSubGroup A ) (x : Group.Carrier A ) : Set c where
|
|
|
97 open Group A
|
|
|
98 open NormalSubGroup N
|
|
|
99 field
|
|
|
100 a n : Group.Carrier A
|
|
|
101 aN=x : a ∙ ⟦ n ⟧ ≈ x
|
|
|
102
|
|
|
103 open import Tactic.MonoidSolver using (solve; solve-macro)
|
|
1102
|
104
|
|
|
105
|
|
1105
|
106 _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c
|
|
|
107 _/_ A N = record {
|
|
|
108 Carrier = (x : Group.Carrier A ) → aN N x
|
|
|
109 ; _≈_ = _=n=_
|
|
|
110 ; _∙_ = qadd
|
|
|
111 ; ε = qid
|
|
|
112 ; _⁻¹ = λ f x → record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; aN=x = ? }
|
|
|
113 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
114 isEquivalence = record {refl = grefl A ; trans = ? ; sym = ? }
|
|
|
115 ; ∙-cong = ? }
|
|
|
116 ; assoc = ? }
|
|
|
117 ; identity = idL , (λ q → ? ) }
|
|
|
118 ; inverse = ( (λ x → ? ) , (λ x → ? ))
|
|
|
119 ; ⁻¹-cong = λ i=j → ?
|
|
|
120 }
|
|
|
121 } where
|
|
|
122 open Group A
|
|
|
123 open aN
|
|
|
124 open NormalSubGroup N
|
|
|
125 open IsGroupHomomorphism normal
|
|
|
126 open EqReasoning (Algebra.Group.setoid A)
|
|
|
127 _=n=_ : (f g : (x : Group.Carrier A ) → aN N x ) → Set c
|
|
|
128 f =n= g = {x : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧
|
|
|
129 qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x
|
|
|
130 qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
|
|
|
131 q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x
|
|
|
132 q00 = begin
|
|
|
133 ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
|
|
|
134 x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
|
|
|
135 x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) )) ⟩
|
|
|
136 x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩
|
|
|
137 x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl A) (aN=x (g x) ) ⟩
|
|
|
138 x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A) ⟩
|
|
|
139 (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A) ⟩
|
|
|
140 ε ∙ x ≈⟨ solve monoid ⟩
|
|
|
141 x ∎
|
|
|
142 qid : ( x : Carrier ) → aN N x
|
|
|
143 qid x = record { a = x ; n = ε ; aN=x = qid1 } where
|
|
|
144 qid1 : x ∙ ⟦ ε ⟧ ≈ x
|
|
|
145 qid1 = begin
|
|
|
146 x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩
|
|
|
147 x ∙ ε ≈⟨ solve monoid ⟩
|
|
|
148 x ∎
|
|
|
149 qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x
|
|
|
150 qinv f x = record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; aN=x = qinv1 } where
|
|
|
151 qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x
|
|
|
152 qinv1 = begin
|
|
|
153 x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
|
|
|
154 x ∙ ⟦ (n (f x)) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
|
|
|
155 x ∙ ⟦ ((n (f x)) ⁻¹ ) ∙ n (f x) ⟧ ≈⟨ ? ⟩
|
|
|
156 x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩
|
|
|
157 x ∙ ε ≈⟨ solve monoid ⟩
|
|
|
158 x ∎
|
|
|
159 idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f
|
|
|
160 idL f = ?
|
|
1102
|
161
|
|
1105
|
162 -- K ⊂ ker(f)
|
|
|
163 K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
|
|
|
164 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where
|
|
|
165 open Group H
|
|
|
166 open NormalSubGroup K
|
|
1102
|
167
|
|
1105
|
168 open import Function.Surjection
|
|
|
169 open import Function.Equality
|
|
|
170
|
|
|
171 module _ (G : Group c c) (K : NormalSubGroup G) where
|
|
|
172 open Group G
|
|
|
173 open aN
|
|
|
174 open NormalSubGroup K
|
|
|
175 open IsGroupHomomorphism normal
|
|
|
176
|
|
|
177 φ : Group.Carrier G → Group.Carrier (G / K )
|
|
|
178 φ g x = record { a = x ; n = ε ; aN=x = gtrans G ( ∙-cong (grefl G) ε-homo) (solve monoid) } where
|
|
|
179
|
|
|
180 φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
|
|
|
181 φ-homo = ?
|
|
|
182
|
|
|
183 φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K))
|
|
|
184 φe = record { _⟨$⟩_ = φ ; cong = φ-cong } where
|
|
|
185 φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧
|
|
|
186 φ-cong = ?
|
|
|
187
|
|
|
188 inv-φ : Group.Carrier (G / K ) → Group.Carrier G
|
|
|
189 inv-φ f = ⟦ n (f ε) ⟧
|
|
1102
|
190
|
|
1105
|
191 φ-surjective : Surjective φe
|
|
|
192 φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } where
|
|
|
193 cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
|
|
|
194 cong-i = ?
|
|
|
195 is-inverse : (f : (x : Carrier) → aN K x ) → {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
|
|
|
196 is-inverse = ?
|
|
|
197
|
|
|
198 record FundamentalHomomorphism (G H : Group c c )
|
|
|
199 (f : Group.Carrier G → Group.Carrier H )
|
|
|
200 (homo : IsGroupHomomorphism (GR G) (GR H) f )
|
|
|
201 (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where
|
|
|
202 open Group H
|
|
|
203 field
|
|
|
204 h : Group.Carrier (G / K ) → Group.Carrier H
|
|
|
205 h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h
|
|
|
206 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x )
|
|
|
207 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) →
|
|
|
208 ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
|
|
|
209
|
|
|
210 postulate
|
|
|
211 FundamentalHomomorphismTheorm : (G H : Group c c)
|
|
|
212 (f : Group.Carrier G → Group.Carrier H )
|
|
|
213 (homo : IsGroupHomomorphism (GR G) (GR H) f )
|
|
|
214 (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf
|
|
|
215
|
|
|
216 Homomorph : ?
|
|
|
217 Homomorph = ?
|
|
|
218
|
|
|
219 _==_ : ?
|
|
|
220 _==_ = ?
|
|
|
221
|
|
|
222 _*_ : ?
|
|
|
223 _*_ = ?
|
|
|
224
|
|
|
225 morph : ?
|
|
|
226 morph = ?
|
|
|
227
|
|
|
228 isGroups : IsCategory (Group c c) ? ? ? ?
|
|
1102
|
229 isGroups = record { isEquivalence = isEquivalence1
|
|
|
230 ; identityL = refl
|
|
|
231 ; identityR = refl
|
|
|
232 ; associative = refl
|
|
|
233 ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
|
|
|
234 }
|
|
|
235 where
|
|
1105
|
236 isEquivalence1 : { a b : (Group c c) } → ?
|
|
1102
|
237 isEquivalence1 = -- this is the same function as A's equivalence but has different types
|
|
|
238 record { refl = refl
|
|
|
239 ; sym = sym
|
|
|
240 ; trans = trans
|
|
|
241 }
|
|
1105
|
242 o-resp-≈ : {a b c' : Group c c } {f g : ? } → {h i : ? } →
|
|
1102
|
243 f == g → h == i → (h * f) == (i * g)
|
|
1105
|
244 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open EqReasoning (Algebra.Group.setoid ?) in begin
|
|
1102
|
245 morph ( h * f )
|
|
1105
|
246 ≈⟨ ? ⟩
|
|
1102
|
247 morph ( i * g )
|
|
|
248 ∎ where
|
|
1105
|
249 open Group c
|
|
|
250 lemma11 : (x : Group.Carrier a) → morph (h * f) x ≈ morph (i * g) x
|
|
|
251 lemma11 x = let open EqReasoning (Algebra.Group.setoid c) in begin
|
|
|
252 morph ( h * f ) x ≈⟨ grefl c ⟩
|
|
|
253 morph h ( ( morph f ) x ) ≈⟨ ? ⟩
|
|
|
254 morph h ( morph g x ) ≈⟨ ? ⟩
|
|
|
255 morph i ( morph g x ) ≈⟨ grefl c ⟩
|
|
1102
|
256 morph ( i * g ) x ∎
|
|
|
257
|
|
|
258 Groups : Category _ _ _
|
|
|
259 Groups =
|
|
1105
|
260 record { Obj = Group c c
|
|
|
261 ; Hom = ?
|
|
1102
|
262 ; _o_ = _*_
|
|
|
263 ; _≈_ = _==_
|
|
1105
|
264 ; Id = ?
|
|
1102
|
265 ; isCategory = isGroups
|
|
|
266 }
|
|
|
267
|
|
1105
|
268 open import Data.Unit
|
|
1102
|
269
|
|
1103
|
270 GC : (G : Obj Groups ) → Category c c (suc c)
|
|
1105
|
271 GC G = record { Obj = Lift c ⊤ ; Hom = λ _ _ → Group.Carrier G ; _o_ = Group._∙_ G }
|
|
1103
|
272
|
|
1105
|
273 F : (G H : Obj Groups ) → (f : Homomorph G H ) → (K : NormalSubGroup G) → Functor (GC H) (GC (G / K))
|
|
1104
|
274 F G H f K = record { FObj = λ _ → lift tt ; FMap = λ x y → record { a = ? ; n = ? ; x=aN = ? } ; isFunctor = ? }
|
|
1103
|
275
|
|
|
276 -- f f ε
|
|
|
277 -- G --→ H G --→ H (a)
|
|
|
278 -- | / | /
|
|
|
279 -- φ | / h φ | /h ↑
|
|
|
280 -- ↓ / ↓ /
|
|
|
281 -- G/K G/K
|
|
|
282
|
|
1105
|
283 fundamentalTheorem : (G H : Obj Groups ) → (K : NormalSubGroup G) → (f : Homomorph G H )
|
|
|
284 → ( kerf⊆K : (x : Group.Carrier G) → aN K x → morph f x ≡ Group.ε H )
|
|
1103
|
285 → coUniversalMapping (GC H) (GC (G / K)) (F G H f K )
|
|
1105
|
286 fundamentalTheorem G H K f kerf⊆K = record { U = λ _ → lift tt ; ε = λ _ g → record { a = ? ; n = ? ; x=aN = ? }
|
|
1104
|
287 ; _* = λ {b} {a} g → solution {b} {a} g ; iscoUniversalMapping
|
|
|
288 = record { couniversalMapping = ? ; uniquness = ? }} where
|
|
1103
|
289 m : Homomorph G G
|
|
1105
|
290 m = NormalSubGroup.normal K
|
|
|
291 φ⁻¹ : Group.Carrier (G / K) → Group.Carrier G
|
|
1103
|
292 φ⁻¹ = ?
|
|
1104
|
293 solution : {b : Obj (GC (G / K))} {a : Obj (GC H)} { f0 : Hom (GC (G / K)) (lift tt) b} →
|
|
|
294 GC (G / K) [ GC (G / K) [ (λ g → record { a = ? ; n = ? ; x=aN = ? }) o
|
|
|
295 (λ y → record { a = ? ; n = ? ; x=aN = ? }) ] ≈ f0 ]
|
|
|
296 solution = ?
|
|
|
297 is-solution : ?
|
|
1103
|
298 is-solution a b g = ?
|
|
1102
|
299
|
|
|
300
|
