凖同型定理の続き

定理の形はあれで良かったらしいんですが、

　　なんどやっても、証明が refl 。つまり自明

さっぱりわからない。

商群 G / N の要素ってのは、aN のこと。つまり、正規部分群の要素を a 倍したもの。

正規部分群 N の群以外の条件は、

aN ≈ Na

つまり、Nに入ってる要素は可換。

凖同型定理は、凖同型写像 f : G → H , 自然な対応

ψ : G → G / N
ψ a = Na

に対して、f のkernel条件 fN ≈ ε　があれば、

　　f a ≈ h (ψ a )

となる凖同型写像 h があるってだけですが、h は f で良くて

f a ≈ h (ψ a) ≈ f (ψ a) ≈ f (aN) ≈ f (Na) ≈ f(N) f(a) ≈ ε f(a) ≈ f a

と一発ででる。

ところが、Na ってのは、実はデータ構造で、a から Nの要素を使ってGの要素を生成するもの。

そのデータ構造 ψ a からは a が取れるようにできる。具体的には record に filed をたせば良い。

なので、 h は Na から a を取り出せるので、 refl になってしまう。

と、こういうことらしい。なんか、証明するところがないんですけど。どういうことなの?

Top Gun -- Merveric

聞いていたより、エースコンバットでした。

　　パルコには米兵さんたちがいっぱい

楽しかったみたいだな。

61番はとうとう一日2便に。IMAXは12時の次が17時。帰りは安謝橋経由。まぁ、110の終バスで。

どんどんバスは不便になるな。

まぁ、でも、IMAXで映画館に通う価値のある映画ではあったかな。

凖同型定理

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

なんとなく、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 になるので、なんか間違えているらしい。でも、寄り道なのであんまりが頑張らない予定です。

雨男雨女

僕もたいがいなんだが、お弁当をたのんだ紗鼓さんも

　　たいがいな雨女

でな〜　なので、OS研究会が二日間土砂降りだったもさもありなんてきな。

きょうもなんか、紗鼓さんはイベントやってるみたいで、ざざ降りです。

とはいえ、気温も低いし、ここまで雨が降る梅雨は沖縄では珍しい。

OS研究会最終日

まぁ、いろいろあったけど、終わったということで。

割とハズレな質問にコメントしたら「最後にうまくまとめましたね」とか言われた今日この頃。

OS研究会初日

久しぶりの沖縄での開催。ハイブリッドです。古島のIT創造館。

いつもの玉石混合ですが、IIJの人の Kernel の処理を User 空間でやると速くなるってのが
面白かったな。Unix domain socket とかが速くなるらしい。

オンラインでもやってるので明日も参加可能。

明日は紗鼓さんのお弁当が登場するので楽しみ。

時間割

なぜか学期の最初に「Webに時間割を載っける」という作業が。たぶん、赴任してから、ずーっとやってる気がする。

　　1) シラバスには教室が載ってない
　　2) 時間割は、くそPDFのみで、Webには一覧はなし

で、まぁ、事務は特に疑問に思ってないらしい。で書き写すはめになってます。事務に言っても無駄でしょ。

もっとも、もう教室はそれほど重要でもないかも。ほとんどオンラインだから。

自分を含めてシス管の学生やら先生やらが、半期ごとに適当に作ってます。

　　自分勝手なスクリプトで

ひどい。シラバスを script でアクセスするわけなんだが、なんで教室が載ってないのかなぁ。

一昨年くらいは PDF の解読になんか使ったらしいんだが「敗れさった」らしい。いやさ、

　　Preview.app で表示して、vim にコピペするのが良い

らしいです。PDFは Adobeのくそフォーマットなので、一度、rendering しないとどうしようもない感じ。

元の Excel よこせとも思うんですけど、もらったことない。

今年は技官の人がやってくれたんですが、シラバスへのリンクが変、それは教務Webにredirectですませたんですが、

　　古いのが文字化け

え、そこで旧悪が露見するの? あぁ、

　　Meta-tag がないのか

macOSを英語モードで使ってると、Meta-tag ないと文字化けする。でも、そんなことするのは

　　自分だけ

かも知れないです。なおす時に間違えてファイル消したが、例のバックアップとれてない問題が...

いや、だいじょうふ。教務Webから取ってこれるから。いや、リンクでもいいんだけど。

でも、なんか、教務WebのURL変わってるみたいんだけど。やっぱりファイルとってきた方が良くない?

いや、昔のはいいか? あぁ、いや、まぁ...

　　気が向いた時になおすかも知れないです

これで10万Mu

なんか、5万muでポイントみたいな ingress event が始まるらしく。

いや、まぁ、無理でしょ。そんなに頑張らない予定〜

最近、緑が元気だしな。

PS3 関係

なんか、Playstation/sony 関連のID統合みたいなことをやったらしく、いろいろ不都合が...

　BDレコーダのアプリの id が .jp じゃなくて .jo になってる

どこでそうなった? いつから? 去年は使っていた気がするんだが。

Startrek Picard Season 2 を PS3 で見ようとしたら、

　PSNが機器パスワードを生成して入力しろ

と言ってくる。ずいぶん態度でかいな。ワンタイムパスワードのつもりなんだろうけど、

　スマホの画面を見て入れる方式

の割に

　大文字小文字混じってそこそこ長い

それなら authenricator 使うとか、Google みたいに数字二桁とかでいいんだが。

アマプラのUIは相変わらずひどいし。え、吹き替えか字幕かの選択で別ソフト? くそだな。

PS3 にキーボードさしてパスワード入れたが

　アマプラの検索時にはキーボードは使えない

まぁ、PS3で見れるだけで偉いといえばそうなんだが。最後に、

　キーボード抜いたら PS3 の kernal freeze くらいました

わかったわかった。こういうの得意なの知ってるでしょ。

agda-vim python3 on neovim 動きました

neovim で .vimrc を外したらなんか動きました。偉いじゃん。なんか、

　　Y が効かないんですけど

いろいろだめ

　　最初の reload に真っ白な画面が10秒
　　default の色付けがピンクベース
　　Unicodeの入力が emacs のと異なる(致命的じゃん...)
　　,n での eval で bad index みたいなエラーがでる

ひどい。まぁ、でも、Emacs/viper は、それはそれで問題なので。こっちは、がんばればなおせそう。

色付けは結局 zellner base で少し変更して逃げました。

Agda の方も、無限ループ避けはだいたいわかったので、まぁ、なんとかなるんじゃないかな。

base はこれです。

　　pip3 install pynvim

が必要。

https://github.com/tc-0/agda-vim.git

呪術廻戦0

まだ、上映中。どうしようか迷ってたんですが、土日は18:10からなので。いつものライカム。

高速バスのバス停からの歩きがつらい。バリアフリーなにそれ的な。でも雨には降られなった。

割とお客さん入ってて。子供と女性ですけどね。リピーター多いのか。

ウルトラマンよりは面白かった気もする。なにせ、

　　五条先生がひどい

まぁ、もう人間じゃないと思うんだよな。なので、明らかに

　　面白い方を選択してる

それなりの必然性はあるけど... 選択される方はなぁ... 自分も少し思い当たることがあるけど...

鬼滅の映画よりは男性うけあるかも。男の純愛の話だから。シンジ君強すぎ。

でも、全体的には「全部。五条悟が仕組んだ」でしょ。呪術廻戦そのものがそういう感じでな。

　　五条悟がラスボス

な話なんじゃないか説。

というわけで、そこそこ楽しかったです。

https://jujutsukaisen-movie.jp

カードと暗証番号

住銀ですけどね。まだ、トラブってます。送られたカードはだめだった。

　　もう一回、失敗した郵送作業を繰り返せと言ってくる

嫌だとはいったんだが、どうも「向うでプロトコルがそれしかない」ぽい。

わかったわかった。やりゃいいんでしょ。プロトコルがあるだけまし。

この手のバグを踏むのは大得意。相手が悪かったな。

virsh の続き

iso image は attach できたので、空の qcow2 を作って...

　　ie-virsh start kono-03
　　ie-virsh console kono-03

で、UEFI Shell に。順調。その先がな。

VNC が全然つながらない。去年もやったんだけど、spice がどうとか言ってる。要するに、

　　macOSの画面共有ではつながらない

ってだけらしい。パスワードまではくるので割と残念。いろいろ悩んだんですが、

　　brew install vnc-viewer

で Real VNC が入るので、それで良いらしい。そうですか。よし、じゃぁ、また Rust と格闘な。

この後、Fedroa OSのkernel を ansible で debug build するってのが待ってるみたいです。

Hugo の続き

NetlifyCMS に接続はできたんですが、そこから先。背景変えたり、投稿ボタンどうやって付けるの?

　　contents/_index.md

が top page でいきなり書き換えるんですか。この辺は、theme によるのか。/admin の URL を書くだけなのね。

gitlab ci に接続するんだけど、

　　ci が git submodule を load するのを拒否

あぁ、security 的な問題かもな。めんどくさいので、submodule をメインに追加。

gitlab から web server に上げるのはいろいろ問題が... rsync するの? まぁ、いいか。

と思ったら、rsync -av public hogeって、 hoge/public を作ってくれないのか。

いいや、と思って rm -rf * ; git checkout -f したら、

　　設定した admin が消えた

くそ〜 git add してなかったのか。まぁ、適当に復旧したら動いたようです。

で、え、なに

　　また、freeradious とらぶってるの?

あんまり、用務員こきつかうなよ。

Agdaの無限ループ

まぁ、確かに、{-# TERMINATING #-} とかで、Agda自体が止まるかどうかは判断できてないんですけどね。

割と簡単なコードなのに無限ループしてしまう。で、部分部分で出力を調べていくんですが...

　　ばっちり合ってる

で、関数を分解してみたら

　　あーら不思議ばっちり動く

ってことは、これは Agda のbugかぁ。まぁ、

　　定理証明系なので実際に eval ことは滅多にない

わけなんですけどね... この手の bug を踏むのは大得意です。

GODIVA

ライカムにウルトラマン観に行ったので(佳作程度なのでコメントなし)

　　GODIVAによったらいつもの四角いののばら売りがない

ので、少し粘ったら実はあるということが判明。

　　隠しメニューですか?! 在庫はこれだけ?

と聞いたら、そんなことはないです。在庫はあります。店頭にないだけだそうです。
(嘘つき)

まぁ、ベルギー人のおばちゃんによると、

　　GODIVAよりおいしいチョコレートはたくさんある

って話ですけどね。

コーヒーやチョコレートにも政治的正しさ関連の話はあるのだが、そのうち取り上げられるのか。

Selected Readings

中原道喜先生の手製参考書ですね。高2のときだな。英標/文標もやったので、まぁ、そっちでもいいかなと思うんですが。

　　タイプライタなのが味がある

引用されてるのが割と格調高い。そのまま書き込みがある。そこそこ面白いんですが、

　　授業自体は「順に当てて和訳していくだけ」

で、だいたいさぼっていた気がする。まぁ、高校時代、あんまり

　　英語の勉強に commit してなかった

のは残念だった。勉強しなおしてわかったのは、

　　そもそも語彙がないとだめ。しけ単で良い
　　発音とかスペルはパターンなので限定的
　　絶対的に読む量が必要
　　たくさん読んでれば文法は重要じゃない

ってことね。それをやってれば大学入試は楽だったはず。しかも、

　　大学入試でそこそこの英語の偏差値取っても
　　実際の文献や論文を読むのには全然足りない

わけでさ。おかげで学部1,2年でかなり英語を学ぶモチベにはなったんですけど。

崩壊したかばんの修理

いや、まぁ、長く使ったぼろいのが良いわけで... チャックのところ壊れてたのを

　　なんとかしようと思っただけで放置

してたのがだめで、崩壊。で、Speedy Stecher なるものを奥様が持っていたので...

　　説明書だけではやりかたがさっぱりわからず

こんな風になるらしい

　　--∩-∩-∩-∩-∩-∩-∩-∩-∩-∩-∩-
　　 ∪ ∪ ∪ ∪ ∪ ∪ ∪ ∪ ∪ ∪

いや、ぜんぜんわかんないと思うんですけどね。

とりあえず、差して、裏の一本糸の方に引っ掛けて抜く。それを繰り返すだけ。

　　修理完了〜
　　

KVM, UEFI and Rust

いろいろあった昨日の続き。OSの課題は、KVM / virsh でやってもらうんですが...

　　virsh の権限の制御が大雑把すぎる

問題があって、結局、virsh のwrapper を書いたんですが、シス管の一人が

　　Rust で書き直す

という技を。「え、それ誰がメンテするの」ってことなんですが、

　　KVMで UEFI で起動するには、vvram の項目をKVMのVM定義xmlに追加する必要がある

ってことなので、泣きながら書き直す羽目に。こんな感じ。

　　let elem = String::from_utf8_lossy(e.escaped()).replace("ie-virsh-template",&self.vm_name) ;
　　writer.write_event(Event::Text(BytesText::from_plain_str(&*elem))).unwrap();

いや、単に xml の一部の文字列を置き換えてるだけですけどね。
とりあえず、&str と &[u8] と String を ad-hoc に変換しながら書く必要があるのはわかりました。

quick-xml がそういう書き方らしい。いや、Rust ってのはそんなもん。OptionとResultをnestさせたり。
僕の Rust の評価はそんなわけでかなり低いです。

　　XMLのparseとか無駄なことするな
　　単純な文字列置換でやれ

とは思いました。汎用じゃないんだから。

まぁ、一応、動いたっぽい。KVMは image を共有すると

　error: internal error: child reported (status=125): Requested operation is not valid:
　Setting different DAC user or group on /mnt/ie-virsh/teacher/kono/kono-02.qcow2 which is already in use

と文句をいうらしい。ついでに、

　OSの課題用の Fedora OSの install を ie-virsh でできるようにする

ってのをやりたいんだが、少し工夫(cdromの接続とBoot順)がいるので、しばらく放置か?

なんか、いろいろあったが...

3/11に、Fortigateの設定を変えたら、Sakura側から、こっちにsshで入れなくなってて、

　　バックアップが取れてなった

あらら。なので逆方向から取るようにしたらしいんですが、.ssh/config の permission miss で動いてなかった。

あと、もう一つ、rsnapshot があるらしいが、

　　それを逆方向にするのはやりたくないです....

教訓。

　　バックアップはちゃんと取れているかどうか確認しよう

NetlifyCMS

static な web page 生成は hugo でやるわけですが、Netlify CMSは、

　　gitlab での *.md の生成を web 上で会話的にやることで blog的なものを作る

わけですね。Head less とかいうんだが、gitlab 使うから、DBがないわけ。

　　gitlab は DB としてくそだろ

という意見には賛成するしかないわけですが。なんが、設定が全然できず。

　　要するに、private gitlab とか想定されてなくって、github とかそんなのばっかり

でも、だいたいわかった。どうも、NetlifyCMS のサイト自体は、どうでも良い感じ。

自分のサイトで回す分には Oauth もいらないのかも。

　Hugo を動くようにする
　Hugoを gitlab に結び付ける

つまり、git init / git clone すればよい。そこに

　admin という directory を掘って
　以下の config.yml と index.html を置く
　gitlab の admin から application を選択
　新しくapplication を作る
　scope は api にする
　gitlab　で必要な permission を許可する

Application id を config.yml に。

　redirect URIを admin の index.html

に向ける。で動くようです。

なるほど。このあたり、生成系を容易、あるいは、gitのtemplateをつくるとよいかもな。

誰かが設定した時の記録がまったくなくて... 結構、てさぐりだった。前に自分でやったような記憶もあるが、

　　気のせい

だったみたいです。

admin/config.yml
　　backend:
　　 name: gitlab
　　 repo: ie-web/programming3
　　 auth_type: pkce
　　 app_id: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
　　 api_root: https://gitlab.xx.u-ryukyu.ac.jp/api/v4
　　 base_url: https://gitlab.xx.u-ryukyu.ac.jp
　　 auth_endpoint: oauth/authorize
　　 site_domain: https://xx.u-ryukyu.ac.jp

admin/index.html
　　<!doctype html>
　　<html>
　　<head>
　　　<meta charset="utf-8" />
　　　<meta name="viewport" content="width=device-width, initial-scale=1.0" />
　　　<title>Content Manager</title>
　　</head>
　　<body>
　　　<!-- Include the script that builds the page and powers Netlify CMS -->
　　　<script src="https://unpkg.com/netlify-cms@^2.0.0/dist/netlify-cms.js"></script>
　　</body>
　　</html>

本を捨てる

なんか学生が 「がらくた置き場、どこですか」とかいうので、ゴミな本が多い書棚を整理。いや

　　捨てるだけ

2008年のC++とかJavaの入門書とか全部捨て。ダンボール箱三つだからたいしたことない。当然。つうか、

　　プログラミング言語の入門書を買うの止めろ

教科書に指定するのも禁止な。まだ、

　　アルゴリズムとか、MITのPythonの教程

だったらギリギリ。

　　例題の動かない入門書とかゴミだろ

いや、動かないで見るだけなら向いてないから、この分野、向いてないから諦めろってなとこです。

プログラミング言語の入門なら、Webのサイトに Tutorial載ってるだろ、そのまま英語でやれってことだね。

原神の現状

螺旋はLv8までは星全部取りましたくらいです。

将軍と神里で十分楽しい。霧切は出たんですが、育てきれてない。なので、

　　ゴミ拾いモードに(鉱石拾いとか雑魚武器拾いとか)

version の端境期なので、まぁ、そんなもんかも。Shenhe が育ってないのは

　　アビザルボスを最近まで倒せてなかった

からです。いや、Lv上げたら倒せなくなってて、少し困ってた。でも、今は先生とメイドでなんとか。

甘雨はアモス持ちなのだが戦力になっているかというと微妙。でも、ギミックには便利。狙うと強いの?

まぁ、あんまりやることなくなってる気もするが、螺旋とか残りのレベル上げとか。香菱とかモナ?

行秋は完凸なんですが、いまいち、強さがわかってないです。おそらくは聖遺物の問題だろうな。

ディルク、メイド、バーバラ、主人公(女/風)でなんでも頑張っていた頃が懐かしい気もする。

シロート質問

いや、さぁ

　　クロート同士の質問って、つまんないもん

なんですよ。ずば抜けた発表なら白熱したりするけど、

　　まぁ、だいたいは、既にわかってることを確認するくらい

なので、面白い質問をする時には

　　この分野、シロートなんですが..

ということに。まぁ、自分はそんなのとは関係なく

　　IBTってなんですか

とか聞くわけですけどね。

昨日のが、まだわからん。

Stack が循環Listになっていて、表示時に無限ループしてるってのはわかったんですが...

Binary Tree

いや、いつもの Model 検査を Agda で書いてるんですが、

　　Binary Tree が無限ループする

まぁ、それ自体はよくあるバグなんですが、

　　それって正しいのを証明したやつじゃなかった?

ん〜 まぁ、それもありがちなんだが。そもそも、

　　Haskell / Agda って bug った時の debug 方法があんまりない

コードを分解して実行するくらい。trace とかあるらしいんだけど...

で、test code を動かしてたら、

　　なんか -- wrong とか書いてある。は?

う、そういえば、

　　元のコードに bug を入れておく方が面白い

と思ってそのままにしたのだった。証明入れたコードとは別なのかよ。いや、

　　自分で書いたんですけどね

で、どうするの。なおすか、証明付きの方を使うか... それも面白いといえば面白いか。

LuaLatex の style file どこ〜

いや、UTF8の対応とか、SVGのincludeとかいろいろ不都合が...

でも、最近は、

　　情報系でも LaTeX で論文書かない

らしいし〜

LuaLaTeXの人、あんまり、互換性、気にしないらしくって...

Bleach 復習終わり

あと、劇場版4つあるみたい。

なんと、書籍の方も「大人買い」した人が。そこまで?! って気もしますけどね。しかし、

　　黒崎一護、なんか死神の力を失ってるんだよ!

本編の話ばかりではないから、いろいろ、よろしくない話もあったけど。JUMPだからな。

アニメオリジナルのは割とひどい話が多くて。

　　一体、何人の死神が封印されてるんですか?!

しかも、わりとろくでもない理由で恨みかって反乱されてるし。まぁ、そういう組織なんだろうな。

組織なんてそういうものか。で、千年血戦篇ですか。漫画先に良むか?!

　　2.1 死神代行篇
　　2.2 尸魂界篇
　　2.2.1 尸魂界潜入篇
　　2.2.2 尸魂界救出篇

　　2.1 バウント篇
　　2.2 バウント 尸魂界・強襲篇
　　2.3 日番谷先遣隊奮闘記
　　2.4 メノスの森篇
　　2.5 新隊長天貝繍助篇

　　2.3 破面篇
　　2.3.1 破面出現篇
　　2.3.2 虚圏突入篇
　　2.3.3 過去篇
　　2.3.4 空座決戦篇

　　2.6 斬魄刀異聞篇
　　2.7 扉絵シリーズ
　　2.8 護廷十三隊侵軍篇

　　2.4 死神代行消失篇

IC規格表

まぁ、その頃だけって感じですね。7セグのカウンタからだったかな。

79年から82年くらいが、一番ハンダ付けしてたかも。痔で寝込んだりしてた。

97年は「アナログやりたい」という気分だったのはわかるけど、それだけだったらしい。ボロ度がない。

ラブ麺復活

なんか綺麗になってました。しかし、

　　レモン麺はなくなってました

まぁ、あっさり系のラーメンはなくなる運命なんだよ。

わた琉は、COVIDで「カウンターだけ、かつ、後ろをテーブルでふさぐ」みたいになって敬遠ぎみ。

　　すべては、COVIDが悪い

ってな感じですね。

ごーるでんうぃーく

サンエーでは東京にいってるOBが。

そして、はちれんでは、

　　妙に綺麗な女の人たちが...

わざわざ、こんな時にとか思ってしまう方ですけどね。