Mercurial > hg > Members > kono > Proof > galois
changeset 283:b89af4300407
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 29 Jan 2023 11:28:56 +0900 (2023-01-29) |
parents | b70cc2534d2f |
children | 69645d667f45 |
files | src/Fundamental.agda |
diffstat | 1 files changed, 38 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Sun Jan 29 10:47:09 2023 +0900 +++ b/src/Fundamental.agda Sun Jan 29 11:28:56 2023 +0900 @@ -132,7 +132,7 @@ open import Function.Surjection open import Function.Equality -module _ (G : Group c c) (K : NormalSubGroup G) where +module GK (G : Group c c) (K : NormalSubGroup G) where open Group G open aN open an @@ -179,17 +179,33 @@ φ-surjective : Surjective φe φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } + gk00 : {x : Carrier } → ⟦ factor ε x ⟧ ⁻¹ ≈ x + gk00 {x} = begin + ⟦ factor ε x ⟧ ⁻¹ ≈⟨ ? ⟩ + ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ? ⟩ + ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x)) ⟩ + ( x ⁻¹ ∙ ε ) ⁻¹ ≈⟨ ? ⟩ + ( x ⁻¹ ) ⁻¹ ≈⟨ ? ⟩ + x ∎ + + gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x > + gk01 x = begin + ⟦ factor ε ( inv-φ x) ⟧ ≈⟨ ? ⟩ + ⟦ n x ⟧ ∎ + + record FundamentalHomomorphism (G H : Group c c ) (f : Group.Carrier G → Group.Carrier H ) (homo : IsGroupHomomorphism (GR G) (GR H) f ) (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where open Group H + open GK G K field h : Group.Carrier (G / K ) → Group.Carrier H h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h - is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → - ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) + → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) FundamentalHomomorphismTheorm : (G H : Group c c) (f : Group.Carrier G → Group.Carrier H ) @@ -201,9 +217,14 @@ ; is-solution = is-solution ; unique = unique } where + open GK G K open Group H + open Gutil H + open NormalSubGroup K + open IsGroupHomomorphism homo + open aN h : Group.Carrier (G / K ) → Group.Carrier H - h r = f ( aN.n ? ) + h r = f ( inv-φ r ) h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y h03 x y = {!!} h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h @@ -214,15 +235,19 @@ ; homo = h03 } ; ε-homo = {!!} } ; ⁻¹-homo = {!!} } - is-solution : (x : Group.Carrier G) → f x ≈ h ( φ G K x ) + open EqReasoning (Algebra.Group.setoid H) + is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) is-solution x = begin - f x ≈⟨ ? ⟩ - ? ≈⟨ ? ⟩ - f ( aN.n (( φ G K ) (Group.ε G ) )) ≈⟨ ? ⟩ - h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → - ( (x : Group.Carrier G) → f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) - unique = ? + f x ≈⟨ gsym ( ⟦⟧-cong (gk00 )) ⟩ + f ( Group._⁻¹ G ⟦ factor (Group.ε G) x ⟧ ) ≈⟨ grefl ⟩ + h ( φ x ) ∎ + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) + → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + unique h1 h1-homo h1-is-solution x = begin + h x ≈⟨ grefl ⟩ + f ( inv-φ x ) ≈⟨ h1-is-solution _ ⟩ + h1 ( φ ( inv-φ x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (gk01 x) ⟩ + h1 x ∎