Category theory

Content created by Egbert Rijke, Fredrik Bakke, Fernando Chu, Elisabeth Bonnevier, Jonathan Prieto-Cubides, Emily Riehl, Daniel Gratzer, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2022-03-11.
Last modified on 2023-09-21.

Examples of categories and large categories

Category	File
Commutative Rings	`commutative-algebra.category-of-commutative-rings`
Groups	`group-theory.category-of-groups`
Rings	`ring-theory.category-of-rings`
Semigroups	`group-theory.category-of-semigroups`
Sets	`foundation.category-of-sets`

Examples of precategories and large precategories

Precategory	File
Abelian groups	`group-theory.precategory-of-abelian-groups`
Commutative monoids	`group-theory.precategory-of-commutative-monoids`
Commutative rings	`commutative-algebra.precategory-of-commutative-rings`
Commutative semirings	`commutative-algebra.precategory-of-commutative-semirings`
Concrete groups	`group-theory.precategory-of-concrete-groups`
Finite species	`species.precategory-of-finite-species`
`G`-sets	`group-theory.precategory-of-group-actions`
Groups	`group-theory.precategory-of-groups`
Monoids	`group-theory.precategory-of-monoids`
Rings	`ring-theory.precategory-of-rings`
Semigroups	`group-theory.precategory-of-semigroups`
Semirings	`ring-theory.precategory-of-semirings`
Sets	`foundation.category-of-sets`

Files in the category theory folder

module category-theory where

open import category-theory.adjunctions-large-precategories public
open import category-theory.anafunctors-categories public
open import category-theory.anafunctors-precategories public
open import category-theory.categories public
open import category-theory.coproducts-in-precategories public
open import category-theory.dependent-products-of-categories public
open import category-theory.dependent-products-of-precategories public
open import category-theory.discrete-categories public
open import category-theory.endomorphisms-in-categories public
open import category-theory.endomorphisms-in-precategories public
open import category-theory.epimorphisms-in-large-precategories public
open import category-theory.equivalences-of-categories public
open import category-theory.equivalences-of-large-precategories public
open import category-theory.equivalences-of-precategories public
open import category-theory.exponential-objects-in-precategories public
open import category-theory.function-categories public
open import category-theory.function-precategories public
open import category-theory.functors-categories public
open import category-theory.functors-large-precategories public
open import category-theory.functors-precategories public
open import category-theory.groupoids public
open import category-theory.homotopies-natural-transformations-large-precategories public
open import category-theory.initial-objects-large-categories public
open import category-theory.initial-objects-large-precategories public
open import category-theory.initial-objects-precategories public
open import category-theory.isomorphisms-in-categories public
open import category-theory.isomorphisms-in-large-categories public
open import category-theory.isomorphisms-in-large-precategories public
open import category-theory.isomorphisms-in-precategories public
open import category-theory.large-categories public
open import category-theory.large-precategories public
open import category-theory.monomorphisms-in-large-precategories public
open import category-theory.natural-isomorphisms-categories public
open import category-theory.natural-isomorphisms-large-precategories public
open import category-theory.natural-isomorphisms-precategories public
open import category-theory.natural-numbers-object-precategories public
open import category-theory.natural-transformations-categories public
open import category-theory.natural-transformations-large-precategories public
open import category-theory.natural-transformations-precategories public
open import category-theory.one-object-precategories public
open import category-theory.opposite-precategories public
open import category-theory.precategories public
open import category-theory.precategory-of-functors public
open import category-theory.pregroupoids public
open import category-theory.products-in-precategories public
open import category-theory.products-of-precategories public
open import category-theory.pullbacks-in-precategories public
open import category-theory.representable-functors-categories public
open import category-theory.representable-functors-precategories public
open import category-theory.sieves-in-categories public
open import category-theory.slice-precategories public
open import category-theory.terminal-objects-in-precategories public
open import category-theory.yoneda-lemma-categories public
open import category-theory.yoneda-lemma-precategories public

Recent changes

2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
2023-09-19. Egbert Rijke. Isomorphisms in large categories and large precategories (#791).
2023-09-18. Fredrik Bakke. Yoneda's lemma for categories (#783).
2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).