3.1. Categories
A category involves a notion of objects, a notion of morphisms
between two such objects, a distinguished morphism from any object to
itself (the identity), the composition law of morphisms, and a few axioms.
In Mathlib, a category is thought as a structure on the type
of objects, and this structure involves a typeclass Category.
If we need to declare a category C as a variable, introduce
three objects X, Y, Z, two composable morphisms f from X to Y
and g from Y to Z, and consider the composition of f and g,
we proceed as follows:
variable {C : Type*} [Category* C]
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
example : X ⟶ Z := f ≫ g -- type `≫` as `\gg`
The arrow ⟶ that is used to denote the type of morphisms in a
category C is typed as \hom and it is different from the basic arrow →
(typed as \to) used for the type of nondependent functions between two types.
Note that the composition denoted here f ≫ g would usually be denoted "gf"
in the mathematical literature. Getting used to this notation is a
rite of passage. Beware that you may experience trouble going back to
the "gf" notation if you do too much formalization of category theory
in Lean.
The identity of an object X is denoted 𝟙 X (type 𝟙 as \b1):
example : f ≫ 𝟙 Y = f := C:Type u_1inst✝:Category.{v_1, u_1} CX:CY:CZ:Cf:X ⟶ Yg:Y ⟶ Z⊢ f ≫ 𝟙 Y = f All goals completed! 🐙
example : 𝟙 X ≫ f = f := C:Type u_1inst✝:Category.{v_1, u_1} CX:CY:CZ:Cf:X ⟶ Yg:Y ⟶ Z⊢ 𝟙 X ≫ f = f All goals completed! 🐙
About universes, we may observe that in this implementation,
the types of morphisms in a category C (with C : Type u) can be
considered as a dependent function C → C → Type v: for each X : C
and Y : C, the type X ⟶ Y of morphisms from X to Y
belongs to Type v for a certain universe v. If we need to be specific
about these two universe parameters u (for objects) and
v (for morphisms), we do:
universe v u -- `v` purposely appears first
variable {C : Type u} [Category.{v} C]
Otherwise, variable {C : Type*} [Category* C] would register
two fresh arbitrary universes. Declaring a u-small category
can be done as
variable {C : Type u} [SmallCategory C]
-- this is equivalent to `[Category.{u} C]`
A few examples of categories will be discussed in this phrasebook. One of
the basic examples is the category structure induced by a preorder. The
definitions homOfLE and leOfHom can be used in order to transform
an inequality h : a ≤ b into a morphism a ⟶ b in the category of
a preorder, and vice versa:
variable {α : Type*} [Preorder α]
#synth SmallCategory α
example {a b : α} (h : a ≤ b) : a ⟶ b := homOfLE h
example {a b : α} (f : a ⟶ b) : a ≤ b := leOfHom f
If C is a category, the opposite category is denoted Cᵒᵖ:
variable {C : Type*} [Category* C]
open Opposite
example (X : C) : Cᵒᵖ := op X
example (X : Cᵒᵖ) : C := X.unop
example {X Y : C} (f : X ⟶ Y) : op Y ⟶ op X := f.op
example {X Y : Cᵒᵖ} (f : X ⟶ Y) : Y.unop ⟶ X.unop := f.unop
The objects of Cᵒᵖ (and also the morphisms in Cᵒᵖ) are
implemented as a 1-field structure Opposite: we do not want
to enforce Cᵒᵖ = C, because it would create a confusion
about which Category instance on this type should be used.
Note that the type Cᵒᵖᵒᵖ is not equal to C either!