記号法で印象が変わる (半)線形射のコンウェイ・ダガー

アフィン線形圏の不動点理論はけっこう難しい。ので扱わない。線形（正確には半線形かな）圏の不動点理論に限定する。線形圏でもけっこう難しい。そもそも不動点の存在を保証するのが難しい。係数半環になんらかの条件が必要だ。ベキ等な連続半環とか、そんなの。→ http://d.hatena.ne.jp/m-hiyama-memo/20061107/1162888657、http://d.hatena.ne.jp/m-hiyama-memo/20061026/1161847087 。

で、fは線形射（線形圏の射）とする。今まで、f:A×X→X と書いてきたが、パラメータ（制御変数）の空間はAじゃなくてTとするかな。f:T×X→X。Tだと時間みたいだ、って懸念もあるけど。

線形圏なので、f:T×X→X は、直和からの射 f:T+X→X と思ってよい。線形圏では直積と直和は一致して双積となるから。fは、a:X→X と b:T→X の余タプル [b, a] と書ける。つまり、f(t, x) = b(t) + a(x) 。線形圏では関数適用と掛け算は同じようなもんだから、一次形式 bt + ax が f(t, x) だと言ってもいい。

fの不動点を考えて、f^†(t) = μx.f(t, x) は Tr(f;Δ)。具体的に書くと、μx.(bt + ax) 。これ以上は絵を描かないと無理だが、次の絵の前半が参考になる。http://d.hatena.ne.jp/m-hiyama-memo/20100701/1277947580 より。

f(t, x) = bt + ax のコンウェイ不動点が (bt);a^* で与えられることが絵からわかる。固定されたtに対する bt = b(t) を改めてbと置けば、b;a^* = a^*b となり、素朴な級数計算の結果と一致する。

コンウェイ圏とは、トレース付きデカルト圏に他ならないが、さらに（半）線形性の条件を付けて線形コンウェイ圏ができる。これはコォゼン／クリーネ圏（Kozen-Kleene）と呼べるもんだろう。