準同型定理もう一度

チコノフの方もだいぶできたんが、少し距離あるので、何かほかのを見直してたら、

　　 g ⁻¹ ∙ f ⁻¹　∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )　　　　 ≈⟨ solve monoid ⟩
　　 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))

とか並べなおしてくれる機能が。これは便利。いちいち、assoc とかするのかなりつらくて。

でも可換とか逆元とかはやってくれないです。Ring solver もあるけど、その程度。

で、集合結構やったので、商群も集合だよなと思って書き直したら、割とうまくいった。

⟦ n ⟧ で、準同型写像を表すのが Agda 流らしい。

　　record an {A : Group c c }　(N : NormalSubGroup A ) (n x : Group.Carrier A　) : Set c where
　　　　field
　　　　　　a : Carrier
　　　　　　aN=x :　a ∙ ⟦ n ⟧ ≈ x
　　
　　record aN {A : Group c c }　(N : NormalSubGroup A )　: Set c where
　　　　　　n : Carrier
　　　　　　is-an : (x : Carrier) → an N n x

と二重にすると良いらしい。なのだが、相変わらず、準同型定理自体は refl に。なんで。

どうも商群の要素の比較を、

　　 λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧

でやってるのがいけないらしい。集合として同じってことなら、少しずれがでる。でも、結局、同じだけどな。

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
　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 ( φ 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 )