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).