Mercurial > hg > Members > kono > Proof > galois

comparison src/homomorphism.agda @ 302:3812936d52c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove lift
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 07 Sep 2023 11:45:11 +0900
parents 38f4e5d35c8b
children
comparison
equal deleted inserted replaced
301:38f4e5d35c8b 302:3812936d52c8
49 open import Relation.Nullary 49 open import Relation.Nullary
50 50
51 -- Set of a ∙ ∃ n ∈ N 51 -- Set of a ∙ ∃ n ∈ N
52 -- 52 --
53 53
54 data IsaN {c d : Level} {A : Group c d } (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where 54 data IsaN {c d : Level} {A : Group c d } (N : NormalSubGroup {d} A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
55 an : (n x : Group.Carrier A ) → A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x 55 an : (n x : Group.Carrier A ) → A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x
56 56
57 record aNeq {c d : Level} {A : Group c d } (N : NormalSubGroup A ) (a b : Group.Carrier A) : Set (Level.suc c ⊔ d) where 57 record aNeq {c d : Level} {A : Group c d } (N : NormalSubGroup A ) (a b : Group.Carrier A) : Set (Level.suc c ⊔ d) where
58 field 58 field
59 eq→ : {x : Group.Carrier A} → IsaN N a x → IsaN N b x 59 eq→ : {x : Group.Carrier A} → IsaN N a x → IsaN N b x
60 eq← : {x : Group.Carrier A} → IsaN N b x → IsaN N a x 60 eq← : {x : Group.Carrier A} → IsaN N b x → IsaN N a x
61 61
62 module AN {c d : Level} (A : Group c d) (N : NormalSubGroup A ) where 62 module AN {c d : Level} (A : Group c d) (N : NormalSubGroup {d} A ) where
63 open Group A 63 open Group A
64 open NormalSubGroup N 64 open NormalSubGroup N
65 open EqReasoning (Algebra.Group.setoid A) 65 open EqReasoning (Algebra.Group.setoid A)
66 open Gutil A 66 open Gutil A
67 open aNeq 67 open aNeq
229 x ⁻¹ ∙ (n ⁻¹) ⁻¹ ≈⟨ cdr f⁻¹⁻¹≈f ⟩ 229 x ⁻¹ ∙ (n ⁻¹) ⁻¹ ≈⟨ cdr f⁻¹⁻¹≈f ⟩
230 x ⁻¹ ∙ n ≈⟨ eq ⟩ 230 x ⁻¹ ∙ n ≈⟨ eq ⟩
231 a ∎ 231 a ∎
232 232
233 -- K ⊂ ker(f) 233 -- K ⊂ ker(f)
234 K⊆ker : {c d : Level} (G H : Group c d) (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) 234 K⊆ker : {c d : Level} (G H : Group c d) (K : NormalSubGroup {d} G ) (f : Group.Carrier G → Group.Carrier H )
235 → Set (Level.suc c ⊔ d) 235 → Set (c ⊔ d)
236 K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where 236 K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε where
237 open Group H 237 open Group H
238 open NormalSubGroup K 238 open NormalSubGroup K
239 239
240 open import Function.Surjection 240 open import Function.Surjection
309 open IsGroupHomomorphism f-homo 309 open IsGroupHomomorphism f-homo
310 open EqReasoning (Algebra.Group.setoid H) 310 open EqReasoning (Algebra.Group.setoid H)
311 311
312 Imf : NormalSubGroup G 312 Imf : NormalSubGroup G
313 Imf = record { 313 Imf = record {
314 P = λ x → Lift (Level.suc c ⊔ d) (f x ≈ ε) 314 P = λ x → f x ≈ ε
315 ; Pε = lift ε-homo 315 ; Pε = ε-homo
316 ; P⁻¹ = im01 316 ; P⁻¹ = im01
317 ; P≈ = im02 317 ; P≈ = im02
318 ; P∙ = im03 318 ; P∙ = im03
319 ; Pcomm = im04 319 ; Pcomm = im04
320 } where 320 } where
321 open NormalSubGroup K 321 open NormalSubGroup K
322 GC = Group.Carrier G 322 GC = Group.Carrier G
323 im01 : (a : Group.Carrier G) → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f ((G Group.⁻¹) a) ≈ ε) 323 im01 : (a : Group.Carrier G) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε
324 im01 a (lift fa=e) = lift (begin 324 im01 a fa=e = begin
325 f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ 325 f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩
326 f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ 326 f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩
327 ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ 327 ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩
328 ε ∎ ) 328 ε ∎
329 im00 : (a : GC) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε 329 im00 : (a : GC) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε
330 im00 a fa=e = begin 330 im00 a fa=e = begin
331 f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩ 331 f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩
332 f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩ 332 f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩
333 ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩ 333 ε ⁻¹ ≈⟨ gsym ε≈ε⁻¹ ⟩
334 ε ∎ 334 ε ∎
335 im02 : {a b : GC} → G < a ≈ b > → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f b ≈ ε) 335 im02 : {a b : GC} → G < a ≈ b > → f a ≈ ε → f b ≈ ε
336 im02 {a} {b} a=b (lift fa=e) = lift ( begin 336 im02 {a} {b} a=b fa=e = begin
337 f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩ 337 f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩
338 f a ≈⟨ fa=e ⟩ 338 f a ≈⟨ fa=e ⟩
339 ε ∎ ) where 339 ε ∎ where
340 open import Gutil G as GU 340 open import Gutil G as GU
341 im04 : {a b : Group.Carrier G} → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) 341 im04 : {a b : Group.Carrier G} → f a ≈ ε →
342 (f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε) 342 f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε
343 im04 {a} {b} (lift fa=e) = lift ( begin 343 im04 {a} {b} fa=e = begin
344 f ( G < b ∙ G < a ∙ (G Group.⁻¹) b > > ) ≈⟨ homo _ _ ⟩ 344 f ( G < b ∙ G < a ∙ (G Group.⁻¹) b > > ) ≈⟨ homo _ _ ⟩
345 f b ∙ f ( G < a ∙ (G Group.⁻¹) b > ) ≈⟨ cdr (homo _ _) ⟩ 345 f b ∙ f ( G < a ∙ (G Group.⁻¹) b > ) ≈⟨ cdr (homo _ _) ⟩
346 f b ∙ ( f a ∙ f ((G Group.⁻¹) b )) ≈⟨ cdr (cdr (⁻¹-homo _)) ⟩ 346 f b ∙ ( f a ∙ f ((G Group.⁻¹) b )) ≈⟨ cdr (cdr (⁻¹-homo _)) ⟩
347 f b ∙ ( f a ∙ f b ⁻¹ ) ≈⟨ cdr (car fa=e) ⟩ 347 f b ∙ ( f a ∙ f b ⁻¹ ) ≈⟨ cdr (car fa=e) ⟩
348 f b ∙ ( ε ∙ f b ⁻¹ ) ≈⟨ solve monoid ⟩ 348 f b ∙ ( ε ∙ f b ⁻¹ ) ≈⟨ solve monoid ⟩
349 f b ∙ f b ⁻¹ ≈⟨ proj₂ inverse _ ⟩ 349 f b ∙ f b ⁻¹ ≈⟨ proj₂ inverse _ ⟩
350 ε ∎ ) 350 ε ∎
351 im03 : {a b : Group.Carrier G} → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f b ≈ ε) → 351 im03 : {a b : Group.Carrier G} → f a ≈ ε → f b ≈ ε →
352 Lift (Level.suc c ⊔ d) (f ((G Group.∙ a) b) ≈ ε) 352 f ((G Group.∙ a) b) ≈ ε
353 im03 {a} {b} (lift fa=e) (lift fb=e) = lift (begin 353 im03 {a} {b} fa=e fb=e = begin
354 f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩ 354 f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩
355 f a ∙ f b ≈⟨ ∙-cong fa=e fb=e ⟩ 355 f a ∙ f b ≈⟨ ∙-cong fa=e fb=e ⟩
356 ε ∙ ε ≈⟨ proj₁ identity _ ⟩ 356 ε ∙ ε ≈⟨ proj₁ identity _ ⟩
357 ε ∎ ) 357 ε ∎
358
359 h05 : Group _ _
360 h05 = G / Imf
358 361
359 h : Group.Carrier (G / K ) → Group.Carrier H 362 h : Group.Carrier (G / K ) → Group.Carrier H
360 h r = f ( GK.inv-φ G K r ) 363 h r = f r
361 h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y 364 h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
362 h03 = ? 365 h03 x y = homo _ _
366 h04 : {x y : Group.Carrier G} → aNeq K x y → h x ≈ h y
367 h04 {x} {y} x=y = ?
363 h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h 368 h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h
364 h-homo = record { 369 h-homo = record {
365 isMonoidHomomorphism = record { 370 isMonoidHomomorphism = record {
366 isMagmaHomomorphism = record { 371 isMagmaHomomorphism = record {
367 isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 372 isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq }
368 ; homo = h03 } 373 ; homo = h03 }
369 ; ε-homo = {!!} } 374 ; ε-homo = ε-homo }
370 ; ⁻¹-homo = {!!} } 375 ; ⁻¹-homo = ⁻¹-homo }
371 is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ ? ? x ) 376 is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ ? ? x )
372 is-solution x = begin 377 is-solution x = begin
373 f x ≈⟨ ? ⟩ 378 f x ≈⟨ ? ⟩
374 h ( GK.φ ? ? x ) ∎ 379 h ( GK.φ ? ? x ) ∎
375 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) 380 unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )