# HG changeset patch # User Shinji KONO # Date 1674663398 -32400 # Node ID 691b2ee844efbeb900498927795206a330291c74 # Parent 9bee24b4017f6f7901f1cafce41c2432cd347de3 ... diff -r 9bee24b4017f -r 691b2ee844ef src/Fundamental.agda --- a/src/Fundamental.agda Tue Jan 24 23:38:32 2023 +0900 +++ b/src/Fundamental.agda Thu Jan 26 01:16:38 2023 +0900 @@ -70,35 +70,17 @@ open import Tactic.MonoidSolver using (solve; solve-macro) -qadd : (A : Group c c ) (N : NormalSubGroup A ) → (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x -qadd A N f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where - open Group A - open aN - open NormalSubGroup N - open IsGroupHomomorphism normal - q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x - q00 = begin - ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩ - x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) )) ⟩ - x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl A) (aN=x (g x) ) ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A) ⟩ - (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A) ⟩ - ε ∙ x ≈⟨ solve monoid ⟩ - x ∎ where - open EqReasoning (Algebra.Group.setoid A) _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c _/_ A N = record { Carrier = (x : Group.Carrier A ) → aN N x ; _≈_ = _=n=_ - ; _∙_ = qadd A N - ; ε = λ x → record { a = x ; n = ε ; x=aN = ? } - ; _⁻¹ = λ f x → record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; x=aN = ? } + ; _∙_ = qadd + ; ε = qid + ; _⁻¹ = qinv ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { isEquivalence = record {refl = grefl A ; trans = ? ; sym = ? } - ; ∙-cong = ? } + ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} } ; assoc = ? } ; identity = idL , (λ q → ? ) } ; inverse = ( (λ x → ? ) , (λ x → ? )) @@ -109,53 +91,93 @@ open aN open NormalSubGroup N open IsGroupHomomorphism normal + open EqReasoning (Algebra.Group.setoid A) _=n=_ : (f g : (x : Group.Carrier A ) → aN N x ) → Set c f =n= g = {x : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ + qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x + qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where + q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x + q00 = begin + ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩ + x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩ + x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) )) ⟩ + x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩ + x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl A) (aN=x (g x) ) ⟩ + x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A) ⟩ + (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A) ⟩ + ε ∙ x ≈⟨ solve monoid ⟩ + x ∎ qid : ( x : Carrier ) → aN N x - qid x = record { a = x ; n = ε ; x=aN = ? } - idL : (f : (x : Carrier )→ aN N x) → (qadd A N qid f ) =n= f + qid x = record { a = x ; n = ε ; aN=x = qid1 } where + qid1 : x ∙ ⟦ ε ⟧ ≈ x + qid1 = begin + x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩ + x ∙ ε ≈⟨ solve monoid ⟩ + x ∎ + qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x + qinv f x = record { a = x ∙ ⟦ n (f x) ⟧ ⁻¹ ; n = n (f x) ; aN=x = qinv1 } where + qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x + qinv1 = begin + x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + x ∙ ⟦ (n (f x)) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + x ∙ ⟦ ((n (f x)) ⁻¹ ) ∙ n (f x) ⟧ ≈⟨ ? ⟩ + x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩ + x ∙ ε ≈⟨ solve monoid ⟩ + x ∎ + 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 + qcong {x} {y} {u} {v} x=y u=v {w} = begin + ⟦ n (x w) ∙ n (u w) ⟧ ≈⟨ homo _ _ ⟩ + ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧ ≈⟨ ∙-cong x=y u=v ⟩ + ⟦ n (y w) ⟧ ∙ ⟦ n (v w) ⟧ ≈⟨ gsym A ( homo _ _) ⟩ + ⟦ n (y w) ∙ n (v w) ⟧ ∎ + idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f idL f = ? - -- K ⊂ ker(f) K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where open Group H open NormalSubGroup K -φ : (G : Group c c) (K : NormalSubGroup G) → Group.Carrier G → Group.Carrier (G / K ) -φ G K g x = record { a = x ; n = ε ; aN=x = ? } where - open Group G - open NormalSubGroup K - -φ-homo : (G : Group c c) (K : NormalSubGroup G) → IsGroupHomomorphism (GR G) (GR (G / K)) (φ G K) -φ-homo = ? - open import Function.Surjection open import Function.Equality -φe : (G : Group c c) (K : NormalSubGroup G) → (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) -φe G K = record { _⟨$⟩_ = φ G K ; cong = φ-cong } where - open Group G - open aN - open NormalSubGroup K - open IsGroupHomomorphism normal - φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ G K f x ) ⟧ ≈ ⟦ n (φ G K g x ) ⟧ - φ-cong = ? +module _ (G : Group c c) (K : NormalSubGroup G) where + open Group G + open aN + open NormalSubGroup K + open IsGroupHomomorphism normal + open EqReasoning (Algebra.Group.setoid G) + + φ : Group.Carrier G → Group.Carrier (G / K ) + φ g x = record { a = g ; n = g ⁻¹ ∙ x ; aN=x = ? } where + gk00 : g ∙ ⟦ ? ⟧ ≈ x + gk00 = ? + + φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ + φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = + record { cong = ? } }}} -inv-φ : (G : Group c c) (K : NormalSubGroup G) → Group.Carrier (G / K ) → Group.Carrier G -inv-φ = ? + φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) + φe = record { _⟨$⟩_ = φ ; cong = φ-cong } where + φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ + φ-cong = ? + + inv-φ : Group.Carrier (G / K ) → Group.Carrier G + inv-φ f = ⟦ n (f ε) ⟧ -φ-surjective : (G : Group c c) (K : NormalSubGroup G) → Surjective (φe G K ) -φ-surjective G K = record { from = record { _⟨$⟩_ = inv-φ G K ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } where - open Group G - open aN - open NormalSubGroup K - open IsGroupHomomorphism normal - cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ G K f ≈ inv-φ G K g - cong-i = ? - is-inverse : (f : (x : Carrier) → aN K x ) → {y : Carrier} → ⟦ n (φ G K (inv-φ G K f) y) ⟧ ≈ ⟦ n (f y) ⟧ - is-inverse = ? + cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g + cong-i = ? + + is-inverse : (f : (x : Carrier) → aN K x ) → {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧ + is-inverse f {y} = begin + ⟦ n (φ (inv-φ f) y) ⟧ ≈⟨ ? ⟩ + ⟦ n (φ (n (f ε)) y) ⟧ ≈⟨ ? ⟩ + ⟦ ε ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∎ + + φ-surjective : Surjective φe + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } where record FundamentalHomomorphism (G H : Group c c ) (f : Group.Carrier G → Group.Carrier H ) @@ -182,7 +204,7 @@ open Group H h : Group.Carrier (G / K ) → Group.Carrier H h r = f ( aN.n (r (Group.ε G ) )) - h03 : (x y : Group.Carrier (G / K ) ) → h ( qadd G K x y ) ≈ h x ∙ h y + 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 h-homo = record {