日々の流転

λ. 始代数の持ち上げ

関手 F: C→D, G: D→C と、FG: D→D の始代数 (μFG, in_FG: FG(μFG)→μFG) があったとする。このとき、(G(μFG), G(in_FG): GFG(μFG)→G(μFG)) は GF: C→C の始代数になっている。任意のGF代数 (X, φ: GFX→X) への射 fold_GF(φ) は φ . G(fold_FG(Fφ)) で定義する。

準同型になっていることの確認:

fold_GF(φ) . G(in_FG)
= φ . G(fold_FG(Fφ)) . G(in_FG)
= φ . G(fold_FG(Fφ) . in_FG)
= φ . G(Fφ . FG(fold_FG(Fφ)))
= φ . GF(φ . G(fold_FG(Fφ)))
= φ . GF(fold_GF(φ))

一意性の確認:

f . G(in_FG) = φ . GFf
⇒
f = φ . GFf . G(in_FG^-1)
  = φ . G(Ff . in_FG^-1)
  = φ . G(Ff . fold_FG(FG(in_FG)))
  = {- Ff . FG(in_FG) = Fφ . FG(Ff) より cata-fusion -}
    φ . G(fold_FG(Fφ))
  = fold_GF(φ)

cata-fusionの部分の図式:

応用?

これを使うとCPOと始代数等で書いた話の、「f:X→Y によらず Ff: FX→FY が正格であるとき、C_⊥でのF始代数は、CでのF始代数にもなっている」という部分を示すことが出来る。Ffはfによらず正格なので、Fは F: C→C_⊥ と見なせる。でもって、Uを忘却関手 C_⊥→C とすると、FU: C_⊥→C_⊥ の始代数 (μFU, in_FU) に対して、(U(μFU), U(in_FU)) は UF: C→C の始代数になっている。

これを示すには lifting L: C→C_⊥ と忘却関手 U: C_⊥→C の随伴が関わってくるのではないかと思ってたけど、全然関係なくて意外だった。むー。

一般化?

終余代数についても同様のことは当然言える。

何かうまい一般化はないか?

λ. 『NHKにようこそ!』 滝本 竜彦

を読んだ。