凖同型定理

まぁ、あの、剰余群とかで考えるとわかりやすいあれですね。四則演算が剰余と平行してるのは不思議だったが...

なんとなく、mod で考えると「全体の模型になっている」ってのを表している定理らしいです。

　　K⊆ker : (G H : Group c l)　(K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c　Level.⊔　l )
　　K⊆ker G H K f = (k : CosetCarrier G K ) → f (CosetCarrier.r k ) ≈ ε　 where
　　　open Group H

　　record FundamentalHomomorphism (G H : Group c l)
　　　　(f : Group.Carrier G → Group.Carrier H )
　　　　(homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f )
　　　　(K : NormalSubGroup G ) (kf : K⊆ker G H K f) :　Set ( c　Level.⊔　l ) where
　　　open Group H
　　　field
　　　　h : CosetCarrier G K → Group.Carrier H
　　　　h-homo :　IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h
　　　　unique : (x : Group.Carrier G)　→　f x ≈ h ( φ x )

ってな感じですが、なんか変〜

G / K が商群つまり剰余群なんだが、こいつが Agda ではめんどうでな〜

でも、圏論だと、普遍問題の解という形で綺麗に書けるらしい。

なんか、unique が refl になるので、なんか間違えているらしい。でも、寄り道なのであんまりが頑張らない予定です。