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.1
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🔗
_ = Precategory _ = Functor _ = is-strict _ = Strict-cats _ = Sets _ = Groups _ = poset→category _ = Disc _ = B _ = Slice _ = Ab↪Sets _ = Hom[_,-] _ = Const
- 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:
- Examples 1.2.6:
- Examples 1.2.7:
- Examples 1.2.8:
1.3 Natural transformations🔗
_ = _=>_ _ = Cat[_,_] _ = _◆_ _ = ◆-interchange _ = よcov₁ _ = yo-is-equiv _ = yo-naturalr _ = yo-naturall _ = constⁿ
- Definition 1.3.1:
_=>_ - Proposition 1.3.2:
Cat[_,_] - Theorem 1.3.3:
- Proposition 1.3.4:
_◆_ - Proposition 1.3.5:
◆-interchange - Examples 1.3.6:
1.4 Contravariant functors🔗
Borceux defines contravariant functors as a distinct object rather than functors from this makes it somewhat difficult to map definitions on a 1-1 basis.
1.5 Full and faithful functors🔗
_ = is-faithful _ = is-full _ = is-fully-faithful _ = is-precat-iso _ = よ-is-fully-faithful _ = よcov-is-fully-faithful _ = Subcat _ = Restrict
1.6 Comma categories🔗
- Definition 1.6.1:
_↓_ - Proposition 1.6.2:
- Definition 1.6.4:
∫cov - Definition 1.6.5:
_×ᶜ_ - Proposition 1.6.6:
Cat⟨_,_⟩
1.7 Monomorphisms🔗
_ = is-monic _ = id-monic _ = monic-∘ _ = monic-cancell _ = has-section _ = has-retract _ = has-retract→monic _ = faithful→reflects-mono _ = embedding→monic _ = monic→is-embedding
- Definition 1.7.1:
is-monic - Proposition 1.7.2:
- Definition 1.7.3:
- Proposition 1.7.4:
has-retract→monic - Proposition 1.7.6:
faithful→reflects-mono - Examples 1.7.7:
1.8 Epimorphisms🔗
_ = is-epic _ = id-epic _ = epic-∘ _ = epic-cancelr _ = has-section→epic _ = faithful→reflects-epi _ = surjective→regular-epi _ = epi→surjective
- Definition 1.8.1:
is-epic - Proposition 1.8.2:
- Proposition 1.8.3:
has-section→epic - Proposition 1.8.4:
faithful→reflects-epi - Examples 1.8.5:
1.9 Isomorphisms🔗
_ = is-invertible _ = id-invertible _ = invertible-∘ _ = invertible→monic _ = invertible→epic _ = has-retract+epic→invertible _ = F-iso.F-map-invertible _ = is-ff→is-conservative _ = equiv≃iso
- Definition 1.9.1:
is-invertible - Proposition 1.9.2:
- 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.10 The duality principle🔗
1.11 Exercises🔗
_ = thin-functor _ = よ-preserves-mono _ = よcov-reverses-epi _ = Curry _ = Uncurry _ = has-section+monic→invertible
- 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🔗
_ = is-product _ = ×-Unique _ = Binary-products.swap-is-iso _ = Cartesian-monoidal _ = is-indexed-product _ = Indexed-product-unique _ = is-indexed-product-assoc
- Definition 2.1.1:
is-product - Proposition 2.1.2:
×-Unique - Proposition 2.1.3:
- 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:
- Examples 2.3.2:
2.4 Equalizers, coequalizers🔗
_ = is-equaliser _ = is-equaliser→iso _ = is-equaliser→is-monic _ = id-is-equaliser _ = equaliser+epi→invertible
- 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🔗
_ = is-pullback _ = Pullback-unique _ = is-monic→pullback-is-monic _ = is-invertible→pullback-is-invertible _ = is-kernel-pair _ = is-kernel-pair→epil _ = is-kernel-pair→epir _ = monic→id-kernel-pair _ = id-kernel-pair→monic _ = same-kernel-pair→id-kernel-pair _ = is-effective-epi.is-effective-epi→is-regular-epi _ = is-regular-epi→is-effective-epi _ = pasting-left→outer-is-pullback _ = Sets-pullbacks
- Definition 2.5.1:
is-pullback - Proposition 2.5.2:
Pullback-unique - Proposition 2.5.3:
- 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
- (1 ⇒ 2):
- 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:
- Examples 2.5.10
2.6 Limits and colimits🔗
_ = Cone _ = is-limit _ = limits-unique _ = is-limit.unique₂ _ = Cocone _ = is-colimit _ = Limit→Equaliser _ = Equaliser→Limit _ = Limit→Pullback _ = Pullback→Limit
- 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.7 Complete categories🔗
- Definition 2.7.2:
is-complete
2.8 Existence theorem for limits🔗
- Proposition 2.8.2:
2.9 Limit preserving functors🔗
_ = preserves-limit _ = is-lex.pres-monos _ = corepresentable-preserves-limits _ = representable-reverses-colimits _ = reflects-limit _ = conservative-reflects-limits
- 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🔗
Borceux uses some outdated terminology here, and also uses a condition that is overly powerful. We opt to stick with the terminology from the nLab instead.
- 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🔗
_ = Free-object _ = free-object-unique _ = free-objects→left-adjoint _ = _⊣_ _ = free-objects≃left-adjoint _ = hom-iso→adjoints _ = make-free-group _ = Free-monoid⊣Forget _ = Disc⊣Γ _ = Γ⊣Codisc
- 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:
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🔗
- Definition 3.3.2:
Solution-set - Theorem 3.3.3:
solution-set→left-adjoint
3.4 Fully faithful adjoint functors🔗
- Proposition 3.4.1:
- Definition 3.4.4:
is-equivalence
3.5 Reflective subcategories🔗
- Definition 3.5.2:
is-reflective
3.6 Epireflective subcategories🔗
3.7 Kan extensions🔗
_ = is-lan _ = is-ran _ = cocomplete→lan _ = ff→pointwise-lan-ext _ = left-adjoint→left-extension _ = is-initial-cocone→is-colimit _ = is-colimit→is-initial-cocone _ = is-colimit→is-initial-cocone _ = adjoint→is-lan-id _ = adjoint→is-absolute-lan
- 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:
- Proposition 3.7.6:
- (1 ⇒ 2)
adjoint→is-lan-id,adjoint→is-absolute-lan
- (1 ⇒ 2)
3.8 Tensor products of set-valued functors🔗
3.9 Exercises🔗
- Exercise 3.9.2:
- 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🔗
_ = is-regular-epi _ = is-strong-epi _ = strong-epi-compose _ = strong-epi-cancell _ = strong-epi+mono→is-invertible _ = is-regular-epi→is-strong-epi _ = is-strong-epi→is-extremal-epi _ = equaliser-lifts→is-strong-epi _ = is-extremal-epi→is-strong-epi
- Definition 4.3.1:
is-regular-epi - Definition 4.3.5:
is-strong-epi - Proposition 4.3.6:
strong-epi-cancel-l
strong-epi-mono→is-invertible
- Proposition 4.3.7:
4.4 Epi-mono factorizations🔗
4.5 Generators🔗
_ = is-separating-family _ = is-separator _ = separating-family→epi _ = epi→separating-family _ = is-strong-separating-family _ = is-regular-separating-family _ = is-dense-separating-family _ = is-dense-separator _ = dense-separator→regular-separator _ = regular-separator→strong-separator _ = is-jointly-faithful _ = is-jointly-conservative _ = separating-family→jointly-faithful _ = jointly-faithful→separating-family _ = separator→faithful _ = faithful→separator _ = strong-separating-family→jointly-conservative _ = lex+jointly-conservative→strong-separating-family _ = strong-separator→conservative _ = lex+conservative→strong-separator _ = equalisers+jointly-conservative→separating-family _ = dense-separating-family→jointly-ff _ = jointly-ff→dense-separating-family _ = zero+separating-family→separator
- Definition 4.5.1:
- Proposition 5.4.2:
- (⇒)
separating-family→epic - (⇐)
epic→separating-family
- (⇒)
- Definition 4.5.3:
- Definition 4.5.4:
- Proposition 4.5.5:
- Definition 4.5.7:
- 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:
- Proposition 4.5.11:
- Proposition 4.5.12:
equalisers+jointly-conservative→separating-family - Proposition 4.5.14
- Proposition 4.5.16:
zero+separating-family→separator
4.6 Projectives🔗
Borceux uses the term “projective” to refer to strong projectives.
_ = is-strong-projective _ = preserves-strong-epis→strong-projective _ = strong-projective→preserves-strong-epis _ = indexed-coproduct-strong-projective _ = retract→strong-projective _ = Strong-projectives _ = strong-projective-separating-faily→strong-projectives _ = zero+indexed-coproduct-strong-projective→strong-projective
- Definition 4.6.1:
is-strong-projective - Proposition 4.6.2: Note that there is a slight typo in Borceux here:
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:
4.7 Injective cogenerators🔗
4.8 Exercises🔗
5 Categories of fractions🔗
5.1 Graphs and path categories🔗
_ = Graph _ = Graph-hom _ = Path-in _ = Path-category _ = Free-category _ = Marked-graph _ = Marked-graphs _ = Marked-free-category
- Definition 5.1.1:
Graph - Definition 5.1.2:
Graph-hom - Definition 5.1.3:
Path-in - Proposition 5.1.4:
Path-category,Free-category - Definition 5.1.5:
Marked-graph,Marked-graphs - Proposition 5.1.6:
Marked-free-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🔗
_ = m⊥m _ = m⊥o _ = o⊥m _ = object-orthogonal-!-orthogonal _ = in-subcategory→orthogonal-to-inverted _ = orthogonal-to-ηs→in-subcategory _ = in-subcategory→orthogonal-to-ηs
- Definition 5.4.1:
m⊥m - Definition 5.4.2:
- 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
- (a ⇒ b)
5.5 Factorisation systems🔗
_ = is-factorisation-system _ = factorisation-essentially-unique _ = E-is-⊥M _ = in-intersection≃is-iso
- 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:
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:
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
- (⇒)
It also serves as an excellent place to find possible contributions!↩︎
References
- Borceux, Francis. 1994. Handbook of Categorical Algebra. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.