module Borceux where

Though the 1Lab is not purely a formalization of category theory, it does aim to be a useful reference on the subject. However, the 1Lab organizes content in a highly non-linear fashion; this can make it somewhat difficult to use as a companion to more traditional resources.

This page attempts to (somewhat) rectify this situation by gathering all of the results from Francis Borceux’s “Handbook of Categorical Algebra” (Borceux 1994) in a single place.¹

Volume 1🔗

1 The language of categories🔗

1.1 Logical foundations of the theory🔗

• Proposition 1.1: Russell’s paradox

1.2 Categories and functors🔗

• Definition 1.2.1: Precategory
• Definition 1.2.2: Functor
• Definition 1.2.3: is-strict
• Proposition 1.2.4: Strict-cats
• Examples 1.2.5:
  • 1. Sets
  • 3. Groups
• Examples 1.2.6:
  • 2. poset→category
  • 3. Disc
  • 4. B
• Examples 1.2.7:
  • 1. Slice
• Examples 1.2.8:
  • 1. Ab↪Sets
  • 4. Hom[_,-]
  • 5. Const

1.3 Natural transformations🔗

• Definition 1.3.1: _=>_
• Proposition 1.3.2: Cat[_,_]
• Theorem 1.3.3:
  • 1. yo-is-equiv
  • 2. yo-naturalr
  • 3. yo-naturall
• Proposition 1.3.4: _◆_
• Proposition 1.3.5: ◆-interchange
• Examples 1.3.6:
  • 3. よcov₁
  • 4. constⁿ

1.4 Contravariant functors🔗

Borceux defines contravariant functors as a distinct object rather than functors from ${\mathcal{C}}^{\mathrm{op}}\text{;}$ this makes it somewhat difficult to map definitions on a 1-1 basis.

• Definition 1.4.1: _^op
• Definition 1.4.2: _^op
• Examples 1.4.3:
  • 1. よcov
  • 2. よ₀
  • 3. よ₁
  • 4. よ

1.5 Full and faithful functors🔗

• Definition 1.5.1:
  • 1. is-faithful
  • 2. is-full
  • 3. is-fully-faithful
  • 4. is-precat-iso
• Proposition 1.5.2:
  • 1. よ-is-fully-faithful
  • 2. よcov-is-fully-faithful
• Definition 1.5.3: Subcat
• Definition 1.5.4: Restrict

1.6 Comma categories🔗

• Definition 1.6.1: _↓_
• Proposition 1.6.2:
  • 1. Dom
  • 2. Cod
  • 3. θ
• Definition 1.6.4: ∫cov
• Definition 1.6.5: _×ᶜ_
• Proposition 1.6.6: Cat⟨_,_⟩

1.7 Monomorphisms🔗

• Definition 1.7.1: is-monic
• Proposition 1.7.2:
  • 1. id-monic
  • 2. monic-∘
  • 3. monic-cancell
• Definition 1.7.3:
  • 1. has-section
  • 2. has-retract
• Proposition 1.7.4: has-retract→monic
• Proposition 1.7.6: faithful→reflects-mono
• Examples 1.7.7:
  • 1. embedding→monic, monic→is-embedding

1.8 Epimorphisms🔗

• Definition 1.8.1: is-epic
• Proposition 1.8.2:
  • 1. id-epic
  • 2. epic-∘
  • 3. epic-cancelr
• Proposition 1.8.3: has-section→epic
• Proposition 1.8.4: faithful→reflects-epi
• Examples 1.8.5:
  • 1. surjective→regular-epi, epi→surjective

1.9 Isomorphisms🔗

• Definition 1.9.1: is-invertible
• Proposition 1.9.2:
  • 1. id-invertible
  • 2. invertible-∘
  • 3. invertible→monic, invertible→epic
• Proposition 1.9.3: has-retract+epic→invertible
• Proposition 1.9.4: F-iso.F-map-invertible
• Proposition 1.9.5: is-ff→is-conservative
• Examples 1.9.6:
  • 1. equiv≃iso

1.10 The duality principle🔗

• Definition 1.10.1: _^op
• Examples 1.10.3:
  • 1. Hom[-,-]

1.11 Exercises🔗

• Exercise 1.11.1: 🚧 thin-functor
• Exercise 1.11.5: よ-preserves-mono
• Exercise 1.11.6: よcov-reverses-epi
• Exercise 1.11.8: 🚧 Curry, Uncurry
• Exercise 1.11.9: has-section+monic→invertible

2 Limits🔗

2.1 Products🔗

• Definition 2.1.1: is-product
• Proposition 2.1.2: ×-Unique
• Proposition 2.1.3:
  • 1. Binary-products.swap-is-iso
  • 2. Cartesian-monoidal
• Definition 2.1.4: is-indexed-product
• Proposition 2.1.5: Indexed-product-unique
• Proposition 2.1.6: is-indexed-product-assoc

2.2 Coproducts🔗

• Definition 2.2.1: is-indexed-coproduct
• Proposition 2.2.2: is-indexed-coproduct→iso
• Proposition 2.2.3: is-indexed-coproduct-assoc

2.3 Initial and terminal objects🔗

• Definition 2.3.1:
  • 1. is-terminal
  • 2. is-initial
• Examples 2.3.2:
  • 1. Sets-initial, Sets-terminal
  • 2. 🚧 Zero-group-is-zero

2.4 Equalizers, coequalizers🔗

• Definition 2.4.1: is-equaliser
• Proposition 2.4.2: is-equaliser→iso
• Proposition 2.4.3: is-equaliser→is-monic
• Proposition 2.4.4: id-is-equaliser
• Proposition 2.4.5: equaliser+epi→invertible

2.5 Pullbacks, pushouts🔗

• Definition 2.5.1: is-pullback
• Proposition 2.5.2: Pullback-unique
• Proposition 2.5.3:
  • 1. is-monic→pullback-is-monic
  • 2. is-invertible→pullback-is-invertible
• Definition 2.5.4: is-kernel-pair
• Proposition 2.5.5: is-kernel-pair→epil, is-kernel-pair→epir
• Proposition 2.5.6:
  • (1 ⇒ 2): monic→id-kernel-pair
  • (2 ⇒ 1): id-kernel-pair→monic
  • (3 ⇒ 2): same-kernel-pair→id-kernel-pair
• Proposition 2.5.7: is-effective-epi.is-effective-epi→is-regular-epi
• Proposition 2.5.8: is-regular-epi→is-effective-epi
• Proposition 2.5.9:
  • 1. pasting-left→outer-is-pullback
• Examples 2.5.10
  • 1. Sets-pullbacks

2.6 Limits and colimits🔗

• Definition 2.6.1: Cone
• Definition 2.6.2: is-limit
• Proposition 2.6.3: limits-unique
• Proposition 2.6.4: is-limit.unique₂
• Definition 2.6.5: Cocone
• Definition 2.6.6: is-colimit
• Examples 2.6.7:
  • 2. Limit→Equaliser, Equaliser→Limit
  • 3. Limit→Pullback, Pullback→Limit

2.7 Complete categories🔗

• Definition 2.7.2: is-complete

2.8 Existence theorem for limits🔗

• Proposition 2.8.2:
  • 2. with-equalisers
  • 3. with-pullbacks

2.9 Limit preserving functors🔗

• Definition 2.9.1: preserves-limit
• Proposition 2.9.3: is-lex.pres-monos
• Proposition 2.9.4: corepresentable-preserves-limits
• Proposition 2.9.5: representable-reverses-colimits
• Definition 2.9.6: reflects-limit
• Proposition 2.9.7: conservative-reflects-limits

2.10 Absolute colimits🔗

2.11 Final functors🔗

• Definition 2.11.1: is-final
• Proposition 2.11.2: extend-is-colimit, is-colimit-restrict

2.12 Interchange of limits🔗

2.13 Filtered colimits🔗

2.14 Universality of colimits🔗

• Definition 2.14.1: has-stable-colimits

2.15 Limits in categories of functors🔗

• Proposition 2.15.1: functor-limit
• Theorem 2.15.2: Functor-cat-is-complete
• Proposition 2.15.6: coyoneda

2.16 Limits in comma categories🔗

2.17 Exercises🔗

• Exercise 2.17.3: 🚧 Cone→cone
• Exercises 2.17.8: extend-is-colimit, is-colimit-restrict

3 Adjoint functors🔗

3.1 Reflection along a functor🔗

• Definition 3.1.1: Free-object
• Proposition 3.1.2: free-object-unique
• Proposition 3.1.3: free-objects→left-adjoint
• Definition 3.1.4: _⊣_
• Theorem 3.1.5: free-objects≃left-adjoint, hom-iso→adjoints
• Examples 3.1.6:
  • 1. Free-monoid⊣Forget
  • 2. make-free-group
  • 11. Disc⊣Γ, Γ⊣Codisc

3.2 Properties of adjoint functors🔗

• Proposition 3.2.1: LF⊣GR
• Proposition 3.2.2: right-adjoint-is-continuous

3.3 The adjoint functor theorem🔗

3.4 Fully faithful adjoint functors🔗

• Proposition 3.4.1:
  • (⇒). is-reflective→counit-is-iso
  • (⇐). is-counit-iso→is-reflective
• Definition 3.4.4: is-equivalence

3.5 Reflective subcategories🔗

• Definition 3.5.2: is-reflective

3.6 Epireflective subcategories🔗

3.7 Kan extensions🔗

• Definition 3.7.1: is-lan
• Theorem 3.7.2: cocomplete→lan
• Proposition 3.7.3: ff→pointwise-lan-ext
• Proposition 3.7.4: left-adjoint→left-extension
• Proposition 3.7.5:
  • (⇒) is-initial-cocone→is-colimit
  • (⇐) is-colimit→is-initial-cocone
• Proposition 3.7.6:
  • (1 ⇒ 2) adjoint→is-lan-id, adjoint→is-absolute-lan

3.8 Tensor products of set-valued functors🔗

3.9 Exercises🔗

• Exercise 3.9.2:
  • (⇒) corepresentable→left-adjoint
  • (⇐) right-adjoint→objectwise-rep
• Exercise 3.9.3: Karoubi-is-completion

4 Generators and Projectives🔗

4.1 Well-powered categories🔗

4.2 Intersection and union🔗

4.3 Strong epimorphisms🔗

• Definition 4.3.1: is-regular-epi
• Definition 4.3.5: is-strong-epi
• Proposition 4.3.6:
  • 1. strong-epi-compose
  • 2. strong-epi-cancel-l
  • 3. strong-epi-mono→is-invertible
  • 4. is-regular-epi→is-strong-epi
  • 5. is-strong-epi→is-extremal-epi
• Proposition 4.3.7:
  • 1. equaliser-lifts→is-strong-epi
  • 2. is-extremal-epi→is-strong-epi

4.4 Epi-mono factorizations🔗

4.5 Generators🔗

• Definition 4.5.1:
  • is-separating-family
  • is-separator
• Proposition 5.4.2:
  • (⇒) separating-family→epic
  • (⇐) epic→separating-family
• Definition 4.5.3:
  • is-strong-separating-family
  • is-regular-separating-family
• Definition 4.5.4:
  • is-dense-separating-family
  • is-dense-separator
• Proposition 4.5.5:
  • dense-separator→regular-separator
  • regular-separator→strong-separator
• Definition 4.5.7:
  • is-jointly-faithful
  • is-jointly-conservative
• Proposition 4.5.8:
  • (⇒) separating-family→jointly-faithful
  • (⇐) jointly-faithful→separating-family {.Agda}
• Proposition 4.5.9:
  • (⇒) separator→faithful
  • (⇐) faithful→separator
• Proposition 4.5.10:
  • (⇒) strong-separating-family→jointly-conservative
  • (⇐) lex+jointly-conservative→strong-separating-family
• Proposition 4.5.11:
  • (⇒) strong-separator→conservative
  • (⇐) lex+conservative→strong-separator
• Proposition 4.5.12: equalisers+jointly-conservative→separating-family
• Proposition 4.5.14
  • (⇒) dense-separating-family→jointly-ff
  • (⇐) jointly-ff→dense-separating-family
• Proposition 4.5.16: zero+separating-family→separator

4.6 Projectives🔗

• Definition 4.6.1: is-strong-projective
• Proposition 4.6.2: Note that there is a slight typo in Borceux here: $\mathcal{C}(P,-)$ must preserve strong epimorphisms. (⇒) preserves-strong-epis→strong-projective (⇐) strong-projective→preserves-strong-epis
• Proposition 4.6.3: indexed-coproduct-strong-projective
• Proposition 4.6.4: retract→strong-projective
• Definition 4.6.5: Strong-projectives
• Proposition 4.6.6: strong-projective-separating-faily→strong-projectives
• Proposition 4.6.7:
  • (⇒) zero+indexed-coproduct-strong-projective→strong-projective
  • (⇐) indexed-coproduct-strong-projective

4.7 Injective cogenerators🔗

4.8 Exercises🔗

5 Categories of fractions🔗

5.1 Graphs and path categories🔗

• Definition 5.1.1: Graph
• Definition 5.1.3: Path-in
• Proposition 5.1.4: Path-category

5.2 Calculus of fractions🔗

• Proposition 5.2.2: Localisation

5.3 Reflective subcategories as categories of fractinos🔗

5.4 The orthogonal subcategory problem🔗

• Definition 5.4.1: m⊥m
• Definition 5.4.2:
  1. m⊥o
  2. o⊥m
• Proposition 5.4.3: object-orthogonal-!-orthogonal
• Proposition 5.4.4:
  • • (a ⇒ b) in-subcategory→orthogonal-to-inverted
    • (a ⇒ c) in-subcategory→orthogonal-to-ηs

5.5 Factorisation systems🔗

• Definition 5.5.1: is-factorisation-system
• Proposition 5.5.2: factorisation-essentially-unique
• Proposition 5.5.3: 🚧 E-is-⊥M
• Proposition 5.5.4:
  • 3. in-intersection≃is-iso

5.6 The case of localisations🔗

5.7 Universal closure operations🔗

5.8 The calculus of bidense morphisms🔗

5.9 Exercises🔗

6 Flat functors and Cauchy completeness🔗

6.1 Exact functors🔗

• Definition 6.1.1: is-lex

6.2 Left exact reflection of a functor🔗

6.3 Flat functors🔗

6.4 The relevance of regular cardinals🔗

6.5 The splitting of idempotents🔗

• Definition 6.5.1: is-idempotent
• Proposition 6.5.2: is-split→is-idempotent
• Definition 6.5.3: is-split
• Definition 6.5.8: is-idempotent-complete
• Proposition 6.5.9: Karoubi-is-completion

6.6 The more general adjoint functor theorem🔗

6.7 Exercises🔗

7 Bicategories and distributors🔗

7.1 2-categories🔗

7.2 2-functors and 2-natural transformations🔗

7.3 Modifications and n-categories🔗

7.4 2-limits and bilimits🔗

7.5 Lax functors and pseudo-functors🔗

7.6 Lax limits and pseudo-limits🔗

7.7 Bicategories🔗

• Definition 7.7.1: Prebicategory
• Definition 7.7.2: _⊣ᵇ_
• Example 7.7.3: Spanᵇ

7.8 Distributors🔗

7.9 Cauchy completeness versus distributors🔗

7.10 Exercises🔗

8 Internal category theory🔗

8.1 Internal categories and functors🔗

• Definition 8.1.1: Internal-cat
• Definition 8.1.2: Internal-functor
• Definition 8.1.3: _=>i_
• Examples 8.1.6:
  • 1. Disci
  • 3. _^opi

8.2 Internal base-valued functors🔗

• Definition 8.2.1: Outer-functor
• Definition 8.2.2: _=>o_
• Proposition 8.2.3: Outer-functors
• Example 8.2.4: ConstO, const-nato

8.3 Internal limits and colimits🔗

8.4 Exercises🔗

• Exercise 8.4.6:
  • (⇒) dependent-product→lcc
  • (⇐) lcc→dependent-product