Category Theory

Wikipedia

Categories and Precategories

Precategory

1. A : π’ž. -- object 2. A, B : π’ž | A β†’ B : π’ž is-0-type(A β†’ B). -- morphism 3. A : π’ž | 1_A : A β†’ A. -- identity morphism 4. A, B, C : π’ž | g : (B β†’ C) β†’ f : (A β†’ B) β†’ g f : (A β†’ C). -- composition 5. A, B : π’ž | (f : A β†’ B) β†’ f = 1_B f = f 1_A. 6. A, B, C, D : A | f : A β†’ B, g : B β†’ C, h : C β†’ D β†’ h (g f) = (h g) f. -- associative

Isomorphism

Wikipedia nLabf : A β†’ B | f : A β‰… B | (g : B β†’ A) Γ— (g f = 1_A) Γ— (f g = 1_B).

Homotopy Equivalence

f : A β†’ B, g : B β†’ A β†’ ⋆ : g f = 1_A, ⋆ : f g = 1_B β†’ ⋆ : a β‰… b. 1_A : a β‰… a, 1_A^[βˆ’1] = 1_A.

Lemma

(f : A β†’ B) β†’ is-0-type(A β‰… B).

Identity to Isomorphism

precategory A | (a, b : A) β†’ (a = b) β†’ (a β‰… b).

Example

precategory Set | A β†’ B ≑ A β†’ B.

Category

Wikipedia nLabcategory A | precategory A | (a, b : A) β†’ (a = b) ≃ (a β‰… b).

Example

precategory Set | category Set.

Lemma

category A | is-1-type(A).(a, b : A) β†’ is-0-type(a β‰… b) β†’ (a = b) ≃ (a β‰… b) β†’ is-0-type(a = b).

Isomorphism to Identity

isotoid : (a β‰… b) β†’ (a = b).

Lemma

p : a = a', q : b = b', f : A β†’ B β†’(p, q)_*(f) = idtoiso(q) β—¦ f β—¦ idtoiso(p)^[βˆ’1].

Example (Preorder)

precategory A | (a, b : A) β†’ is-(βˆ’1)-type(a β†’ b) | a ≀ a, -- reflexivity a ≀ b β†’ b ≀ c β†’ a ≀ c. -- transitivity(f : a ≀ b) β†’ (g : b ≀ a) β†’ (a β‰… b) β†’ is-(βˆ’1)-type(a β‰… b).(A, ≀) : Preord β†’ (a, b : A) β†’ is-(βˆ’1)-type(a = b) β†’ (a β‰… b β†’ a = b)β†’ (A, _) : πΆπ‘Žπ‘‘.

Example

(A, _) : πΆπ‘Žπ‘‘ β†’ _ : is-0-type(A) ≃ (a, b : A β†’ is-(βˆ’1)-type(a ≃ b)).(A, _) : πΆπ‘Žπ‘‘ β†’ a, b : A β†’ _ : (a β‰… b) ≃ (a = b).

Groupoid

A : U β†’ ⋆ : is-1-type(A) β†’ (A, a = b) : Groupoid. A : U β†’ ⋆ : is-0-type(A) β†’ (A, a = b) : DiscCat.

Fundamental Pregroupoid

A : U β†’ (A, ||a = b||_0) : Precat β†’ a, b, c : A β†’(b = c) β†’ (a = b) β†’ (a = c) β†’ ||b = c||_0 β†’ ||a = b||_0 β†’ ||a = c||_0 β†’(A, ||a = b||_0) : FundPregroupoid.

Homotopy Precategory of Types

(U, ||A β†’ B||_0) : Precat, (U, ||A β†’ B||_0) : HPrecat.

Example

(0-type_U, A β†’ B β†’ (βˆ’1)-type_U) : Precat β†’ A : 0-type_U β†’ 1_A(a, a') ≑ (a = a') β†’ R : A β†’_[𝑅𝑒𝑙] B β†’ S : B β†’_[𝑅𝑒𝑙] C β†’ (S β—¦ R)(a, c) ≑ ||b : B, R(a, b) Γ— S(b, c)|| β†’(0-type_U, A β†’ B β†’ (βˆ’1)-type_U) : 𝑅𝑒𝑙. R : A β‰… B β†’ 1.1. R(a, b), R^[βˆ’1](b', a) β†’ (R β—¦ R^[βˆ’1])(b', b) β†’ b' = b. 1.2. R(a, b), R^[βˆ’1](b, a') β†’ (R^[βˆ’1] β—¦ R)(a, a') β†’ a = a'. 2. a : A β†’ a = a β†’ (R^[βˆ’1] β—¦ R)(a, a) β†’ b : B, R(a, b), R^[βˆ’1](b', a). 3. 4. _ : 𝑅𝑒𝑙 β†’ πΆπ‘Žπ‘‘.

Functors and Transformations

Functor

Wikipedia nLab(A, _), (B, _) : Precat β†’ 1. F : A β†’ B. 2. a, b : A β†’ F_[a, b] : (A β†’ B) β†’ (F(a) β†’_B F(b)). 3. a : A β†’ F_[a, a](1_A) = 1_[F(a)]. 4. a, b, c : A β†’ f : A β†’ B, g : b β†’_A c β†’ F_[a, c](g β—¦ f) = F_[b, c](g) F_[a, b](f).

Natural Transformation

Wikipedia(A, _), (B, _) : Precat β†’ (F, F_[a, b]), (G, G_[a, b]) : Functor β†’ 1. a : A β†’ Ξ³_a : F(a) β†’_B G(a). -- components 2. a, b : A β†’ f : A β†’ B β†’ G_[a, b](f) β—¦ Ξ³_a = Ξ³_b β—¦ F_[a, b](f). -- naturality axiomNatural Transformation

Functor Precategory

(A, _), (B, _) : Precat β†’ (B^A, F β†’_[B^A] G) : Precat β†’ B^A : A β†’ B, F β†’_[B^A] G is the type of natural transformation F β†’ G.

Lemma

A natural transformation Ξ³ : F β†’ G is an isomorphism in B^A if and only if each Ξ³_a is an isomorphism in B.

Theorem

A : Precategory, B : Category β†’ B^A : Category.

Composite of functors

Definition

Functors F : A β†’ B, G : B β†’ C β†’ G_0 F_0 : A_0 β†’ C_0, a, b : A β†’ (G_[F(a), F(b)] F_[a, b]) : (A β†’ B) β†’ ((G F)(a) β†’_C (G F)(b)).

Composite of natural transformations and functors

Definition

F : A β†’ B, G, H : B β†’ C, Ξ³ : G β†’ H, Ξ³ F : G F β†’ H F, a : A, Ξ³_[F(a)], b : B, K(Ξ³_b).

Lemma

F, G : A β†’ B, H, K : B β†’ C, Ξ³ : F β†’ G, Ξ΄ : H β†’ K,(Ξ΄ G) (H Ξ³) = (K Ξ³) (Ξ΄ F).

Lemma

H (G F) = (H G) F.

Adjoint Functors/Adjunction

Wikipedia nLab

Functor F : A β†’ B β†’ is-left-adjoint(F) ≑

  • G : B β†’ A,
  • Ξ· : 1_A β†’ G F (unit),
  • Ξ΅ : F G β†’ 1_B (counit),
  • (e F) (F Ξ·) = 1_F, (G Ξ΅) (Ξ· G) = 1_G (triangle identities).

Equivalence

Definition

is-left-adjoint(F), A ≃ B.

Lemma

F : A β†’ B β†’(A ≃ B) = (G : B β†’ A) Γ— (G F ≃ 1_A) Γ— (F G ≃ 1_B).

Injective

F : A β†’ B β†’ F_[a, b]

'Faithful'.

Surjective

F : A β†’ B β†’ F_[a, b]

'Full'.

Split Essentially Surjective

F : A β†’ B β†’(b : B) β†’ (a : A) Γ— F(a) ≃ b.

Lemma

A, B : Precategory, F : A β†’ B β†’(A ≃ B) ≃ (b : B) β†’ (a : A) Γ— F(a) ≃ b.

Essentially Surjective

F : A β†’ B β†’(b : B) β†’ mere (a : A) Γ— F(a) ≃ b.

Weak Equivalence

F is bijective and essentially surjective.

Lemma

F is bijective, A : Category β†’(b : B) β†’ is-truncated_[βˆ’1]((a : A) Γ— F(a) ≃ b). F is an equivalence = F is a week equivalence.

Isomorphism

F is bijective and F_0 is an equivalence of types. A β‰… B.

Lemma

A, B : Precategory, F : A β†’ B β†’(A β‰… B)≃ ≃.

Lemma

A, B : Precategory β†’(A = B) β†’ (A β‰… B).

Lemma

A, B : Category β†’(A = B) β†’ (A ≃ B).

Dual

Wikipedia nLabA : Precategory β†’ A^* : Precategory, A^*_0 ≑ A_0, a β†’_[A^*] b ≑ A β†’ B.

Product

A, B : Precategory β†’ A Γ— B : Precategory,(A Γ— B)_0 ≑ A_0 Γ— B_0,(a_0, b_0) β†’_[A Γ— B] (a_1, b_1) ≑ (a_0 β†’_A a_1) Γ— (b_0 β†’_B b_1), 1_[(a, b)] ≑ (1_A, 1_B),(g, g') (f, f') ≑ (g f, g' f').

Lemma

A, B, C : Precategory β†’(A Γ— B β†’ C) ≃ (A β†’ C^B).A : Precategory β†’ hom_a : A^* Γ— A β†’ 𝑆𝑒𝑑.(a, b) : A^*_0 Γ— A_0 ≑ A_0 Γ— A_0,(f, f') : (a, b) β†’_[A^* Γ— A] (a', b'),(hom_a)_[(a, b), (a', b')](f, f') ≑ (g ↦ (f' g' f)) : (A β†’ B) β†’ (a' β†’_A b').

Yoneda Embedding

y : A β†’ 𝑆𝑒𝑑^[A^*],

Yoneda Lemma

Wikipedia nLabA : Precategory, a : A, F : 𝑆𝑒𝑑^[A^*] β†’(y a β†’_[𝑆𝑒𝑑^[A^*]] F) β‰… F(a).

Corollary

y : A β†’ 𝑆𝑒𝑑^[A^*] is bijective.

Corollary

A : Category β†’ y_0 : A_0 β†’ (𝑆𝑒𝑑^[A^*])_0 is an embedding.(y a = y b) β†’ (a = b).

Representable

F : 𝑆𝑒𝑑^[A^*] β†’(a : A) Γ— y a β‰… F.

Lemma

A, B : Precategory, F : A β†’ B β†’ is-left-adjoint(F) ≃ (b : B) β†’ is-representable(a ↦ F(a) β†’_b b).

Strict Category

nLabA : Precategory, A_0 ≑ 0-type.

Monomorphism

Wikipedia nLab(m f = m g) β†’ (f = g).

†-category

Structure Identity Principle

Notion of Structure

(P, H), P : X_0 β†’ U, x : X_0, P(x) ((P, H)-structures). x, y : X_0, f : x β†’_X y, Ξ± : P(x), Ξ² : P(y), H_[Ξ± Ξ²](f) ((P, H)-homomorphism). x : X_0, Ξ± : P(x), H_[Ξ± Ξ±](1_x). x, y, z : X_0, Ξ± : P(x), Ξ² : P(y), Ξ³ : P(z), f : x β†’_X y, g : y β†’_X z, H_[Ξ± Ξ²](f) β†’ H_[Ξ² Ξ³](g) β†’ H_[Ξ± Ξ³](g f).(Ξ± ≀_x Ξ²) ≑ H_[Ξ± Ξ²](1_x). A ≑ Str_[(P, H)](X) (precategory of (P, H)-structures), A_0 ≑ (x : X_0) Γ— P(x),(x, Ξ±) : A_0, |(x, Ξ±)| ≑ x.(x, Ξ±), (y, Ξ²) : A_0 β†’(x, Ξ±) β†’_A (y, Ξ²) ≑ {f : x β†’ y | H_[Ξ± Ξ²](f)}.

Theorem: Structure identity principle

X, (P, H), Str_[(P, H)](X).

Definition

P(x) ≑ P_0(x) Γ— P_1(x), P_0(x) ≑ (Ο‰ : Ξ©_0) β†’ x_[|Ο‰|] β†’ x, P_1(x) ≑ (Ο‰ : Ξ©_1) β†’ x_[|Ο‰|] β†’ (βˆ’1)-type_U.

Rezk Completion

Lemma

(g : F(b) β†’_C G(b)) Γ— (a : A) β†’ (f : H(a) ≃ b) β†’ (Ξ³_a) = G(f^[βˆ’1]) g F(f).

Theorem

(- H) : C_b β†’ C_a.

Theorem

A β†’ A_^.

Diagonal Functor

WikipediaC β†’ C Γ— C. a Γ— b : Ξ” β†’ <a, b>.

Functor Category

WikipediaF, G : C β†’ D β†’ Ξ· : F β†’ G, Component of Ξ· at X Ξ·_X : F(X) β†’ G(X), f : X β†’ Y, Ξ·_Y β—‹ F(f) = G(f) β—‹ Ξ·_X.

Diagram

Wikipedia nLabProductSum

Commutative Diagram

Wikipedia nLab

Groupoid

Wikipedia nLabf : A β†’ B, g : B β†’ C, h : C β†’ D g f : A β†’ C, h g : B β†’ D, (h g) f : A β†’ D, h (g f) : A β†’ D, f^[βˆ’1] f = id_a, f f^[βˆ’1] = id_b

Internal Category

nLab

Small category

nLab

Initial Object

Terminal Object

Category of Sets

Wikipedia nLab

Category of Groups

Wikipedia nLab

Category of Rings

Category of Modules

Wikipedia nLab

Category of Manifolds

Wikipedia

Categorification

Wikipedia nLab

Decategorification

nLab

Indexed category

Wikipedia nLab

Limit

Wikipedia

Coinduction

Wikipedia nLab

Corecursion

nLab

References