İşlev olarak kategoriler

Question

Programcılar için Kategori Teorisi kitabı üzerinde çalışıyorum .

Burada kitapta kategori örneği olarak "<=" ilişkisini buluyorum: özdeşlik ilişkisine ( a <= a) saygı duyuyor ve birleştirilebilir ( a <= b, b <= c -> a <= c).

Benim için net olmayan şey, 3. sayfadaki kitapta bahsedildiği gibi, morfizmler ve işlevler arasındaki analojidir: bir işlev, belirli bir değerin <= herhangi bir değerini döndüremeyeceğinden, sipariş kategorisini uygulayamaz, yani ... nedir morfizmler ve fonksiyonlar arasındaki ilişki? Görünüşe göre morfizmler tipler arasındaki bağlantılar, oysa fonksiyon tanımları değerler arasındaki bağlantılar, bu yüzden ikincisi bana birincisinin özel bir uygulaması gibi geliyor.

Bu, orada gördüğüm tüm kimlik işlevleri örnekleriyle çelişirdi, ancak bir kimlik işlevi, aynı değere sahip bir değeri değil, aynı türdeki bir türü eşleyeceğinden, örneğin, doğru bir f x = x + 1" ok" ve aynı türden, ki bu açıkça doğru değil.

Öte yandan, böyle kategori temsilleri görüyorum:

Burada A bir tür mü yoksa bir nesne mi?

Answer 1

Neyin kafanızın karıştığını tam olarak anlamıyorum ve özellikle "bir işlev sipariş kategorisini uygulayamaz" ile ne demek istediğinizi tam olarak anlamıyorum, bu yüzden alakalı olduğunu umduğum bazı şeyler söyleyeceğim.

1. Morfizmler, işlevler açısından herhangi bir özel yoruma sahip olarak başlamazlar. Çıplak kategori aksiyomları size sadece bir grup nesne ve ok ve okların nasıl oluşturulması gerektiğine dair aksiyom verir ve bu aksiyomlar herhangi bir kısmi düzen tarafından karşılanır. $\le$, ve bu kadar. Başlarken, kategorileri bu "çıplak" şekilde düşünmenin en az kafa karıştırıcı yolunun, onları kenarlarda bir birleştirme işlemiyle donatılmış yönlendirilmiş grafikler olarak düşünmek olduğunu düşünüyorum .

2. Öte yandan, her kategori$C$Yoneda yerleştirmesi var $C \to [C^{op}, \text{Set}]$, bu bize morfizmlerin seçkin bir yorumunu verir$f : x \to y$fonksiyonlar olarak$f : \text{Hom}(a, x) \to \text{Hom}(a, y)$genelleştirilmiş noktalarda , burada genelleştirilmiş bir nokta$x$sadece herhangi bir morfizm$a \to x$neyse. Bu, morfizmleri yorumlamamızı sağlar$x \le y$aşağı kümelerden işlevler (zorunlu olarak benzersiz) olarak kısmi bir sırada $\{ a : a \le x \}$düşüşlere$\{ a : a \le y \}$, yani benzersiz işlev gönderme$a$ile$a$.

3. Nesneler ayrıca türler açısından herhangi bir özel yoruma sahip olarak başlamazlar. Tip teorisi, kategorilere bakmanın veya onları oluşturmanın özel bir yoludur ve tek yol bu değildir. Tip teorileri için standart kategorik semantikte, nesneler tiptir (olarak yorumlanır).$A$ve morfizmler$f : A \to B$giriş türüyle (olarak yorumlanır) işlevlerdir$A$ve çıkış tipi$B$. Bir kategorinin bir terminal nesnesi varsa $1$(birim tipi olarak yorumlanabilir) sonra morfizmler$1 \to A$tür terimleri olarak yorumlanabilir$A$ve bir morfizm$f : A \to B$daha sonra gerçek bir işleve neden olur$\text{Hom}(1, A) \to \text{Hom}(1, B)$tür şartları gönderme$A$tür açısından$B$. Genellikle yeterli "nokta" yoktur (işlevler$1 \to A$) bunu birçok kategoride ilginç bir işlem haline getirmek için; örneğin, pozlarda$1$, eğer varsa, maksimal bir elemandır , yani$\text{Hom}(1, A)$sürece boş$A$aynı zamanda maksimumdur.