CLTT 補題 2.6.5 (Lambek)

昨日の読書会で未消化だったので復習.

補題 2.6.5 (Lambek)
T-始代数 φ: TY → Y は iso.

下の図で考える.

      Tf          Tφ
TY────→TTY────→TY
｜          ｜           ｜
｜φ        ｜Tφ        ｜φ
｜          ｜           ｜
↓          ↓           ↓
 Y────→TY ────→ Y
       f           φ

左の四角は φ が始代数だから f が唯一つ存在することで保証される.
右の四角が代数の射であることは直接確かめれば明らか.
全体の四角も代数の射であることは明らか. さらに始代数から始代数への射だから, 唯一つ存在し, それは id でなければならない. 従って

f ; φ = id

である.
左の四角の可換性より,

φ ; f = (Tf) ; (Tφ) = T(f ; φ) = T(id) = id,
φ ; f = id

となる。
よって T-始代数 φ: TY → Y は iso.

図を普通に書ければわかりやすい。