Adjunction から Universal mapping を導く
Menu MenuUniversal Mapping と Adjunction の対応
Universal Mapping は Adjunction と一対一の対応があります。まず、Adjunction から Universal Mapping を導きます。 universal-mapping.agdaAdjoint には二つのFunctor U, Fと二つの自然変換η,εがあるので、道具立てが豊富なので、この方向の方が簡単です。
Universal Mapping の U,F,ηは、そのまま Adjoint のU,F,ηが対応します。あとは、解を求めて、唯一性を証明するだけです。
Adjoint の定義は、
open import Category.Cat
record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
( F : Functor A B )
( η : NTrans A A identityFunctor ( U ○ F ) )
( ε : NTrans B B ( F ○ U ) identityFunctor )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
field
adjoint1 : { b : Obj B } →
A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
adjoint2 : {a : Obj A} →
B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ]
こういう感じでした。使える道具はこれだけです。いや、いっぱい飛び道具がある感じです。でも、単にこれを仮定すればよいだけです。
Adjunction A B U F η ε →
と書くだけです。これで、adjoint1, adjoint2 などが使い放題です。
証明するべき Adjunction から Universal mapping の命題は以下のように記述します。前に定義した、UniversalMapping A B U (FObj F) (TMap η) の record を構成すれば勝ちです。
Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
→ (adj : Adjunction A B ) → UniversalMapping A B (Adjunction.U adj)
Adj2UM A B adj = record {
F = FObj (Adjunction.F adj) ;
η = TMap (Adjunction.η adj) ;
_* = solution ;
isUniversalMapping = record {
universalMapping = universalMapping;
uniquness = uniqueness
}
} where
U : Functor B A
U = Adjunction.U adj
F : Functor A B
F = Adjunction.F adj
η : NTrans A A identityFunctor ( U ○ F )
η = Adjunction.η adj
ε : NTrans B B ( F ○ U ) identityFunctor
ε = Adjunction.ε adj
solution : { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) → Hom B (FObj F a ) b
solution {_} {b} f = B [ TMap ε b o FMap F f ]
解は、f* = ε(b) o F(f) です。随伴関手の可換図を書いてみると、このような感じです。
FU(b)
・ |
・ |
F(f) ・ |
・ ε(b)
・ |
・ f* v
F(a) -----------------> b
U(f*)
UF(a) -----------------> Ub
^ ・
| ・
| ・
η(a) ・ f
| ・
| ・ f = U(f*)η
|・
a
ηとεの位置が対称になっているのがわかります。Free Monoid の例では、b から逆向きに f* をF(a)に届くまで f を使って合成しました。
この解が、UniversalMapping の解になっていることは一直線に証明することができます。
universalMapping {a} {b} {f} =
let open ≈-Reasoning (A) in
begin
FMap U ( solution f) o TMap η a
≈⟨⟩
FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a
≈⟨ car (distr U ) ⟩
( (FMap U (TMap ε b)) o (FMap U ( FMap F f )) ) o TMap η a
≈⟨ sym assoc ⟩
(FMap U (TMap ε b)) o ((FMap U ( FMap F f )) o TMap η a )
≈⟨ cdr (nat η) ⟩
(FMap U (TMap ε b)) o ((TMap η (FObj U b )) o f )
≈⟨ assoc ⟩
((FMap U (TMap ε b)) o (TMap η (FObj U b))) o f
≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩
id (FObj U b) o f
≈⟨ idL ⟩
f
∎
ηの可換性と adjoint1 が使われています。adjoint1 は、
A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ]
つまり、
U(ε(b)) o η(U(b)) = id(U(b))
これは、ε(b) が、id(U(b)) の solution であることを示しています。(a = U(b)) の場合。
U(ε(b))
UF(a) -----------------> U(b) = a
<-----------------
η(a)
と η(a)で UF(a) に行ったあと、U(ε(b)) で、U(b) に戻ってくるわけです。
これをηの可換性で f を使って下に引き伸ばすと、任意のfに対する解が得られます。
U(ε(b))
UF(U(b)) -----------------> U(b)
^ <----------------- ^
| η(U(b)) |
| |
UF(f)| |f
| |
| |
UF(a) <----------------- -a
η(a)
この図がηの可換図であることと、U (ε(b) o F(f) ) o η(a) = f であることを示していることを理解できれば証明を理解したことになります。これが Agda の証明に対応していることもわかります。
唯一性
uniqness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} →
A [ A [ FMap U g o TMap η a' ] ≈ f ] → B [ solution f ≈ g ]
を証明することになりますが、仮定に等式が入っているのと、cong が使えないのとで、ちょっと大変です。(cong は、x ≡ y → f x ≡ f y です )
uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
と、k で、仮定の等式 FMap U g o TMap η a' ≈ f を受けています。
solution f
は、
TMap ε b o FMap F f
ですので、ここの f を等式を使って入れ替えます。Agda では代入は簡単ではありません。cong を使うことを意味するからです。圏の射に対する cong はありませんが、IsFunctor.≈-cong (isFunctor F) が使えます。これは、
≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ]
つまり、Functor ならば cong と同じことができます。
≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩
として、lemma1 を呼び出します。
lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g : Hom B (FObj F a) b) →
A [ A [ FMap U g o TMap η a ] ≈ f ] →
B [ (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ]
lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
これで、FMap F f が、(FMap F (A [ FMap U g o TMap η a ] )) に置き換わります。
あとは少し変形すると、
g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) )
となり、ε(F(a)) o F(η(a)) = id(F(a)) という adjoint2 に帰着します。まとめると、こうなります。
uniqness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} →
A [ A [ FMap U g o TMap η a' ] ≈ f ] → B [ solution f ≈ g ]
uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
begin
solution f
≈⟨⟩
TMap ε b o FMap F f
≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩
TMap ε b o FMap F ( A [ FMap U g o TMap η a ] )
≈⟨ cdr (distr F ) ⟩
TMap ε b o ( FMap F ( FMap U g) o FMap F ( TMap η a ) )
≈⟨ assoc ⟩
( TMap ε b o FMap F ( FMap U g) ) o FMap F ( TMap η a )
≈⟨ sym ( car ( nat ε )) ⟩
( g o TMap ε ( FObj F a) ) o FMap F ( TMap η a )
≈⟨ sym assoc ⟩
g o ( TMap ε ( FObj F a) o FMap F ( TMap η a ) )
≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
g o id (FObj F a)
≈⟨ idR ⟩
g
∎
つまり、mapping の方で adjoin1 を使い、uniquness で adjoint2 を使います。Universal mapping の解と唯一性が随伴関手の二つの等式に対おいうしていることがわかります。こちらでは、εの可換性が使われています。
普遍問題は、任意のfに対して唯一の解f* が存在するという量化記号が入った形式ですが、随伴関手では、それが等式二つだけで書けています。
また、uniquenes はε側から見た普遍問題の解に相当することもわかります。二つの証明は構造的にまったく同じなこともわかります。
Hom(F(-),-) = Hom(-,U(-))
随伴関手から普遍問題の解を導けたので、
Hom(F(-),-) = Hom(-,U(-))
を証明することができます。これは、随伴関手の組 F,U は、
f : a -> U(b)
と、
f* :F(a) -> b
とが一対一対応するという意味の式です。Hom(a,b) は、Hom A a b です。a から b への射の集合です。(f : Hom A a b) などとして、その要素 f を取り出していました。
Hom(F(-),-) = λ a b -> Hom A F(a) b
Hom(-,U(-)) = λ a b -> Hom A a U(b)
というわけです。実際、f* は普遍問題の解そのものです。
Hom(F(-),-) = Hom(-,U(-))
から随伴関手を構成するためには、普遍問題の解から随伴関手の二つの自然変換を構成する必要があります。