Mercurial > hg > Members > kono > Proof > galois
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 |