Maths in Lean : category theory #
category typeclass is defined in category_theory/default.lean.
It depends on the type of the objects, so for example we might write
category (Type u) if we're talking about a category whose objects are types (in universe
Functors (which are a structure, not a typeclass) are defined in category_theory/functor.lean, along with identity functors and functor composition.
Natural transformations, and their compositions, are defined in category_theory/natural_transformation.lean.
The category of functors and natural transformations between fixed categories
is defined in category_theory/functor_category.lean.
Cartesian products of categories, functors, and natural transformations appear in category_theory/products/basic.lean. (Product in the sense of limits will appear elsewhere soon!)
The category of types, and the hom pairing functor, are defined in category_theory/types.lean.
We use the
\hom) arrow to denote sets of morphisms, as in
X ⟶ Y.
This leaves the actual category implicit; it is inferred from the type of
Y by typeclass inference.
\b1) to denote identity morphisms, as in
\gg) to denote composition of morphisms, as in
f ≫ g, which means "
f followed by
You may prefer write composition in the usual convention, using
\circledcirc), as in
f ⊚ g which means "
g followed by
f". To do so you'll need to add this notation locally, via
local notation f ` ⊚ `:80 g:80 := category.comp g f
≅ for isomorphisms.
\func) to denote functors, as in
C ⥤ D for the type of functors from
⇒ is reserved in
logic.relator: https://github.com/leanprover-community/mathlib/blob/master/src/logic/relator.lean, so we can't use that here.)
F.obj X to denote the action of a functor on an object.
F.map f to denote the action of a functor on a morphism`.
Functor composition can be written as
F ⋙ G.
Natural transformations #
τ.app X for the components of a natural transformation.
Otherwise, we mostly use the notation for morphisms in any category:
F ⟶ G (
-->) to denote the type of natural transformations, between functors
F ≅ G (
\iso) to denote the type of natural isomorphisms.
For vertical composition of natural transformations we just use
≫. For horizontal composition,