PS

Reader monads in String diagrams

@deprecated 代わりに Reader monad transformers in string diagrams - PS を参照。 Constant morphism Reader monad を たちにばらまいている。 参考文献 All About Monads - HaskellWiki

State monads in String diagrams

Monoidal category にて・・・ Diagonal morphism Naturality Terminating morphism (とはたぶん呼ばない) Naturality これらは、より一般には cartesian monoidal category のときに作れる。 State monad get/put 参考文献 [1203.0202] Pictures of Processes:…

Haskell-monads in String diagrams

@deprecated 代わりに Haskell-monads in string diagrams rev.2 - PS を参照。 Monoidal category にて・・・ Haskell-monad の flip 版を使った方が分かりやすいみたい。*1 Haskell-monad laws Kleisli composition Haskell-monad @deprecated Haskell-monad …

Basic Concepts of Enriched Category Theory

Basic Concepts of Enriched Category Theory というすごい本についての感想と補足・・・ 動機 Category Theory (Oxford Logic Guides) を読んでも Coyoneda らしきものが出てこない。 予備知識 Monoidal category の coherence 要件が(凡人には)複雑すぎて遅か…

Enriched hom functors preserve weighted limits

命題: Limits in 証明 実装 補題: A reduction of limits in 命題: Hom functors preserve limits (Limits via limits in ) 証明 および、補題により確かに Preservation of weighted limits - PS の形になる。 参考文献 Basic Concepts of Enriched Category…

Enriched Kan adjoints

定義: Precomposition functor Exponentiation 2-functor on enriched categories - PS の を使って、 命題 Left Kan extension: について -natural in しかも、この representation の unit は 。 証明 参考文献の通り(に計算する)。 系: Kan adjoints Left…

Conical limits in enriched categories

定義: 1-limits 1-functor: 命題: 1-limits via weighted limits 証明 Representability による limit - PS による。 による。 命題 1-functor: 1-category: -category: について、Free enriched category - PS による 2-adjunction: を使うと -natural in …

Preservation of ends

(の定義が抜けていたので・・・) Preservation of ends -functor: および -end: について が -end となること。 記法 命題: Internal hom functors preserve ends (と呼ぶのが良さそう) 証明 記法 参考文献 Basic Concepts of Enriched Category Theory

Naturality of Yoneda bijections

1-naturality of Yoneda bijections についての 1-naturality*1: 特に のときは 系 つまり で、かつ iso ならば iso 参考文献 Basic Concepts of Enriched Category Theory *1:comma category 間の 1-functoriality でもある

(Co)ends in enriched categories

End 特に、 のとき、 preserves ends より記号に矛盾は無い。 Coend 命題: (Co)ends via weighted (co)limits existence-compatible 証明 命題: (Co)powers preserve (co)ends ただし、preservation of ends は (Co)ends via weighted (co)limits を通して P…

(Co)power

Constant enriched functor Unit category からの constant functor を と定義できる。 命題 Unlambda は iso。 証明 Power 上記の命題により、constant -functor の weighted limit と existence-compatible: 特に のとき、flip iso により記号に矛盾はない…

Free enriched category

Free enriched category 1-category について -category: を Unit-copower monoidal functor - PS を使って次のように定義できる。 これは monoidal functoriality により確かに -category になる。 Enriching 2-functor 上記と同様にして Unit-copower mono…

Unit-copower monoidal functor

(・・・とでも呼んでみる) 以下、curry(close) bijection の箱の添字は省略する。 Copowers in 1-categories natural in Copower bijections 上記の natural isomorphism は copower injection: による bijection: により表すことができるのであった。 命題: Cl…

Enriched Kan extension

以下、Lambda 記法 - PS を使う。 Right Kan extension -functor: について、要件: 任意の -functor: について を満たす -functor: -natural transformation: のペアのことを right kan extension of along といい、特に を(一つ選んで) *1 と書く。また、 …

Lambda 記法

やっぱり lambda 記法の方が読みやすい。*1 Lambda 記法 と書くことにする*2と、例えば Pointwise weighted limits - PS は となって覚えやすい(と思う)。 と も区別しなくてよくなる。 Unlambda (Evaluation) 特に、Enriched functor category - PS で使っ…

Enriched isomorphism まとめ

記法 *1 *2 Ends Fubini Yoneda bijections (Co)representations Yoneda Limits Colimits Limits in self-enriched categories Yoneda via (co)limits Fubini via (co)limits Powers Copowers Continuity in weights Ends in enriched categories Coends in …

Limit-cylinder

Weighted limit の limiting-cone 的なもの。 記法.1 @deprecated 以下、Currying の記法 を使って とする。 記法.1' 以下、Lambda 記法 - PS を使って とする。 Cylinder -morphism: のこと。Enriched Yoneda lemma (weak form) - PS の対応により -natural…

Weighted limits via conical limits

Conical (co)limits Weighted (co)limit に対してフツーの (co)limit のことを conical (co)limit という。 *1 に注意すると、特に weight が constant functor: の場合の weighted (co)limit が conical (co)limit である: Category of elements Any set-va…

RAPL

@deprecated 代わりに RAPL in string diagrams - PS を参照。 記法.1 の limiting cone を それへの mediator を と書いてしまうことにする。 記法.2 命題 Right Adjoints Preserve Limits: adjunction について ならば 証明.1 よって Universality - PS よ…

Existence-compatibility of representations

(・・・とでも) 記法 命題.1 記法 -functor: について となるとき と書くことにする。 の記号はこの記事以外では省略する。 命題.2 -functor: について -natural in ならば 証明 命題.3 かつ or ならば -natural in 証明 Existence-compatibility @error -funct…

Weighted limits of representations

記法 Representation について と書くことにする。定義により 命題 -functor: について ならば preserves the 記法 証明 まず、Enriched representability - PS の命題より右辺は well-formed。 これを計算すると確かに Preservation of weighted limits - P…

Fubini theorem in weighted limits

記法.1 @deprecated と(勝手に)書くことにする。詳しくは Monoidal product of enriched categories - PS Self-enriched monoidal product - PS を使って 記法.2 命題 証明 系 Dual 証明 @deprecated 参考文献 Basic Concepts of Enriched Category Theory (…

Every presheaf is a colimit of representables

以下、Lambda 記法 - PS の記法を使う。 Pointwise weighted limits Pointwise weighted limits - PS より: Pointwise weighted colimits (怪しい)証明 @deprecated @deprecated Contravariant Yoneda embedding @deprecated 命題 証明 具体的には、以下の二…

Weighted colimit

Opposite category の記法 @deprecated とすると は functorial にならないことに注意する。 以下、この記法により variance を明示する。 Weighted limit @deprecated Weighted colimit @deprecated Commutativity Symmetricity of weighted colimits 証明 …

Pointwise weighted limits

Currying の記法 @deprecated -functor: について、curry isomorphism により対応する -functor: を と書くことに(勝手に)する。 Lambda 記法 Lambda 記法 - PS を参照。 命題 -functor: について、weighted limit の族: が存在するならば (右辺は Enriched …

Fubini theorems via ends

Fubini theorem.1 -functor: について 証明 1.について(2.も同様)・・・ 左辺から右辺: 右辺から左辺: Fubini theorem.2 証明 参考文献 Basic Concepts of Enriched Category Theory (2.1)

Enriched RAPL

Weighted limits in self-enriched categories Weighted limit による enriched Yoneda lemma - PS の命題より となるのであった。 HPL (という略語は見たことがない) enriched Hom functors Preserve weighted Limits: (Enriched hom functors preserve wei…

Enriched adjunction

Hom-object adjunction -functor: (left adjoint) (right adjoint) および -natural isomorphism in : (adjoint iso) からなる代数的構造のこと。 Enriched representability - PS の命題により representation of の族: が存在すれば十分である。 命題 Hom-…

Identity natural transformation による functorial equality

命題 Natural transformation: について 証明

Preservation of weighted limits

Preservation of weighted limits -enriched functor: について、-weighted limit of が存在するとき、その counit を とすると が iso になっているとき preserves the limit と言う。 記法 参考文献 Basic Concepts of Enriched Category Theory (3.2)