正規部分群、部分圏

最初に随伴関手定理をやった時に

　　いきなり部分圏が出てくる

ので結構困って。だってマクレーンもそうなんだけど集合論抜きでやってるわけでしょ? なので、

　　圏Aで、Functor A A があれば、その像は部分圏になる

ってのを使ってた。Obj A と、その条件 P : Obj A → Set から作るべきなんだと今ではわかるが。

正規部分群でも自己凖同型があってとかやってたんだが、部分群よりも強い条件なんだよな。なので

　　凖同型定理が自明になってしまう

らしい。で、

　　正規部分群から、自己凖同型を作る
　　部分圏から、自己関手を作る

ってのを考えてたんだけど、非構成的ならありそうな気がする。逆に選択公理が偽ならなくても良い。

実区間の圏や群から開区間の部分圏や部分群を作るとか考えてました。

まぁ、気が向いたら書き直すかも。でも、凖同型や関手があるってのでもわかりやすくて良いかも。