証明.

解析的関手 F:SetA→Set に対し、 F♯: Nat(SetA) ⟶ Set γ ⟼ 󰄘cAutEl(F)((γ,c))\AutNat(SetA)(γ) と定める。 ここで、 右辺の余積は、 (γ,c) という形の El(F) の弱正規対象を全て考え、 その各同型類の代表元 c を回るものとする。 また、 右辺の余積の中身は、 左からの自然な群作用 Aut((γ,c))↷Aut(γ) による商集合である。

これにより、 関手 -♯: [SetA,Set]AF ⟶ SetNat(SetA) F ⟼ F♯ が定まった。 射の対応は、 自然に決まる通りである。

逆に、 関手 G:Nat(SetA)→Set に対し、 G♭: SetA ⟶ Set X ⟼ 󰄘γAutNat(SetA)(γ)\(HomSetA(γ,X)×Gγ) と定める。 ここで、 右辺の余積は、 全ての Nat(SetA) の対象 γ を回るものとする。 また、 右辺の余積の中身は、 左からの群作用 Aut(γ)×(Hom(γ,X)×Gγ) ⟶ Hom(γ,X)×Gγ (p,(f,x)) ⟼ (f∘p−1,(Gp)x) による商集合である。

この G♭ は解析的関手になっている。 実際、 Nat(SetA) の対象 γ と群作用 Aut(γ)↷Gγ の軌道 V に対し、 何らかの xV∈V を 1 つ選んで固定し、 KV:={p∈Aut(γ)∣p·xV=xV} とおけば、 G♭X≅󰄘(γ,V)KV\HomSetA(γ,X) が成り立つ。 この余積は、 上記の全ての対 (γ,V) を回るものとする。

この同型は、 以下のように確かめることができる。 まず、 KV は固定部分群だから、 剰余群 Aut(γ)/KV が考えられ、 集合としての同型 Gγ≅󰄘VAut(γ)/KV が成り立つ。 これを用いると、 商集合をとる操作と積をとる操作がともに余積と交換することから、 󰄘γAut(γ)\(Hom(γ,X)×Gγ) ≅ 󰄘γAut(γ)\(Hom(γ,X)×󰄘VAut(γ)/KV( ≅ 󰄘γ󰄘VAut(γ)\(Hom(γ,X)×Aut(γ)/KV) が分かる。 さらに、 少し考えれば、 󰄘γ󰄘VAut(γ)\(Hom(γ,X)×Aut(γ)/KV)≅󰄘(γ,V)KV\Hom(γ,X) も成り立つことが分かる。 これで、 示したかった同型が示せた。

続いて、 射の対応を定める。 別の関手 G󰎘:Nat(SetA)→Set があったとし、 自然変換 ν:G→G󰎘 を考える。 ここで、 ξX♭: G♭X ⟶ G󰎘♭X [f,x]@γ ⟼ [f,ξγx]@γ として、 自然変換 ξ♭:G♭→G󰎘♭ を定める。

この ξ♭ は、 以下に示すように弱カルテシアンになる。 そのためには、 任意の射 u:X→Y に対し、 図式 G♭XG󰎘♭XG♭YG󰎘♭YξX♭G♭uξY♭G󰎘♭u が弱引き戻しであることを示せば良い。 そこで、 任意に [g,x]∈G♭Y と [f,y]∈G󰎘♭X であって、 ξY♭[g,x]=(G♭u)[f,y] を満たしているものをとる。 ξ♭ と G♭ の定義から、 この等式は [g,ξγx]=[u∘f,y] が成り立つということである。 したがって、 群作用の定義により、 ある p∈Aut(γ) が存在して、 g=u∘f∘p−1ξγx=(Hp)y が成り立つ。 このとき、 [f,(Gp−1)x]∈G♭X を考えると、 簡単な計算により、 (G♭u)[f,(Gp−1)x]=[g,x]ξX♭[f,(Gp−1)x]=[f,y] がともに成り立つことが分かる。 これはすなわち、 上の四角形の図式が Set で弱引き戻しであることを意味している。

以上により、 関手 -♭: SetNat(SetA) ⟶ [SetA,Set]AF G ⟼ G♭ も定まった。

この 2 つの関手は同型の違いを除いて互いに逆になっている。 これについては、 今は少し時間がないのでまた後日に。 もしくは、 私のノートの p5745 と p5746 を参照。