haskell-jp / math #3

ですよね。ありがとうございます。

@maru10t has joined the channel

あれ？素体Z_pからZ_pへの自己同型写像ってidしかない……のか？

f(1)=1 かつ f(1+1)=f(1)+f(1) を満たそうとするとidにしかならない気がする

この質問が関連ありそうですね https://math.stackexchange.com/questions/665275/is-an-automorphism-on-the-prime-field-the-identity-map

@ has joined the channel

LをK上の有限拡大としたときに “|Aut(L/K)| ≤ [L : K] and equality holds if and only if L is Galois.” だったと思うので、 |Aut(Z_p / Z_p)| ≤ [Z_p : Z_p] = 1 になりそうな気がする。

体の準同型写像の定義:
f : X→Y
f(0_X)=0_Y
f(1_X)=1_Y
f(a+b)=f(a)+f(b)
f(a・b)=f(a)・f(b)
がほぼ線型写像の性質そのもので、素体は線型ベクトル空間としての基底が1つしかないのでfの行列表現がA=(1)しかなくなるという風に理解しています

@駒鳥(hxf_vogel) has joined the channel

@hsjoihs has joined the channel

じょんどろさんの「詳説word2vec」、lotzさんの「作って学ぶBitcoin」、すごくよくて有り難いです！
Haskell communityからの情報はimpressiveですねー:star:

@siosio has joined the channel

Frobenius Automorphism http://mathonline.wikidot.com/the-frobenius-automorphism-for-a-finite-field という便利な道具があるのを今更知った件

@ has joined the channel

ほぼポエムなんですけどHask categoryについての記事を書いてみました
https://myuon.github.io/posts/versus-hask-category/

Hask is not a category
↑これすき

@n4to4 has joined the channel

@thimura has joined the channel

@kakkun61 has joined the channel

@tsubaki has joined the channel

@ has joined the channel

@yokomotod has joined the channel

@tanimocchi has joined the channel

@ohnabe has joined the channel

@genkami has joined the channel

@kazu has joined the channel

@ has joined the channel

@nobkz has joined the channel

@rei has joined the channel

@MonogusaBose has joined the channel

圏論の圏の定義で、射の合成に関してはきちんと定義を要請しますが、射の=については、結合律、単位律を満たすように定義するべきですよね？

= は何を表す記号ですか? 射の等しさ?

その、圏の定義をを見てたら、=が出てきたので、なんなんだこいつみたいな感じが。

射の等しさなんでしょうけど。

例えば射 f : a -> b について f・id_a = f といったりするときの = ですよね。「この両辺を等しくするよう射の合成・恒等射を考える」の代わりに「この両辺を等しくみなすよう射の等しさを考える」と思うような…? あまり深く考えたことなかったです…

CoqだとSetoid(Haskellで言うEq)を使ってその辺処理したりするっぽい https://qiita.com/mathink/items/2067c162fb7cf8f6c83f#setoid-%E3%82%92%E3%83%99%E3%83%BC%E3%82%B9%E3%81%AB%E3%81%97%E3%81%A6%E3%81%84%E3%82%8B%E7%90%86%E7%94%B1

反射律、推移律、対称律は普通前提になってますけど、これらがない場合に何を失うのかはよく分からないです

上にもあるとおり圏を与える時についでに同値関係=を与えてしまう方法と、ロジックに元々組み込みの=を使う方法があると思います。
Setoidでやる場合はid, compositionがSetoidの=を保つみたいな条件がいるので数学では組み込みの=を使い、必要があれば拡張したりするという立場を取るのが普通な気がします

(いずれにせよ同値関係になるようにはするので反射律とか諸々は満たします)

なるほど。ありがとうございます。

ついでなんですが、圏C において、射f,gがあり、f=gのとき、dom(f) = dom(g), cod(f) = cod(g)って成り立ちますかね?

代入原理から成り立ちます

通常，=は同値律 + 代入原理を満たす関係として導入するのが一般的ですね

ありがとうございます!

* 代入原理
* みょんさんの「id, compositionがSetoidの=を保つみたいな条件」
* 「Coqと圏論」のページの `Proper`
この3つは同じ物を指している、と考えていいのかな

みょんさんのはちょっと分からないですが，CoqのProperに関しては代入原理と同じだと思います(あまり詳しくないので断言はできませんが)．要はrewriteがsubstitutionにあたるので．まあ，Coqの場合Properを明示しなければいけないので，一般に暗黙的な代入原理を認めてるわけではないと思いますが

@as_capabl 1つめ≠2つめ=3つめです Properは単にproper conditionを満たせばrewriteルールが使えるようになるってだけです
「普通の」数学は=とはrefl+substをみたす組み込みのrelationと考えるし、これだけあれば圏論するには十分ですが、Coqでは(というか構成的数学の立場では)implicitな=を扱うのが苦手で「同一視」が欲しくなる時に不便なのでじゃあMorを与える時に一緒に同値関係も与えればいいやんけ！という考え方が上のリンクのやつですね(ただしSetoidの場合は与えられた同値関係がcompositionとcompatibleとかそういう条件がないと上手く機能しないっていうのが上の説明, これはsubstがあるなら自動的に成り立つので組み込みの立場だと不要)

という感じの説明でどうでしょうか(自分でもわかりやすいとは思ってない)

こんなことちゃんと考える分野があるんですね…なるほど，知りませんでした
http://staff.math.su.se/palmgren/czf_and_setoids_final_lmcs.pdf

技術的にはSetoid-enriched category theoryだと思えばいいので難しくはないんですが、何を言語として使うか(ZFCで扱える範囲に限定するか、それとも圏論自体を言語として捉えるか)みたいなのを反映しようとするとこういうのも真面目に考えないといけないというアレですね

Setoidでやろうとすると、何か新しい物を導入するたびにProperを証明しないと駄目になる感じで面倒だったので、組み込みの=を活かす方向性で次はやってみたいですね

@ has joined the channel