豊穣圏 - 雑多な感じ

豊穣圏

enriched category

summary.icon

モノイダル圏$ V をhomに持つ圏

最初にやった人がVってつけたから

豊穣圏の話をするときはVにしがち

signature.icon

code:enriched_category.sig

sig EnrichedCategory in CAT @ %

Data

model

MonoidalCategory V ⊗ i α λ ρ

%0-morph

.0-morph @ Ob : CLASS

%1-morph

hom : Ob × Ob -> V

%2-morph

"identity element" @ id

: ! * i => Δ * hom

: Ob -> V

"composition morphism" @ comp

: Ob^ × Δ × Ob^ ; hom ⊗ hom

=> Ob^ × ! × Ob^ ; hom

: Ob × Ob × Ob -> V

Axioms

%3-eq "associative"

comp ⊗ hom^; comp

=(hom×hom×hom)α; hom^ ⊗ comp; comp

: Ob^ × Δ × Δ × Ob^; (hom⊗hom)⊗hom

=> Ob^ × ! × ! × Ob^ ; hom

: Ob × Ob × Ob × Ob -> V

%3-eq "left unital"

: ⊗ hom

Ref.icon モノイド圏、豊饒圏、閉圏と内部ホム - 檜山正幸のキマイラ飼育記 (はてなBlog)

Ref.icon enriched category in nLab

失敗録:Δで考えると向き辻褄が合わない→トレースだ！