Skip to content

Instantly share code, notes, and snippets.

@mathink

mathink/coq_cat_functor.md

Created April 3, 2020 00:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mathink/3ac0370f703ad4f6ac79b8878eb3552d to your computer and use it in GitHub Desktop.
Save mathink/3ac0370f703ad4f6ac79b8878eb3552d to your computer and use it in GitHub Desktop.
Download ZIP
Coq で圏論：函手とその等価性
Raw
coq_cat_functor.md
title tags author slide
Coq で圏論：函手とその等価性
Coq Coq-8.5
mathink
false

まとめ

前提

Coq で圏論をやるにあたっての方針的なものは 前回の記事(Coq で圏論：背景と普遍性について) に少し書いてあるので、そちらを読んでからだとわかりやすいかもしれません。

以降のコードを追うには Setoid と、圏の型 Category の定義が必要になります。 これらについてはそれぞれ

あと、 Universe polymorphism は大事なので、忘れずに。

函手の定義

圏 $C$ から圏 $D$ への函手とは、対象の割り当て $F_O: |C| \rightarrow |D|$ と、それに依存した射の割り当て $F_{A(X,Y)}: C(X,Y) \rightarrow D(F_O(X),F_O(Y))$ の組 $F = (F_O, F_{A})$ で、 $F_A$ が射の合成と恒等射を保存するものです。

函手が満たすべき性質をまとめて仕様として書き下すと、以下の型クラス IsFunctor が定義できます。

Class IsFunctor (C D: Category)
      (fobj: C -> D)
      (fmap: forall {X Y: C}, C X Y -> D (fobj X) (fobj Y)) :=
  {
    fmap_proper:>
              forall X Y: C, Proper ((==) ==> (==)) (@fmap X Y);
    fmap_comp:
      forall (X Y Z: C)(f: C X Y)(g: C Y Z),
        fmap (g \o f) == fmap g \o fmap f;
    fmap_id:
      forall X: C, fmap (Id X) == Id (fobj X)
  }.

fmap_proper は f == g の時に fmap f == fmap g が成り立つことを保証するためのものです。 圏の hom は Setoid ですから、この仮定は割り当て fmap が well-defined であることを述べています。

そして、 C から D への函手を表す型 Functor C D が次のように定義されます。

Structure Functor (C D: Category): Type :=
  {
    fobj:> C -> D;
    fmap: forall {X Y: C}, C X Y -> D (fobj X) (fobj Y);

    fun_prf:> IsFunctor (@fmap)
  }.
Existing Instance fun_prf.

Notation "C --> D" := (Functor C D).
Arguments fmap_comp {C D fobj fmap F}{X Y Z}(f g): rename, clear implicits.
Arguments fmap_id {C D fobj fmap F}(X): rename, clear implicits.

Notation "[ 'Functor' 'by' fmap 'with' fobj ; C 'to' D ]" := (@Build_Functor C D fobj fmap _).
Notation "[ 'Functor' 'by' fmap 'with' fobj ]" := [Functor by fmap with fobj ; _ to _].
Notation "[ 'Functor' 'by' fmap ]" := [Functor by fmap with _].
Notation "[ 'Functor' 'by' f :-> Ff 'with' X :-> FX ; C 'to' D ]" := [Functor by (fun _ _ f => Ff) with (fun X => FX) ; C to D].
Notation "[ 'Functor' 'by' f :-> Ff 'with' X :-> FX ]" := [Functor by f :-> Ff with X :-> FX ; _ to _].
Notation "[ 'Functor' 'by' f :-> Ff ; C 'to' D ]" :=
  [Functor by f :-> Ff with _ :-> _ ; _ to _].
Notation "[ 'Functor' 'by' f :-> Ff ]" := [Functor by f :-> Ff with _ :-> _ ; _ to _].

Notation がごちゃごちゃしていますが、あまり気にしないでください。

具体例

定数函手

面白みも何もないですが、私の作っているライブラリではこのようにして函手を構成するのだ、という例になります。

Program Definition constant_functor (C D: Category)(d: D): C --> D :=
  [Functor by f :-> Id d with c :-> d].
Notation "[ * 'in' D |-> c 'in' C ]" := (constant_functor D C c).

対象は全て d へ、射は全て Id d へ。それをそのまま書き下しています。

本来ならば Program Definition の後に函手性の証明が求められますが、この記事では省略しています。

二種類の hom 函手

Notation と Program の組み合わせの使い方の例示も兼ねて、函手の例として、共変と反変、二つの hom 函手を定義してみます。

まずは共変 hom 函手 $C(X,-): C \rightarrow Setoids$ です。 これは対象 $Y$ を $C(X,Y)$ に割り当て、射 $g: Y \rightarrow Z$ に対しては $g$ の後ろからの合成 $g \circ -: C(X,Y) \rightarrow C(X,Z)$ を割り当てるものです。

後ろからの合成は hom setoid の間の変換になるので、 Map の定義記法 を利用して記述しています。

Program Definition covariant_hom_functor (C: Category)(X: C)
  : C --> Setoids :=
  [Functor by (fun (Y Z: C)(g: C Y Z) => [ f in C X Y :-> g \o f])
   with (fun Y => C X Y)].
Notation "'Hom' ( X , -)" := (covariant_hom_functor _ X) (format "'Hom' ( X ,  -)").

Program Definition のあとには、 covariant_hom_functor の函手性の他、 [f in C X Y -> g \o f] が実際に Map (C X Y) (C X Z) 型のデータであること、つまり $g \circ -$ の well-definedness の証明も求められます。

次に、反変 hom 函手 $C(-,Y): C^{op} \rightarrow Setoids$ を定義します。双対圏の定義はここ です。 これは対象 $X$ を $C(X,Y)$ に割り当て、射 $f: W \rightarrow X$ に対しては $f$ の前からの合成 $- \circ f: C(X,Y) \rightarrow C(W,X)$ を割り当てます。 covariant_hom_functor と似たやり方で、次のような定義になります。

Program Definition contravariant_hom_functor (C: Category)(Y: C)
  : C^op --> Setoids :=
  [Functor by (fun (X W: C)(f: C W X) => [g in C X Y :-> g \o f] )
   with (fun X => C X Y)].
Notation "'Hom' (- , Y )" := (contravariant_hom_functor _ Y) (format "'Hom' (- ,  Y )").

以上で、二つの hom 函手を構成することができました。 今回はこれ以上の出番はないですが、米田の補題とかを扱うときには出てきます。

データ型と函手

option や list は　Type -> Type 型を持つ型変換子です。 これらは、それぞれに対応した map でもって、 Type の圏 Types 上の自己函手(定義域と値域が同じ函手)を構成します。

Definition _option := option.
Program Definition option: Types --> Types :=
  [Functor by f :-> option_map f].
Definition _list := list.
Program Definition list: Types --> Types :=
  [Functor by f :-> map f].

アンダーバーを付けて型名をエスケープしているのは、函手の名前を option とか list にしてみたかったからです。 coercion のおかげで、これでも X: Type に対して list X とか書けるので、なかなか便利です。

また、 option や list からは Setoid を作ることもできるので、そうすると Setoids 上の自己函手を構成することも可能です。 気になる方は ここ を見てください。

圏の圏 Cat

函手 $F: C \rightarrow D$ を圏の間の射と見做せば、圏の圏を構築することができます。

函手の等価性について

しかし、圏の圏を構築するにあたって、一つ問題になることがあります。 函手の等価性です。

前回の記事 では、圏で重要なのは射とその間の等価性である、的なことを言っていました。 とすれば、圏の圏における射であるところの函手の等価性も、重要になってきます。

函手は対象の割り当て $F_O$ と射の割り当て $F_A$ の組 $F=(F_O,F_A)$ でした。 そこで、函手の等価性を

$$F = G :\Leftrightarrow \forall f \in C(X,Y). F_A(f) = G_A(f)$$

と定めれば一見うまくいきそうです。この定義は $\forall X. F_O(X) = G_O(X)$ も内包しているからです。

ですが、この「内包しているからです」の部分が Coq 上で定義しようとすると問題になります。

上述の条件について Coq 上で考えてみると $F_A(f)$ は fmap F f: D (F X) (F Y) であり、 $G_A(f)$ は fmap G f: D (G X) (G Y) です。つまり、両者の型が異なっています。 射の等価性は異なる型を考慮していないので、 fmap F f == fmap G f と書くことはできません。

それを解決するため、圏の射に特化した JMeq 的なもの、その名も hom_eq を用意してそれを用いることにします。

Inductive hom_eq (C : Category)(X Y: C)(f: C X Y):
  forall (Z W: C), C Z W -> Prop :=
  hom_eq_def:
    forall (g: C X Y), f == g -> hom_eq f g.
Notation "f =H g 'in' C" := (@hom_eq C _ _ f _ _ g) (at level 70, g at next level).
Infix "=H" := hom_eq (at level 70, only parsing).

この hom_eq を用いることで、型の異なる二つの射についても等価性の記述ができるようになります。 一応、この hom_eq が「同値関係」的なものであることを、以下の補題で示しておきます。

Lemma hom_eq_refl:
  forall (C: Category)(df cf: C)(bf: C df cf),
    bf =H bf.

Lemma hom_eq_sym:
  forall (C: Category)
         (df cf: C)(bf: C df cf)
         (dg cg: C)(bg: C dg cg),
    bf =H bg -> bg =H bf.

Lemma hom_eq_trans:
  forall (C : Category)
         (df cf: C)(bf: C df cf)
         (dg cg: C)(bg: C dg cg)
         (dh ch: C)(bh: C dh ch),
    bf =H bg -> bg =H bh -> bf =H bh.

注意すべきは JMeq x y -> x = y が公理なしには言えないのと同様、 hom_eq f g -> f == g は一般には言えないということです。 そして、 Coq.Logic.JMeq が JMeq x y -> x = y を公理として採用しているのとは異なり、 Coq 上で圏論を行なうにあたっては(今のところ) hom_eq f g -> f == g を公理として採用することはしません。 おそらく矛盾はしないと思のですが、基本的に公理の追加なしに圏論を展開することを目標としているからです。

さて、この hom_eq を使うことで、 Functor の Setoid を作ることが出来ます。

Program Definition Functor_setoid (C D: Category): Setoid :=
  [Setoid by `(forall (X Y: C)(f: C X Y), fmap F f =H fmap G f) on C --> D].
Canonical Structure Functor_setoid.

hom_eq_refl などは、この際に求められる Setoid 性の証明のための補題でもあります。

また、ここにある Canonical Structure コマンドは、これ以降、圏の圏 Cat を定義したあとに二つの函手 F, G について G \o F として合成を記述できるようにするためのものです。 何のことやら、という人は気にしないでおいてください。

Cat を定義する

さて、函手の等価性が定義できさえすれば、あとは、函手の合成と恒等函手を定義するだけで Coq 上で圏の圏 Cat を定義することが出来ます(もちろん、圏であることの証明は要りますが)。

Program Definition Functor_compose (C D E: Category)(F: C --> D)(G: D --> E): C --> E :=
  [Functor by f :-> fmap G (fmap F f)].

Program Definition Functor_id (C: Category): C --> C :=
  [Functor by f :-> f].

Program Definition Cat: Category :=
  [Category by Functor_setoid with Functor_compose, Functor_id].
Canonical Structure Cat.

ちなみに、 Universer polymorphism のおかげで

Check Cat: Cat: Cat.

なんてことをすることも可能です。 universe について多相的に Cat が定義されているので、三つの Cat はそれぞれ異なるレベルにあるということです。 こうしてみると、通常の圏論における大小の問題が Coq の上では少し異なる様相をしているのが見てとれるかなと思います。

最後に

函手を定義するだけなら難しくはないのですが、函手の等価性を考えてみると少々厄介なのでした。 今のところ、 Coq 上で圏論を展開するにあたっては圏の圏 Cat は Setoids ほど出番がないんですけども。

次回予告

自然変換、米田の補題、データ型との関係、的なものを書いてみようと思います。 同じテーマの文書は世に溢れておりますが、 Coq 上でやるんだからまぁいいかな、という気持ちです。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment