Mercurial > hg > Members > kono > Proof > galois

annotate src/FundamentalHomorphism.agda @ 287:1874c573682f

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 16:50:56 +0900
parents f257ab4afa51
children d08663bae245
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- fundamental homomorphism theorem
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 --
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level hiding ( suc ; zero )
284
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
5 module FundamentalHomorphism (c : Level) where
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Algebra
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Algebra.Structures
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Algebra.Definitions
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
10 open import Algebra.Core
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
11 open import Algebra.Bundles
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
12
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Data.Product
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
14 open import Relation.Binary.PropositionalEquality
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
15 open import Gutil0
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
16 import Gutil
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
17 import Function.Definitions as FunctionDefinitions
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
18
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
19 import Algebra.Morphism.Definitions as MorphismDefinitions
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
20 open import Algebra.Morphism.Structures
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
269
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
22 open import Tactic.MonoidSolver using (solve; solve-macro)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
23
264
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
24 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
25 -- Given two groups G and H and a group homomorphism f : G → H,
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
26 -- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
27 -- (where G/K is the quotient group of G by K).
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
28 -- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
29 -- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
30 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
31 -- f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
32 -- G --→ H
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
33 -- | /
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
34 -- φ | / h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
35 -- ↓ /
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
36 -- G/K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
37 --
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
39 import Relation.Binary.Reasoning.Setoid as EqReasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
40
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
41 _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
42 m < x ∙ y > = Group._∙_ m x y
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
43
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
44 _<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c
277
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
45 m < x ≈ y > = Group._≈_ m x y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
46
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
47 infixr 9 _<_∙_>
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
48
261
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
49 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
50 -- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
51 --
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
53 open GroupMorphisms
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
55 -- import Axiom.Extensionality.Propositional
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
56 -- postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
57
286
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
58 open import Data.Empty
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
59 open import Relation.Nullary
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
60
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
61 record NormalSubGroup (A : Group c c ) : Set c where
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
62 open Group A
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
63 field
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
64 ⟦_⟧ : Group.Carrier A → Group.Carrier A
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
65 normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
66 comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b
286
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
67 -- because of ¬ ¬ Factor
275
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
68 factor : (a b : Carrier) → Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
69 is-factor : (a b : Carrier) → b ∙ ⟦ factor a b ⟧ ≈ a
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
70
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
71 -- Set of a ∙ ∃ n ∈ N
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
72 --
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
73 record an {A : Group c c } (N : NormalSubGroup A ) (n x : Group.Carrier A ) : Set c where
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
74 open Group A
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
75 open NormalSubGroup N
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
76 field
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
77 a : Carrier
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
78 aN=x : a ∙ ⟦ n ⟧ ≈ x
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
79
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
80 record aN {A : Group c c } (N : NormalSubGroup A ) : Set c where
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
81 open Group A
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
82 field
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
83 n : Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
84 is-an : (x : Carrier) → an N n x
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
85
286
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
86 record Factor (A : Group c c ) (N : NormalSubGroup A) (a b : Group.Carrier A ) : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
87 open Group A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
88 open NormalSubGroup N
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
89 open IsGroupHomomorphism normal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
90 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
91 factor : Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
92 is-factor : b ∙ ⟦ factor ⟧ ≈ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
93
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
94 ¬¬Factor : (A : Group c c ) (N : NormalSubGroup A) → ¬ ¬ ( (a b : Group.Carrier A ) → Factor A N a b )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
95 ¬¬Factor A N neg = ⊥-elim ( fa ( λ y → record { n = y ; is-an = λ x → record { a = x ∙ ⟦ y ⟧ ⁻¹ ; aN=x = f03 } } )) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
96 open Group A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
97 open NormalSubGroup N
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
98 open IsGroupHomomorphism normal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
99 open EqReasoning (Algebra.Group.setoid A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
100 open Gutil A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
101 open aN
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
102 f03 : {x y : Carrier } → x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
103 f03 {x} {y} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
104 x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
105 x ∙ ( ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧) ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
106 x ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
107 fa : ¬ ( (x : Carrier) → aN N )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
108 fa f = neg ( λ a b → record { factor = n (f ( a ∙ b ⁻¹)) ; is-factor = fa01 a b } ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
109 fa01 : (a b : Carrier ) → b ∙ ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
110 fa01 a b = begin
287
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
111 b ∙ ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
112 b ∙ ( ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ ( an.a (is-an (f ( a ∙ b ⁻¹) ) (a ∙ ⟦ b ⁻¹ ⟧ ) ) ∙ ⟦ n (f ( a ∙ b ⁻¹)) ⟧)) ≈⟨ cdr ( cdr (f06 ( a ∙ b ⁻¹) (a ∙ ⟦ b ⁻¹ ⟧ ))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
113 b ∙ ( ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ (a ∙ ⟦ b ⁻¹ ⟧ )) ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
114 ⟦ b ⟧ ∙ ( a ∙ ⟦ b ⁻¹ ⟧ ) ≈⟨ ? ⟩
286
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
115 a ∎ where
287
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
116 f06 : (x y : Carrier ) → an.a (is-an (f x) y ) ∙ ⟦ n (f x) ⟧ ≈ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
117 f06 x y = an.aN=x (is-an (f x) y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
118 f07 : (y : Carrier ) → an.a (is-an (f ( a ∙ b ⁻¹)) y ) ∙ ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
119 f07 y = an.aN=x (is-an (f ( a ∙ b ⁻¹)) y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
120 f08 : ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ ( an.a (is-an (f ( a ∙ b ⁻¹) ) (a ∙ ⟦ b ⁻¹ ⟧ ))) ≈ ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 286
diff changeset
121 f08 = ?
286
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 285
diff changeset
122
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
123 _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
124 _/_ A N = record {
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
125 Carrier = aN N
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
126 ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
127 ; _∙_ = qadd
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
128 ; ε = qid
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
129 ; _⁻¹ = ?
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
130 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
131 isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
132 ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
133 ; assoc = ? }
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
134 ; identity = ? , (λ q → ? ) }
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
135 ; inverse = ( (λ x → ? ) , (λ x → ? ))
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
136 ; ⁻¹-cong = λ i=j → ?
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
137 }
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
138 } where
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
139 open Group A
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
140 open aN
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
141 open an
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
142 open NormalSubGroup N
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
143 open IsGroupHomomorphism normal
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
144 open EqReasoning (Algebra.Group.setoid A)
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
145 open Gutil A
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
146 qadd : (f g : aN N) → aN N
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
147 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
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
148 qadd0 : {x : Carrier} → x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
149 qadd0 {x} = begin
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
150 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
151 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
152 x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧ ∙ ⟦ n g ⟧ )) ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
153 x ⁻¹ ∙ (a (is-an f x) ∙ ( a (is-an g x) ∙ ⟦ n f ⟧) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
154 x ⁻¹ ∙ (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) ) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
155 x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
156 x ⁻¹ ∙ (x ∙ x) ≈⟨ ? ⟩
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
157 (x ⁻¹ ∙ x ) ∙ x ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
158 ε ∙ x ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
159 x ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
160 qid : aN N
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
161 qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
162 qid1 : {x : Carrier } → x ∙ ⟦ ε ⟧ ≈ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
163 qid1 {x} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
164 x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
165 x ∙ ε ≈⟨ proj₂ identity _ ⟩
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
166 x ∎
271
c209aebeab2a Fundamental again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
167
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
168
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
169 -- K ⊂ ker(f)
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
170 K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
171 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
172 open Group H
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
173 open NormalSubGroup K
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
174
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
175 open import Function.Surjection
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
176 open import Function.Equality
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
177
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
178 module GK (G : Group c c) (K : NormalSubGroup G) where
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
179 open Group G
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
180 open aN
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
181 open an
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
182 open NormalSubGroup K
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
183 open IsGroupHomomorphism normal
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
184 open EqReasoning (Algebra.Group.setoid G)
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
185 open Gutil G
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
186
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
187 φ : Group.Carrier G → Group.Carrier (G / K )
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
188 φ g = record { n = factor ε g ; is-an = λ x → record { a = x ∙ ( ⟦ factor ε g ⟧ ⁻¹) ; aN=x = ? } }
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
189
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
190 φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
191 φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
192 record { cong = ? } }}}
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
193
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
194 φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K))
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
195 φe = record { _⟨$⟩_ = φ ; cong = ? } where
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
196 φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
197 φ-cong = ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
198
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
199 -- inverse ofφ
277
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
200 -- f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧ ) = (af)K , fn ≡ factor x af , af ≡ a (f x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
201 -- (inv-φ f)K ≡ (af)K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
202 -- φ (inv-φ f) x → f (h0 x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
203 -- f x → φ (inv-φ f) (h1 x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
204
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
205 inv-φ : Group.Carrier (G / K ) → Group.Carrier G
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
206 inv-φ f = ⟦ n f ⟧ ⁻¹
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
207
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
208
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
209 cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
210 cong-i = ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
211
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
212 is-inverse : (f : aN K ) → ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
213 is-inverse f = begin
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
214 ⟦ n (φ (inv-φ f) ) ⟧ ≈⟨ grefl ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
215 ⟦ n (φ (⟦ n f ⟧ ⁻¹) ) ⟧ ≈⟨ grefl ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
216 ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
217 ε ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
218 ( ⟦ n f ⟧ ∙ ⟦ n f ⟧ ⁻¹) ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
219 ⟦ n f ⟧ ∙ ( ⟦ n f ⟧ ⁻¹ ∙ ⟦ factor ε (⟦ n f ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
220 ⟦ n f ⟧ ∙ ε ≈⟨ ? ⟩
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
221 ⟦ n f ⟧ ∎
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
222
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
223 φ-surjective : Surjective φe
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
224 φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse }
276
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 275
diff changeset
225
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
226 gk00 : {x : Carrier } → ⟦ factor ε x ⟧ ⁻¹ ≈ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
227 gk00 {x} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
228 ⟦ factor ε x ⟧ ⁻¹ ≈⟨ ? ⟩
285
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
229 (ε ∙ ⟦ factor ε x ⟧) ⁻¹ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
230 ( ( x ⁻¹ ∙ x ) ∙ ⟦ factor ε x ⟧ ) ⁻¹ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
231 ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x)) ⟩
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
232 ( x ⁻¹ ∙ ε ) ⁻¹ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
233 ( x ⁻¹ ) ⁻¹ ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
234 x ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
235
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
236 gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
237 gk01 x = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
238 ⟦ factor ε ( inv-φ x) ⟧ ≈⟨ ? ⟩
284
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
239 ( inv-φ x ) ⁻¹ ∙ ( inv-φ x ∙ ⟦ factor ε ( inv-φ x) ⟧) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
240 ( inv-φ x ) ⁻¹ ∙ ε ≈⟨ ? ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
241 ( ⟦ n x ⟧ ⁻¹) ⁻¹ ≈⟨ ? ⟩
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
242 ⟦ n x ⟧ ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
243
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
244
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
245 record FundamentalHomomorphism (G H : Group c c )
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
246 (f : Group.Carrier G → Group.Carrier H )
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
247 (homo : IsGroupHomomorphism (GR G) (GR H) f )
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
248 (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
249 open Group H
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
250 open GK G K
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
251 field
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
252 h : Group.Carrier (G / K ) → Group.Carrier H
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
253 h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
254 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
255 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
256 → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
257
d500309866da fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
257
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
258 FundamentalHomomorphismTheorm : (G H : Group c c)
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
259 (f : Group.Carrier G → Group.Carrier H )
264
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
260 (homo : IsGroupHomomorphism (GR G) (GR H) f )
260
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
261 (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
262 FundamentalHomomorphismTheorm G H f homo K kf = record {
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
263 h = h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
264 ; h-homo = h-homo
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
265 ; is-solution = is-solution
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
266 ; unique = unique
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
267 } where
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
268 open GK G K
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
269 open Group H
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
270 open Gutil H
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
271 open NormalSubGroup K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
272 open IsGroupHomomorphism homo
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
273 open aN
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
274 h : Group.Carrier (G / K ) → Group.Carrier H
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
275 h r = f ( inv-φ r )
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
276 h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
277 h03 x y = {!!}
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
278 h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h
260
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
279 h-homo = record {
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
280 isMonoidHomomorphism = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
281 isMagmaHomomorphism = record {
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
282 isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} }
260
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
283 ; homo = h03 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
284 ; ε-homo = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
285 ; ⁻¹-homo = {!!} }
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
286 open EqReasoning (Algebra.Group.setoid H)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
287 is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x )
272
ce372f6347d6 Foundamental definition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
288 is-solution x = begin
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
289 f x ≈⟨ gsym ( ⟦⟧-cong (gk00 )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
290 f ( Group._⁻¹ G ⟦ factor (Group.ε G) x ⟧ ) ≈⟨ grefl ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
291 h ( φ x ) ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
292 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
293 → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
294 unique h1 h1-homo h1-is-solution x = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
295 h x ≈⟨ grefl ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
296 f ( inv-φ x ) ≈⟨ h1-is-solution _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
297 h1 ( φ ( inv-φ x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (gk01 x) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
298 h1 x ∎
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
301
259
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
302
282
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
303
b70cc2534d2f double record on quontient group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
304