A category \({\cal C}\) consists of:

1. objects \(\operatorname {Ob}({\cal C})\): \(O, X, Y, \dots \)
2. arrows \(\operatorname {Arr}({\cal C})\): \(f, g, h, \dots \), where for each arrow \(f\),
   • a pair of operations \(\operatorname {dom}\) and \(\operatorname {cod}\) assign a domain object \(X=\operatorname {dom}(f)\) and a codomain object \(Y=\operatorname {cod}(f)\) to \(f\),
   • thus f can be denoted by \[f : X \to Y\] or \[X \xrightarrow {f} Y\]
3. compositions: a composite arrow of any pair of arrows \(f\) and \(g\), denoted \(g \circ f\) or \( f \mathbin {\bullet } g \), makes the diagram commute (we say that \(f \mathbin {\bullet } g\) factors through \(Y\)),
4. a identity arrow for each object \(O\), denoted \(\mathit {1}_O : O \to O\)

1. associativity of composition: the diagram commutes,
2. identity law: the diagram commutes.

In literatures, composition of arrows in a category is most frequently denoted \(\circ \) or just by juxtaposition, i.e. for the diagram

But this is the opposite of the order of arrows in the diagram, so arguably a more natural way could be to denote the above as \(f ; g\) [kostecki2011introduction, 1.1], or as \(f \mathbin {⨟} g\) [fong2018seven, 3.6], or as \(f \mathbin {\bullet } g\) [nakahira2023diagrammatic, sec. 1.1].

We use \(f \mathbin {\bullet } g\) throughout this note, so it can always be understood as \(\xrightarrow {f}\xrightarrow {g}\). This way saves mental energy when reading commuting diagrams, pasting diagrams and string diagrams which we employ heavily.

A category C is called locally small iff for any of its objects \(X, Y\) , the collection of arrows from \(X\) to \(Y\) is a set, called a hom-set, denoted \[\operatorname {Hom}_{{\cal C}}(X, Y)\]

A category is called small iff the collection of all its arrows is a set.

\(\operatorname {Hom}\) in \(\operatorname {Hom}_{{\cal C}}(X, Y)\) is short for homomorphism, since an arrow in category theory is a morphism (i.e. an arrow), a generalization of homomorphism between algebraic structures.

This notation could be unnecessarily verbose, so when there is no confusion, we follow [leinster2016basic] and [zhang2021type] to simply write \(X,Y \in \operatorname {Ob}({\cal C})\) as \[X,Y \in {\cal C}\] and \(f \in \operatorname {Hom}_{{\cal C}}(X, Y)\) as \[f \in {\cal C}(X, Y)\]

In some other scenarios, when the category in question is clear (and it might be to too verbose to write out, e.g. a functor category), we omit the subscript of the category and write just \[\operatorname {Hom}(X, Y)\]

In general, collection \(\operatorname {Ob}({\cal C})\) and \(\operatorname {Arr}({\cal C})\) are not neccessarily sets, but classes. In that case, \(\operatorname {Hom}_{{\cal C}}(X, Y)\) is called a hom-class.

Later, we will also learn that \(\operatorname {Ob}\) and \(\operatorname {Arr}\) are representable functors.

A category is called finite iff it is small and it has only a finite number of objects and arrows.

A diagram in a category \({\cal C}\) is defined as a collection of objects and arrows that belong to the category \({\cal C}\) with specified operations \(\operatorname {dom}\) and \(\operatorname {cod}\).

A commuting diagram is defined as such diagram that any two arrows of this diagram which have the same domain and codomain are equal.

For example, that the diagram

It's also called a arrow diagram [nakahira2023diagrammatic, 1.1] when compared to a string diagram, as it represents arrows with \(\to \).

A string diagram represents categories as surfaces (2-dimensional), functors as wires (1-dimensional), natural transformations as blocks or just dots (0-dimensional).

String diagrams has the advantage of being able to represent objects, arrows, functors, and natural transformations from multiple categories, and their vertical and horizontal composition, and has various topologically plausible calculational rules for proofs.

Later, when we have learned about functors and natural transformations, we will see that, in string diagram for 1-category:

1. A category \({\cal C}\) is represented as a colored region:
2. Functors of type \(\mathbf {1} \to {\cal C}\) can be identified with objects of the category \({\cal C}\), where \(\mathbf {1}\) is the the terminal category, so an object \(X \in \operatorname {Ob}({\cal C})\) can be represented as:
3. An arrow \(f : X \to Y\) is then a natural transformation between two of these functors, represented as:

The general idea is that we try to use visually distinct letters for different concepts:

1. uppercase calligraphic letters \({\cal C}, {\cal D}, {\cal E}, {\cal J}, {\cal S}\) denote categories
   • \({\cal C}, {\cal D}, {\cal E}\) are prefered in concepts about one to three categories, since \({\cal C}\) is the first letter of "category"
   • \({\cal J}\) is used in concepts like diagram, and assumed to be small
   • \({\cal S}\) is used in concepts like subcategory, or sometimes in concepts about a small category
2. boldface uppercase Roman letters denote specific categories, e.g. \(\mathbf {Cat}, \mathbf {Set}, \mathbf {Grp}, \mathbf {Top}, \mathbf {1}\)
3. uppercase Roman letters \(X, Y, Z, W, O, E, V\) denote objects in categories
   • \(X, Y\) usually mean objects in \({\cal C}\) and \({\cal D}\), respectively
   • \(O\) denotes any object
   • \(E\) denotes the equalizer object
   • in limit-related concepts, \(\mathrm {-}\) denotes any object, \(V\) denotes the vertex
4. lowercase Roman letters \(f, g, h, i, k, l, r\) and sometimes the lowercase Roman letter of the corresponding codomain or domain object denote arrows
   • occationally, when two arrows are closely related, they are denoted by the same letter with different subscripts, e.g. \(g_1, g_2\)
   • as special cases, \(\iota , p, i\) denote the inclusion, projection and injection arrows
5. uppercase script letters \(\mathscr {F}, \mathscr {G}, \mathscr {H}, \mathscr {I}, \mathscr {K}, \mathscr {L}, \mathscr {R}\) denote functors
   • \(\mathscr {D}\) denotes a diagram functor
   • \(\mathscr {L}\) and \(\mathscr {R}\) denote the left and right adjoint functors in an adjunction, respectively
   • \(\mathscr {H}\) denotes the Yoneda embedding functors
   • as a special case, functors with the terminal category (i.e. constant object functors) as the domain are identified with the objects in the codomain category, thus are denoted like an object: \(X : \mathbf {1} \to {\cal C}, \mathrm {*} \mapsto X\)
   • \(\mathscr {I}\) is only used in the inclusion functor (note that this is letter "I")
   • we do not use \(\mathscr {J}\) and \(\mathscr {S}\) because they are visually ambiguous
6. lowercase Greek letters \(\alpha , \beta , \eta , \epsilon , \sigma \) denote natural transformations, their components are denoted by them with subscripts.

An arrow \(f : X \to Y\) is monic if the diagram

"Monic" is short for "monomorphism", which is a generalization of the concept of injective (one-to-one) functions between sets.

An arrow \(f : X \to Y\) is epic if the diagram

"Epic" is short for "epimorphism", which is a generalization of the concept of surjective (onto) functions between sets.

An arrow \(f : X \to Y\) is iso, or \(X\) and \(Y\) are isomorphic, denoted \(X \cong Y\), or \(X \xrightarrow {\sim } Y\), if the diagram

"Iso" is short for "isomorphism", which is a generalization of the concept of bijective (one-to-one and onto) functions.

Uniqueness of an arrow is denoted \(\exists ! f\) or simply \(!f\), and visualized as a dashed arrow in diagrams, and \(!\) is often omitted.

An iso arrow is always monic and epic. However, not every arrow which is monic and epic is also iso.

Proof. 

The diagram

commutes for the iso arrow \(f\), thus

• \(g = h\) i.e. \(f\) is monic,
• \(k = l\) i.e. \(f\) is epic.

An initial object in a category \({\cal C}\) is an object \(\mathrm {0} \in \operatorname {Ob}({\cal C})\) such that for any object \(X\) in \({\cal C}\), there exists a unique arrow \(\mathrm {0} \to X\). It's also called a universal object, or a free object.

A terminal object in a category C is an object \(\mathrm {1} \in \operatorname {Ob}({\cal C})\) such that for any object \(X\) in \({\cal C}\), there exists a unique arrow \(X \to \mathrm {1}\). It's also called a final object, or a bound object.

Diagramatically,

A null object is an object which is both terminal and initial, confusingly, it's also called a zero object.

All initial objects in a category are isomorphic.

All terminal objects in a category are isomorphic.

In other words, they are unique up to isomorphism, respectively.

Let \(X, S \in \operatorname {Ob}({\cal C})\).

An element or a generalized element of \(X\) at stage \(S\) (or, of shape \(S\)) is an arrow \(x : S \to X\) in \({\cal C}\), also denoted \(x \in _{S} X\).

An arrow \(1 \to X\) is called a global element of \(X\), a.k.a. a point of \(X\).

An arrow \(S \to X\), if \(S\) is not isomorphic to \(1\), is called the local element of \(X\) at stage \(S\).

An arrow \(\mathit {1}_X : X \to X\) is called the generic element of \(X\).

In an element \(x : S \to X\), the object \(S\) is called a stage in order to express the intuition that it is a "place of view" on \(X\). In the same sense, \(S\) is also called a domain of variation, and \(X\) a variable element.

Sometimes, the term shape is used instead [leinster2016basic, 4.1.25], intuitive examples are:

• when the object is a set, a generalized element of \(X\) of shape \(\mathbb N\) is a sequence in the set \(X\)
• when the object is a topological space, a generalized element of \(X\) of shape \(S^1\) is a loop

In the context of studying solutions to polynomial equations, we may also call it a \(S\)-valued point in \(X\), where \(S\) is the number set where the solution is taken, e.g. the real, complex, and \(\operatorname {Spec} \mathbb F_p\)-valued solutions.

Two monic arrows \(x\) and \(y\) which satisfy

The equivalence class of \(x\) is denoted as \([x]\), i.e., \([x]=\{y \mid x \sim y\}\).

A subobject of any object is defined as an equivalence class of monic arrows into it.

The class of subobjects of an object \(X\) is denoted as \[ \operatorname {Sub}(X):=\{[f] \mid \operatorname {cod}(f)=X \wedge f \text { is monic }\}. \]

\(\mathbf {Set}\), the category of sets, consists of objects which are sets, and arrows which are functions between them. The axioms of composition, associativity and identity hold due to standard properties of sets and functions.

\(\mathbf {Set}\) has the initial object \(\varnothing \), the empty set, and the terminal object, \(\{*\}\), the singleton set.

\(\mathbf {Set}\) doesn't have a null object.

Monic arrows in \(\mathbf {Set}\) are denoted by \(f: X \hookrightarrow Y\), interpreted as an inclusion map (see also inclusion function in nLab).

Given \(X : \mathbf {Set}\), the subobjects of \(X\) are in canonical one-to-one correspondence with the subsets of \(X\).

In

We denote by \(\mathbf {Cat}\) the category of small categories and functors between them.

A discrete category has no arrows apart from the identity arrow, i.e. it amounts to just a class of objects.

We can regard a set as a discrete category.

A terminal category, denoted \(\mathbf {1}\), has only one object, denoted \(\mathrm {*}\), and only the identity arrow, denoted \(\mathit {1}\).

1. (reversion of arrows) \[\operatorname {Ob}({\cal C}^{op}) = \operatorname {Ob}({\cal C})\] \[\operatorname {Arr}({\cal C}^{op}) \ni f: Y \to X \Longleftrightarrow \operatorname {Arr}({\cal C}) \ni f: X \to Y\]
2. (reversion of composition)

Given categories \({\cal C}\) and \({\cal D}\), there is a product category, denoted \({\cal C} \times {\cal D}\), in which

• an object is a pair \((X, Y)\)
• an arrow \((X, Y) \to \left (X', Y'\right )\) is a pair \((f, g)\)
• the composition is given by \[(f_1, g_1) \mathbin {\bullet } (f_2, g_2) = (f_1 \mathbin {\bullet } f_2, g_1 \mathbin {\bullet } g_2)\]
• the identity on \((X, Y)\), denoted \(\mathit {1}_{(X, Y)}\) is \((\mathit {1}_X, \mathit {1}_Y)\)

Let \({\cal C}\) be a category. A subcategory \({\cal S}\) of \({\cal C}\) consists of a subclass \(\operatorname {Ob}({\cal S})\) of \(\operatorname {Ob}({\cal C})\) together with, for each \(S, S' \in \operatorname {Ob}({\cal S})\), a subclass \({\cal S}\left (S, S'\right )\) of \({\cal C}\left (S, S'\right )\), such that \({\cal S}\) is closed under composition and identities.

It is a full subcategory if \({\cal S}\left (S, S'\right )={\cal C}\left (S, S'\right )\) for all \(S, S' \in \operatorname {Ob}({\cal S})\).

A (covariant) functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is given by the diagram

A functor \(\mathscr {F}\) is called a contravariant functor from \({\cal C}\) to \({\cal D}\), and denoted \(\mathscr {F} : {\cal C}^{op} \to {\cal D}\), if it obeys the definition given by the (covariant) functor for \({\cal C}\) replaced by \({\cal C}^{op}\), i.e. it's given by the diagram

For some expression \(E(X)\) containing \(X\), when we say \(E(X)\) is (covariant) functorial in \(X\), we mean that there exists a functor \(\mathscr {F}\) such that

Dually, we use the term contravariantly functorial in.

For simplicity, when there is no confusion, we use \(\bullet \) to represent corresponding objects, and omit the arrow names in the codomain of a functor, e.g.

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is full iff for any pair of objects \(X, Y\) in \({\cal C}\) the induced map \(F_{X, Y}: {\cal C}(X, Y) \to {\cal D}(\mathscr {F}(X), \mathscr {F}(Y))\) is surjective (onto). \(\mathscr {F}\) is faithful if this map is injective (one-to-one).

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is called to preserve a property \(\wp \) of an arrow iff for every \(f \in \operatorname {Arr}({\cal C})\) that has a property \(\wp \) it follows that \(\mathscr {F}(f) \in \operatorname {Arr}({\cal D})\) has this property. A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) is called to reflect a property \(\wp \) of an arrow iff for every \(\mathscr {F}(f) \in \operatorname {Arr}({\cal D})\) that has a property \(\wp \) it follows that \(f \in \operatorname {Arr}({\cal C})\) has this property.

Every inclusion functor is faithful.

Every functor preserves isomorphisms.

Every faithful functor reflects monomorphisms and epimorphisms.

Every full and faithful functor reflects isomorphisms.

The identity functor \(\mathit {1}_{{\cal C}}: {\cal C} \to {\cal C}\) (denoted also by \( 1_{{\cal C}}: {\cal C} \to {\cal C}\)), defined by \(\mathit {1}_{{\cal C}}(X)=X\) and \(\mathit {1}_{{\cal C}}(f)=f\) for every \(X \in \operatorname {Ob}({\cal C})\) and every \(f \in \operatorname {Arr}({\cal C})\).

The constant functor \(\Delta _O: {\cal C} \to {\cal D}\) which assigns a fixed \(O \in \mathrm {Ob}({\cal D})\) to any object of \({\cal C}\) and \(\mathit {1}_O\), the identity arrow on \(O\), to any arrows from \({\cal C}\) :

A functor from the terminal category \(\mathbf {1}\) to a category \({\cal C}\) simply picks out an object of \({\cal C}\), called a constant object functor (which is a constant functor), denoted \(\Delta _X : \mathbf {1} \to {\cal C}\) for some \(X \in \operatorname {Ob}({\cal C})\), or simly denoted by the object, e.g. \(X\).

As special cases, constant object functor for initial and terminal objects are denoted by \(\mathrm {0}\) and \(\mathrm {1}\), respectively.

A unique functor, is a functor from a category \({\cal C}\) to the terminal category \(\mathbf {1}\), uniquely determined by mapping all arrows in \({\cal C}\) to the identity arrow \(\mathit {1}_{\mathrm {*}}\) of the unique object \(\mathrm {*}\) in \(\mathbf {1}\).

This functor is often denoted by \(! : {\cal C} \to \mathbf {1}\).

Intuitively, the functor \(!\) acts to erase all information about the input.

Given a small category \({\cal J}\) and a category \({\cal C}\), the diagonal functor \[\Delta _{{\cal J}}: {\cal C} \to [{\cal J}, {\cal C}]\] maps each object \(X \in {\cal C}\) to the constant functor \(\Delta _{{\cal J}}(X): {\cal J} \to {\cal C}\), which in turn maps each object in \({\cal J}\) to \(X\), and all arrows in \({\cal J}\) to \(\mathit {1}_X\).

When \({\cal J}\) is clear in the context, we may write \(\Delta _{{\cal J}}(X)\) as \(\Delta _X\).

Particularly [kostecki2011introduction, 3.1, example 6], when \({\cal J}\) is a discrete category of two objects, \(\Delta : {\cal C} \to {\cal C} \times {\cal C}, \Delta (X)=(X, X)\) and \(\Delta (f)=(f, f)\) for \(f: X \to X^{\prime }\)

\(\Delta _{{\cal J}}(X)\) is the same as \(X \mathbin {\bullet } !\), thus [nakahira2023diagrammatic, eq. 2.12] \[\Delta _{{\cal J}} = - \mathbin {\bullet } !\]

The forgetful functor, which forgets some part of structure, however arrows, compositions and identities are preserved.

Whenever \({\cal S}\) is a subcategory of a category \({\cal C}\) , there is an inclusion functor \(\mathscr {I} : {\cal S} \hookrightarrow {\cal C}\) defined by \(\mathscr {I}(S) = S\) and \(\mathscr {I}( f ) = f\) , i.e. it sends objects and arrows of \({\cal S}\) into themselves in category \({\cal C}\). It is automatically faithful, and it is full iff S is a full subcategory.

Some other special functors are introduced in later sections in context, e.g. hom-functor, Yoneda embedding functors.

A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is a unique pair \((O , u)\) that makes the diagram

Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a unique pair \((O , u)\) that makes the diagram

We say universal arrows satisfy some universal property.

The term universal property is used to describe some property (usually some equality of some compositions, or a commuting diagram in general) that is satisfied for all (hence universal) relevant objects/arrows in the "world" (i.e. in the relevant categories), by a corresponding unique object/arrow.

It's usually spell out like this:

In a context where (usually a given diagram), for all (some objects/arrows), there exists a unique (object/arrow) such that (some property).

Diagramatically,

For clarity and brevity, usually the \(\forall \) clauses are specified outside the diagram, and the \(\exists !\) clause is expressed by dashed arrows. For more elaborate diagrams, see [freyd1976properties][fong2018seven][ochs2022missing].

For the diagram above, we also say that \(f\) uniquely factors through \(u\) along \(g\) [riehl2017category, 2.3.7].

A universal property is a property of some construction which boils down to (is manifestly equivalent to) the property that an associated object is an initial object of some (auxiliary) category [nlab2020univ].

Given categories and functors

A universal arrow from \(X \in {\cal D}\) to \(\mathscr {F} : {\cal C} \to {\cal D}\) is an initial object in the comma category \(X \downarrow \mathscr {F}\).

Conversely, a (co)universal arrow from \(\mathscr {F} : {\cal C} \to {\cal D}\) to \(X \in {\cal D}\) is a terminal object in the comma category \(\mathscr {F} \downarrow X\).

A pasting diagram represents categories as points (0-dimensional), arrows \(\to \) (1-dimensional), natural transformations as surfaces with level-2 arrows \(\Rightarrow \) (0-dimensional).

For example:

It's dual to a corresponding string diagram

In string diagrams,

1. A functor \(\mathscr {F} : {\cal C} \to {\cal D}\) can be represented as an edge, commonly referred to as a wire:
2. Functors compose from left to right:
3. A natural transformation \(\alpha : \mathscr {F} \to \mathscr {F}'\) can be represented as a dot on the wire from top to bottem (the opposite direction of [marsden2014category], but the same as [sterling2023models]), connecting the two functors :
4. Natural transformations (for the same pair of categories) compose vertically from top to bottem:
5. Natural transformations (from different pairs of categories) compose horizontally from left to right:
6. The two ways of composing natural transformations are related by the interchange law: i.e. \[(\alpha \mathbin {\bullet } \alpha ') \mathbin {\bullet } (\beta \mathbin {\bullet } \beta ') = (\alpha \mathbin {\bullet } \beta ) \mathbin {\bullet } (\alpha ' \mathbin {\bullet } \beta ')\]

7. The naturality in natural transformations is equivalent to the following equality:

   where \(X\) and \(X'\) are objects in \({\cal C}\), understood as functors from the terminal category \(\mathit {1}\) to \({\cal C}\).

   👉

   Since a string diagrams is composed from top to bottem, left to right, we can read

   as \[(X \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (\alpha _X) \mathbin {\bullet } (f \mathbin {\bullet } \mathscr {G})=(X' \mathbin {\bullet } \mathscr {G}) \quad {\large =} \quad (X \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (f \mathbin {\bullet } \mathscr {F}) \mathbin {\bullet } (\alpha '_X)=(X' \mathbin {\bullet } \mathscr {G})\] where each pair of parentheses corresponds to an overlay in the string diagram, or with the notation in the opposite direction that is more familiar to most: \[\mathscr {G}(f) \circ \alpha _X \circ \mathscr {F}(X) = \mathscr {G}(X') \quad {\large =} \quad \alpha '_X \circ \mathscr {F}(f) \circ \mathscr {F}(X) = \mathscr {G}(X')\] Note that we read the wire from \(\mathscr {F}\) to \(\mathscr {G}\) as \(\mathscr {F}\) before the natural transformation, but as \(\mathscr {G}\) after the transformation.

   Effectively naturality says that the natural transformation and function \(f\) “slide past each other”, and so we can draw them as two parallel wires to illustrate this.

The functor category from \({\cal C}\) to \({\cal D}\), denoted \([{\cal C}, {\cal D}]\) or \({\cal D}^{{\cal C}}\), is a category whose objects are functors from \({\cal C}\) to \({\cal D}\) and whose arrows are natural transformations between them, where composition is given by

One can think of a functor category \([{\cal C}, {\cal D}]\) or \({\cal D}^{{\cal C}}\) as a category of diagrams in \(D\) indexed (or labelled) by the objects from \({\cal C}\).

This particularly makes sense in a diagram.

A natural transformation \(\sigma : \mathscr {F} \to \mathscr {G}\) between functors \(\mathscr {F}: {\cal C} \to {\cal D}\) and \(\mathscr {G} : {\cal C} \to {\cal D}\) is called a natural isomorphism or a natural equivalence, denoted \(\sigma : \mathscr {F} \cong \mathscr {G}\), if each component \(\sigma _X : \mathscr {F}(X) \to \mathscr {G}(X)\) is an isomorphism in \({\cal D}\), i.e. \(\mathscr {F}(X) \underset {\sigma _X}{\cong } \mathscr {G}(X)\).

We call \(\mathscr {F}\) and \(\mathscr {G}\) naturally isomorphic to each other.

We also say that \(\mathscr {F}(X) \cong \mathscr {G}(X)\) naturally in \(X\) [leinster2016basic, 1.3.12].

Diagramatically,

A natural isomorphism between functors from categories \({\cal C}\) and \({\cal D}\) is an isomorphism in the functor category \([{\cal C}, {\cal D}]\).

The cateories \({\cal C}\) and \({\cal D}\) are called isomorphic, denoted \({\cal C} \cong {\cal D}\), iff there exists functors

The categories \({\cal C}\) and \({\cal D}\) are called equivalent, denoted \({\cal C} \simeq {\cal D}\), iff there exist functors

A category is a world of objects, all looking at one another. Each sees the world from a different viewpoint.

We may ask: what objects see? Fix an object, this can be described by the arrows from it, this corresponds to the covariantly representable functor.

We can also ask the dual question: how objects are seen? Fix an object, this can be described by the arrows into it, this corresponds to the contravariantly representable functor.

For every locally small category \({\cal C}\), the covariant hom-functor, denoted \[{\cal C}(X,-): {\cal C} \to \mathbf {Set} \] is given by

Conversely, the contravariant hom-functor, denoted \[{\cal C}(-,X): {\cal C}^{op} \to \mathbf {Set} \] is given by

Further, the hom-bifunctor, denoted \[{\cal C}(-,=): {\cal C}^{op} \times {\cal C} \to \mathbf {Set} \] defined as a contravariant hom-functor at first argument and as a covariant hom-functor at second argument.

We see \(-\) and \(=\) as placeholders for any object and its "associated arrow" (whose domain/codomain is the object, respectively) in the corresponding category. And we use boxes to mark the placeholder objects in diagrams.

Diagramatically [leinster2016basic, 4.1.22],

A set-valued functor \(\mathscr {F}: {\cal C} \to \mathbf {Set}\) is called covariantly representable if for some \(X \in {\cal C}\), \[\tau : \mathscr {F} \cong {\cal C}(X,-)\] where \(\cong \) denotes a natural isomorphism.

Conversely, a set-valued functor \(\mathscr {G} : {\cal C}^{op} \to \mathbf {Set}\) is called contravariantly representable if for some \(X \in {\cal C}\), \[\tau : \mathscr {G} \cong {\cal C}(-, X)\]

Such an object \(X\) is called a representing object for the functor \(\mathscr {F}\) or \(\mathscr {G}\), respectively.

The pair \((\tau , X)\) is called a representation of the functor \(\mathscr {F}\) (respectively, \(\mathscr {G}\) ).

A representation \((\tau , X)\) of a representable functor \(\mathscr {F}\) is a choice of an object \(X \in {\cal C}\) and an isomorphism \(\tau \) between the corresponding type of hom-functor and \(\mathscr {F}\).

Representable functors are sometimes just called representables. Only set-valued functors can be representable.

Let \({\cal C}\) be a locally small category. The covariant Yoneda embedding functor of \({\cal C}\) is the functor \[ \mathscr {H}^{\bullet }: {\cal C}^{op} \to [{\cal C}, \mathbf {Set}] \] defined on objects \(X\) by the covariant hom-functor on \(X\).

This functor embeds what every object in \({\cal C}\) sees the "world" of the category \({\cal C}\), i.e. arrows from each object.

Conversely, the (contravariant) Yoneda embedding functor of \({\cal C}\) is the functor \[ \mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}] \] defined on objects \(X\) by the contravariant hom-functor on \(X\).

This functor embeds how every object in \({\cal C}\) is "seen", i.e. arrows to each object.

\(\bullet \) is a placeholder for an object. \(\mathscr {H}^X\) and \(\mathscr {H}_X\) denote the corresponding Yoneda embedding functors applied to \(X\), and are called covariant/contravariant Yoneda functors, respectively.

Diagramatically [rosiak2022sheaf, def. 161]:

When one speaks of the Yoneda (embedding) functor without specifying covariant or contravariant, it means the contravariant one, because it's the one used in the Yoneda lemma.

Let \({\cal C}\) be a locally small category. Then \[ \operatorname {Nat}(\mathscr {H}_X, \mathscr {F}) \cong \mathscr {F}(X) \] naturally in \(X \in {\cal C}\) and \(\mathscr {F} \in \left [{\cal C}^{\mathrm {op}}, \mathbf {Set} \right ]\), where \(\mathscr {H}_X\) is the (contravariant) Yoneda embedding functor on \(X\), and Nat denotes all the natural transformations between the two functors.

Diagramatically, \(\operatorname {Nat}(\mathscr {H}_X, \mathscr {F})\) is

The Yoneda lemma can be regarded as saying:

To understand an object it suffices to understand all its relationships with other things.

This is similar to the seventeenth-century philosopher Spinoza's idea that what a body is (its “essence”) is inseparable from all the ways that the body can affect (causally influence) and be affected (causally influenced) by other bodies.

The idea of Yoneda is that we can be assured that if a robot wants to learn whether some object \(X\) is the same thing as object \(Y\), it will suffice for it learn whether \[{\cal C}(-, X) \cong {\cal C}(-, Y)\] or, dually, \[{\cal C}(X, -) \cong {\cal C}(Y, -)\] i.e. whether all the ways of probing \(X\) with objects of its environment amount to the same as all the ways of probing \(Y\) with objects of its environment.

The Yoneda embedding functor \(\mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}]\) is full and faithful.

Given a small category \({\cal C}\), there is a functor \(\operatorname {Ob} : \mathbf {Cat} \to \mathbf {Set}\) that sends \({\cal C}\) to its set of objects where \(\mathbf {Cat}\) is the category of small categories. Thus, \[ \mathscr {H}^{\mathrm {1}}({\cal C}) \cong \operatorname {Ob}({\cal C}) \] where \(\mathscr {H}\) is a Yoneda embedding functor.

This isomorphism is natural in \({\cal C}\); hence \(\operatorname {Ob} \cong \mathbf {Cat}(\mathrm {1}, -)\) where \(\mathbf {Cat}(\mathrm {1}, -)\) is a covariant hom-functor.

Functor \(\operatorname {Ob}\) is representable. Similarly, the functor \(\operatorname {Arr} : \mathbf {Cat} \to \mathbf {Set}\) sending a small category to its set of arrows is representable.

Let \({\cal C}\) be a category. A presheaf \(\mathscr {F}\) on \({\cal C}\) is a functor \({\cal C}^{op} \to \mathbf {Set}\).

It is called representable if \(\mathscr {F} \cong \mathscr {H}_X\) for some \(X\).

We'll use \(\mathscr {F}\) to denote a presheaf since sheaf in French is faisceau.

The Yoneda lemma says that for any \(X \in {\cal C}\) and presheaf \(\mathscr {F}\) on \({\cal C}\), a natural transformation \(\mathscr {H}_X \to \mathscr {F}\) is an element of \(\mathscr {F}(X)\) of shape \(\mathscr {H}_X\).

We may ask the question [chen2016infinitely, 68.6.4]:

What kind of presheaves are already "built in" to the category \({\cal C}\)?

The answer by the Yoneda lemma is, the Yoneda embedding \(\mathscr {H}_{\bullet }: {\cal C} \to [{\cal C}^{op}, \mathbf {Set}]\) embeds \({\cal C}\) into its own presheaf category.

In mathematics at large, the word "embedding" is used (sometimes informally) to mean a map \(i: X \to Y\) that makes \(X\) isomorphic to its image in \(Y\), i.e. \(X \cong i(X)\). [leinster2016basic, 1.3.19] tells us that in category theory, a full and faithful functor \(\mathscr {I}: X \to Y\) can reasonably be called an embedding, as it makes \(X\) equivalent to a full subcategory of \(Y\).

So, \({\cal C}\) is equivalent to the full subcategory of the presheaf category \([{\cal C}^{op}, \mathbf {Set}]\) whose objects are the representables.

The functor category of contravariant set-valued functors \([{\cal C}^{op}, \mathbf {Set}]\), called the category of presheaves or varying sets, the objects of which are contravariant functors \({\cal C}^{op} \to \) Set. It may be regarded as a category of diagrams in \(\mathbf {Set}\) indexed contravariantly by the objects of \({\cal C}\).

By definition, objects of \({\cal C}\) play the role of stages, marking the "positions" (in passive view) or "movements" (in active view) of the varying set \(\mathscr {F}: {\cal C}^{op} \to \mathbf {Set}\). For every \(X\) in \({\cal C}^{op}\), the set \(\mathscr {F}(X)\) is a set of elements of \(\mathscr {F}\) at stage \(X\).

An arrow \(f: Y \to X\) between two objects in \({\cal C}^{op}\) induces a transition arrow \(\mathscr {F}(f): \mathscr {F}(X) \to \mathscr {F}(Y)\) between the varying set \(\mathscr {F}\) at stage \(A\) and the varying set \(\mathscr {F}\) at stage \(B\).

Let \({\cal C}\) be a category and \({\cal J}\) a small category. A functor \(\mathscr {D} : {\cal J} \to {\cal C}\) is called a diagram in \({\cal C}\) of shape \({\cal J}\).

\({\cal J}\) is also called the indexing category of the diagram, and we say that \(\mathscr {D}\) is a diagram indexed by \({\cal J}\) [rosiak2022sheaf, example 35]. \(J\) is also called the template.

The diagram

For simplicity, we refer to a diagram of shape E by "a shape \(E(f, g)\)".

"E" in "shape E" stands for "equal", and the reason will unfold in the definition of equalizer.

A fork over a shape \(E(f, g)\) is the diagram

For simplicity, we refer to a fork by "a fork \((E, \iota )\) (over the shape \(E(f, g)\))".

We use grey arrows to represent the composition arrow in a fork. This convention is not from literatures and is subject to change.

An equalizer of a shape \(E(f, g)\) is a fork \((E, \iota )\) over it, such that, for any \((\mathrm {-}, d)\) over the fork, the diagram

For simplicity, we refer to the equalizer of a shape \(E(f, g)\) as \(\operatorname {Eq}(f, g)\), and \(\iota \) is the canonical inclusion.

We say that a category \({\cal C}\) has equalizers iff every shape E in \({\cal C}\) has an equalizer.

Equalizer in a category is a generalisation of a subset which consists of elements of a given set such that two given functions are equal on them, formally:

For any two arrows \(f, g: X \to Y\), their equalizing set \(E \subseteq X\) is defined as \[ E:=\{e \mid e \in X \wedge f(e)=g(e)\} \]

The diagram

For simplicity, we refer to a diagram of shape P by "a shape \(P(f, g)\)".

"P" in "shape P" may stand for "product/projection/pullback", and the reason will unfold in the definition of pullback.

A pullback of a shape \(P(f, g)\) is an object \(X \times _O Y\) in \({\cal C}\) together with arrows \(p_X\) and \(p_Y\), called projections, such that, for any object \(\mathrm {-}\) and arrows \(h\) and \(k\), the diagram

We say that a category \({\cal C}\) has pullbacks iff every shape \(P(f, g)\) in \({\cal C}\) has a pullback in \({\cal C}\).

A pullback is also called a fiber product.

The square

Pullbacks can be pasted together, i.e. for diagram

The diagram

For simplicity, we refer to a diagram of shape T by "a shape \(T(X, Y)\)" where \(X\) and \(Y\) are the 2 objects.

"T" in "shape T" stands for "two". Shape T is useful in the definition of binary product [kostecki2011introduction, 2.18].

We say that a category \({\cal C}\) has binary products iff every pair \(X, Y\) in \({\cal C}\) has a binary product \(X \times Y\) in \({\cal C}\).

When there is no confusion, we simply call bianry products products.

coshape, coequalizer, pushout (fiber coproduct), binary coproduct can be defined by reversing all arrows in the definitions of shape, equalizer, pullback (fiber product), binary product respectively.

The pushout equivalent of the fiber product object in pullback is the fiber coproduct object, denoted \(X +_{O} Y\), and the pushout equivalent of projections in pullback are injections, denoted \(i_X\) and \(i_Y\), respectively. The unique arrow of a pushout is denoted \([f, g]\).

The binary coproduct equivalent of the binary product object in binary product is the binary coproduct object, denoted \(X + Y\), and the binary coproduct equivalent of projections in binary product are injections, denoted \(i_X\) and \(i_Y\), respectively. The unique arrow of a binary coproduct is denoted \([f, g]\).

Diagramatically,

• Coshapes:
  • \(T\) =
  • \(E\) =
  • \(P\) =
• coequalizer:
• pushout (fiber coproduct):
• binary coproduct:

An arrow \(X \xrightarrow {f} Y\) is monic iff the square

The significance of this lemma is that whenever we prove a result about limits, a result about monics will follow.

An arrow \(X \xrightarrow {f} Y\) is epic iff the square

This is dual to Lemma [tt-003J].

In any category with binary products the objects \(X \times (Y \times Z)\) and \((X \times Y) \times Z\) are isomorphic. In any category with binary coproducts the objects \(X+(Y+Z)\) and \((X+Y)+Z\) are isomorphic.

This allows to consider \(n\)-fold products \(X_1 \times \dots \times X_n\) and \(n\)-fold coproducts \(X_1 + \dots + X_n\) of objects of a given category.

A category which has n-fold (co)products for any \(n \in \mathbb N\) is said to have finite (co)products.

Adjointness is about the relationships between categories. Representability is a property of set-valued functors. Limits are about what goes on inside a category.

Whenever you meet a method for taking some objects and arrows in a category and constructing a new object out of them, there is a good chance that you are looking at either a limit or a colimit.

Let \({\cal C}\) be a category, \({\cal J}\) a small category, and \(\mathscr {D} : {\cal J} \to {\cal C}\) a diagram in \({\cal C}\) of shape \({\cal J}\).

A cone on \(\mathscr {D}\) is an object \(V \in {\cal C}\) (the vertex of the cone) together with a family \[ \left (V \xrightarrow {\pi _J} \mathscr {D}(J)\right )_{J \in {\cal J}} \] of arrows in \({\cal C}\) such that for all arrows \(J \to J'\) in \({\cal J}\), the diagram

The family of arrows are components of a natural transformation \(\pi : \Delta _V \to \mathscr {D}\), i.e. from the constant functor ( which assigns the same object \(V\) to any object \(J_i\) in \({\cal J}\)) to diagram functor \(\mathscr {D}\).

For simplicity, we refer to a cone by "a cone \((V, \pi )\) on \(\mathscr {D}\)".

The cone for a diagram

A cone \((V, \pi )\) on \(\mathscr {D} : {\cal C} \to {\cal J}\) is called a limit of \(\mathscr {D}\), denoted \[\lim \mathscr {D}\] if the diagram

The arrows \(\pi _J\) are called the projections of the limit.

Other possible terms of limit are limiting cone, universal cone.

The basic types of diagrams are actually examples of limits:

1. binary product [kostecki2011introduction, 2.18]:
2. pullback (fiber product) [kostecki2011introduction, 2.12]:
3. equalizer [leinster2016basic, 5.1.11]:
4. the limit of \(\mathscr {D} : \mathbf {\emptyset } \to {\cal C} \), where \(\mathbf {\emptyset }\) is an empty category: i.e. the terminal object \(\mathrm {1}\) in \({\cal C}\). In particular, for \({\cal C} = \mathbf {Set}\) we have \[\mathrm {-} \xrightarrow {!} V = \lim \mathscr {D} = \{∗\} \]

A cocone and a colimit are defined by dualization, that is, by reversing the arrows in cone [leinster2016basic, 5.1.19] and limit [kostecki2011introduction, 4.10].

In another word, given \(\mathscr {D}^{op} : {\cal J}^{op} \to {\cal C}^{op}\), a cocone on \(\mathscr {D}\) is a cone on \(\mathscr {D}^{op}\), a colimit of \(\mathscr {D}\) is a limit of \(\mathscr {D}^{op}\) [leinster2016basic, 5.2.1].

The arrows \(\pi _J\) are called the coprojections of the colimit.

In the same say, one can and show that coequaliser, coproduct, pushout and initial object are examples of colimits.

If all products and equalizers exist, all limits exist.

Dually, if all coproducts and coequalizers exist, all colimits exist.

We say that a category \({\cal C}\) has (finite) limits or is (finitely) complete if every diagram \(\mathscr {D} : {\cal J} \to {\cal C}\), where \({\cal J}\) is a (finite) category, has a limit.

A category \({\cal C}\) is called left exact iff it is finitely complete.

Dually to Definition [tt-002F], when every diagram \(\mathscr {D} : {\cal J} \to {\cal C}\), where \({\cal J}\) is a (finite) category, has a colimit, it is said that the category \({\cal C}\) has (finite) colimits or is (finitely) cocomplete.

A category is called right exact iff it is finitely cocomplete.

A category \({\cal C}\) is (finitely) complete if it has a terminal object, equalizers and (finite) products, or if it has a terminal object and (finite) pullbacks.

Dually, a category \({\cal C}\) is (finitely) cocomplete if it has an initial object, coequalizers and (finite) coproducts, or if it has an initial object and (finite) pushouts.

If category \({\cal D}\) is complete and category \({\cal C}\) is small, then the functor category \({\cal D}^{{\cal C}}\) is complete.

Dually, if category \({\cal D}\) is cocomplete and category \({\cal C}\) is small, then the functor category \({\cal D}^{{\cal C}}\) is cocomplete.

Let \(P\) be a set. The properties

• (reflexivity) \(\forall p \in P, p \leq p\)
• (transitivity) \(\forall p, q, r \in P, p \leq q \wedge q \leq r \Rightarrow p \leq r\)

A partially ordered set (called a partial order, or a poset) is defined as a preorder \((P, \leq )\) for which

• (antisymmetry) \(\forall p \in P, p \leq q \wedge q \leq p \Rightarrow p=q\)

A total order (or a linear order) is a partial order \((P, \leq )\) for which

• (comparability) \(\forall p, q \in P, p \leq q \vee q \leq p\)

The category \(\mathbf {Preord}\) consists of objects which are preorders and of arrows which are orderpreserving functions.

The category \(\mathbf {Poset}\) consists of objects which are posets and of arrows which are order-preserving functions between posets, that is, the maps \(T: P \to P'\) such that \[ p \leq q \Rightarrow T(p) \leq T(q) \]

Any any preorder \((P, \leq )\) and poset \((P, \leq )\) can be considered as a category consisting of objects which are elements of a set \(P\) and arrows defined by \(p \to q \Longleftrightarrow p \leq q\).

A directed poset is a poset that is inhabited (nonempty) and for which every finite subset has an upper bound. Explicitly,

• (directedness) \(\forall x,y \in P, \exists z \in P, x \leq z \land y \leq z\)

An example of a preorder category which is not poset is:

An example of a poset category which is not a directed poset is [rosiak2022sheaf, example 3] :

An example that is a directed poset category but not a total order is:

A more complicated example of a directed poset category which is not a total order is [spivak2013category, example 3.4.1.3]:

One can see immediately that this is a preorder because length=0 paths give reflexivity and concatenation of paths gives transitivity. To see that it is a partial order we only note that there are no loops.

To see that it is a poset, we note that every pair of nodes from one side or both sides has the central node as an upper bound, thus satisfying directedness.

But this partial order is not a total order because there is no path (in either direction) between some nodes, thus violating comparability.

Let \({\cal J}\) be a directed poset and \(\mathscr {F} : {\cal J} \to {\cal C}\) be a contravariant functor. The limit of \(\mathscr {F}\) is called an inverse limit or projective limit, and is denoted \(\lim \limits _{\leftarrow {\cal J}} \mathscr {F}\) or simply \(\lim \limits _{\longleftarrow } \mathscr {F}\).

Let \({\cal J}\) be a directed poset and \(\mathscr {F}: {\cal J} \to {\cal C}\) be a contravariant functor. The colimit of \(\mathscr {F}\) is called a direct limit (some called directed limit) or inductive limit, and is denoted \(\lim \limits _{\to {\cal J}} \mathscr {F}\), or simply \(\lim \limits _{\longrightarrow } \mathscr {F}\).

This is dual to inverse limit.

A functor \(\mathscr {F}: {\cal C} \to {\cal D}\) preserves (all) limits and is called left exact iff it sends all limits in \({\cal C}\) into limits in \({\cal D}\).

Dually, a functor \(\mathscr {F}: {\cal C} \to {\cal D}\) preserves (all) colimits and is called right exact iff it sends all colimits in \({\cal C}\) into colimits in \({\cal D}\).

	Limit	Colimit
diagram
arrows through the vertex	into the diagram	out of the diagram
on (co)shape P	pullback	pushout
categories have finite ...	left exact	right exact
functors preserve all ...	left exact	right exact
on directed poset	inverse/projective limit \(\lim \limits _{\longleftarrow } \mathscr {F}\)	direct/inductive limit \(\lim \limits _{\longrightarrow } \mathscr {F}\)

One can see from the table that, in general, limits have the direction "back" "into" (where "back", "left", "inverse" are directional consistent), and colimits have the opposite: "forward" "out of".

This might help to memorize the directions in these concepts without disorientation.

Given functors

The components of the natural isomorphism \(\sigma \) are isomorphisms \[ \sigma _{XY} : {\cal D}(\mathscr {L}(X), Y) \cong {\cal C}(X, \mathscr {R}(Y)) \]

An adjunction \(\mathscr {L} \dashv \mathscr {R}\) means arrows \(\mathscr {L}(X) \to Y\) are essentially the same thing as arrows \(X \to \mathscr {R}(Y)\) for any \(X \in {\cal C}\) and \(Y \in {\cal D}\).

This means the diagram

The above can also be diagramatically denoted by transposition diagram \[ \begin {array}{ccccccc} X' & \xrightarrow {x} & X & \xrightarrow {\sigma _{X Y}(f)} & \mathscr {R}(Y) & \xrightarrow {\mathscr {R}(y)} & \mathscr {R}\left (Y'\right ) \\ \hline \mathscr {L}\left (X'\right ) & \xrightarrow {\mathscr {L}(x)} & \mathscr {L}(X) & \xrightarrow {f} & Y & \xrightarrow {y} & Y' \end {array} \] or simply, \[ \frac {X \to \mathscr {R}(Y) \quad ({\cal C})}{\mathscr {L}(X) \to Y \quad ({\cal D})} \]

An adjunction is a concept that describes the relationship between two functors that are weakly inverse to each other [nakahira2023diagrammatic, sec. 4].

By "weakly inverse", we don't mean that applying one after the other gives the identity functor, but in a sense similar to eroding (i.e. enhancing holes) and dilating (i.e. filling holes) an image, applying them in different order yeilds upper/lower "bounds" of the original image [rosiak2022sheaf, sec. 7.1].

Here we follow the string diagram style of [marsden2014category] and [sterling2023models], but with additional string diagram types inspired by [nakahira2023diagrammatic, eq. 3.1, 4.3].

1. The covariant hom-functor \({\cal C}(X, -)\), denoted \(-^X\), can be represented in string diagrams as where the dotted circle denotes any arrows with the domain \(X\) and codomain \(-\).
2. The contravariant hom-functor \({\cal C}(-, X)\), denoted \(X^-\), can be represented in a similar manner.
3. The hom-bifunctor \({\cal C}(-,=)\), also denoted \(=^-\), can be represented as where the dotted circle denotes any arrows with the domain \(-\) and codomain \(=\).
4. The natural isomorphism \[{\cal D}(\mathscr {L}(-), =) \cong {\cal C}(-, \mathscr {R}(=))\] in adjunction can be represented as

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), there exists \(f^{\sharp }\) and \(g^{\flat }\) such that the diagrams

\(f^{\sharp }\) is called the left transpose of \(f\). \(g^{\flat }\) is called the right transpose of \(g\).

Other possible terms are left/right adjunct of each other, and mates [nlab2023adjunct].

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), we may obtain two endofunctors \( \mathscr {L} \mathbin {\bullet } \mathscr {R} : {\cal C} \to {\cal C}\) and \( \mathscr {R} \mathbin {\bullet } \mathscr {L} : {\cal D} \to {\cal D}\) that commute the diagram

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), the natural transformation \[\eta : \mathit {1}_{{\cal C}} \to \mathscr {L} \mathbin {\bullet } \mathscr {R} \] is called the unit of the adjunction, and \[\epsilon : \mathscr {R} \mathbin {\bullet } \mathscr {L} \to \mathit {1}_{{\cal D}}\] is called the counit.

We call an arrow \[\eta _X: X \to (\mathscr {L} \mathbin {\bullet } \mathscr {R})(X)\] a unit over \(X\), and \[\epsilon _Y: (\mathscr {R} \mathbin {\bullet } \mathscr {L})(Y) \to Y\] a counit over \(Y\). They are components of the natural transformations \(\eta \) and \(\epsilon \), respectively.

Diagramatically, the diagrams

The unit \(\eta \) and counit \(\epsilon \) of an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\) are universal, i.e. the diagram

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), the diagrams

Note that \(\mathscr {L}\) in \(\epsilon _\mathscr {L}\) is a subscript, meaning \(\epsilon _\mathscr {L}: {\cal D} \to {\cal D}, \mathscr {L}(X) \mapsto \epsilon _{\mathscr {L}(X)}\) for \(X \in {\cal C}\). Similar for \(\eta _\mathscr {R}\).

Continuing from Notation [tt-001U], the triangle identities can be represented in string diagrams as follows, and called the snake identities (or zig-zag identities):

Following Notation [tt-001G], recall that a string diagram is composed from top to bottem, left to right, we can read the left snake

Given an adjunction

In string diagrams, Lemma [tt-001Y] can be represented as:

The string diagrams in Lemma [tt-0030] and Notation [tt-0033] are topologically plausible equations, i.e. the equality can be obtained by simply pulling the string straight.

The natural transformation \(\sigma _{XY}\) and \(\tau _{XY}\) that are the components of the natural isomorphism in the adjunction \(\mathscr {L} \dashv \mathscr {R} : {\cal C} \rightleftarrows {\cal D}\) are related to the unit and counit of the adjunction: \[\begin {aligned} \sigma _{XY}(f) & = \eta _X \mathbin {\bullet } \mathscr {R}(f^{\sharp })\\ \tau _{XY}(g) & = \mathscr {L}(g^{\flat }) \mathbin {\bullet } \epsilon _Y \end {aligned} \] and they are reverse of each other \[\sigma _{XY} = \tau _{YX}^{-1}\]

A left or right adjoint, if it exists, is unique up to natural isomorphism.

Given categories and functors

Given categories and functors

1. the adjunction \(\mathscr {L} \dashv \mathscr {R}\)

2. natural transformations \(\eta : \mathit {1}_{{\cal C}} \to \mathscr {L} \mathbin {\bullet } \mathscr {R}\) such that \(\eta _X\) is initial in the comma category \(X \Rightarrow \mathscr {R}\) for every \(X \in {\cal C}\)

   Diagramatically,

   where the functor \(X\) is the constant object functor.

In this section, we will discuss the interactions between

• (co)limits
• adjunctions
• representables

Given an adjunction \(\mathscr {L} \dashv \mathscr {R}: {\cal C} \rightleftarrows {\cal D}\), \(\mathscr {L}\) preserves colimits, and \(\mathscr {R}\) preserves limits.

Explictly, given \(\mathscr {D}: {\cal J} \to {\cal C}\), we have \[(\operatorname {colim} \mathscr {D}) \mathbin {\bullet } \mathscr {L} \cong \operatorname {colim}(\mathscr {D} \mathbin {\bullet } \mathscr {L})\] and given \(\mathscr {D}': {\cal J} \to {\cal D}\), we have \[(\lim \mathscr {D}') \mathbin {\bullet } \mathscr {R} \cong \lim (\mathscr {D}' \mathbin {\bullet } \mathscr {R})\]

Let \({\cal C}\) be a locally small category and \(\mathscr {F} : {\cal C}^{op} \to \mathbf {Set}\). Then a representation of \(\mathscr {F}\) consists of a pair \((X, u)\) such that the diagram

Pairs \((Y, y)\) with \(Y \in {\cal C}\) and \(y \in \mathscr {F}(Y)\) in Corollary [tt-0035] are sometimes called elements of the presheaf \(\mathscr {F}\).

Indeed, Lemma [tt-002N] (Yoneda) tells us that \(y\) amounts to a generalized element of \(\mathscr {F}\) of shape \(\mathscr {H}_Y\).

An element \(u\) satisfying condition in Corollary [tt-0035] is sometimes called a universal element of \(\mathscr {F}\). So, Corollary [tt-0035] says that a representation of a presheaf \(\mathscr {F}\) amounts to a universal element of \(\mathscr {F}\).

Any set-valued functor with a left adjoint is representable.

Now, given a diagram \(\mathscr {D}: {\cal J} \to {\cal C}\) and an object \(V \in {\cal C}\), a cone on \(\mathscr {D}\) with vertex \(V\) is simply a natural transformation from the diagonal functor \(\Delta _V\) to the diagram \(\mathscr {D}\).

Writing \(\operatorname {Cone}(V, \mathscr {D})\) for the set of cones on \(\mathscr {D}\) with vertex \(V\), we therefore have \[ \operatorname {Cone}(V, \mathscr {D})=[{\cal J}, {\cal C}] (\Delta _V, \mathscr {D}) . \]

Thus, \(\operatorname {Cone}(V, \mathscr {D})\) is functorial in \(V\) (contravariantly) and \(\mathscr {D}\) (covariantly).

Let \({\cal J}\) be a small category, \({\cal C}\) a category, and \(\mathscr {D}: {\cal J} \to {\cal C}\) a diagram. Then there is a one-to-one correspondence between

• limit cones on \(\mathscr {D}\)
• representations of the natural transformation Cone

Briefly put: a limit \((V, \pi )\) of \(\mathscr {D}\) is a representation of \([{\cal J}, {\cal C}] (\Delta _{-}, \mathscr {D})\).

Diagramatically,

It implies that \[\operatorname {Cone}(\mathrm {-}, \mathscr {D}) \cong {\cal C}\left (\mathrm {-}, \lim \limits _{\leftarrow {\cal J}} \mathscr {D} \right )\] for any \(\mathrm {-} \in {\cal C}\).

Let \(\mathscr {A}\) be a locally small category and \(X \in {\cal C}\). Then \({\cal C}(X,-): {\cal C} \to \mathbf {Set}\) preserves limits.

Let \({\cal I}\) and \({\cal J}\) be small categories. Let \({\cal C}\) be a locally small category with limits of shape \({\cal I}\) and of shape \({\cal J}\).

Define \[\begin {array}{llll} \mathscr {D}^{\bullet }: & {\cal I} & \to & {[{\cal J}, {\cal C}]} \\ & I & \mapsto & \mathscr {D}(I,-) \end {array}\] and \[\begin {array}{rrrr} \mathscr {D}_{\bullet }: & {\cal J} & \to & {[{\cal I}, {\cal C}]} \\ & J & \mapsto & \mathscr {D}(-, J) \end {array}\]

Then for all \(\mathscr {D}: {\cal I} \times {\cal J} \to {\cal C}\), we have \[ \lim _{\leftarrow {\cal J}} \lim _{\leftarrow {\cal I}} \mathscr {D}^{\bullet } \cong \lim _{\leftarrow {\cal I} {\cal J}} \mathscr {D} \cong \lim _{\leftarrow {\cal I} \leftarrow {\cal J}} \mathscr {D}_{\bullet } \] and all these limits exist. In particular, \({\cal C}\) has limits of shape \({\cal I} \times {\cal J}\).

Dual to Lemma [tt-0047], colimits commute with colimits.

Limits do not in general commute with colimits.

Some special cases where they do:

• filtered colimits commute with finite limits [stacks2017stacks, 002W].

Initial and terminal objects can be described as adjoints. Let \({\cal C}\) be a category. There exist the unique functor \(! : {\cal C} \to \mathbf {1}\), and a constant object functor \(X : 1 \to {\cal C}\) for each object \(X\).

A left adjoint to \(!\) is exactly an initial object of \({\cal C}\): \[ \mathrm {0} \dashv \ ! : \mathbf {1} \rightleftarrows {\cal C} \]

Similarly, a right adjoint to \(!\) is exactly a terminal object of \({\cal C}\): \[ ! \dashv \mathrm {1} : {\cal C} \rightleftarrows \mathbf {1} \]

(Co)limits can be phrased entirely in terms of adjunctions:

The advantages of this adjunction perspective is that the (co)limit of every \({\cal J}\)-shaped diagram in \({\cal C}\) can be defined all at once.

Let \({\cal S}\) be a small category, \({\cal C}\) a locally small category. For each \(X \in {\cal S}\), there is a functor \[ \begin {array}{lccc} \operatorname {ev}_X: & [{\cal S}, {\cal C}] & \to & {\cal C} \\ & \mathscr {F} & \mapsto & \mathscr {F}(X) \end {array} \] called evaluation at \(X\).

Given a diagram \(\mathscr {D}: {\cal J} \to [{\cal S}, {\cal C}]\), we have for each \(X \in {\cal S}\) a functor \[ \begin {array}{lccc} \mathscr {D} \mathbin {\bullet } \operatorname {ev}_X : & {\cal J} & \to & {\cal C} \\ & J & \mapsto & \mathscr {D}(J)(X) \end {array} \]

We write \(\mathscr {D} \mathbin {\bullet } \operatorname {ev}_X\) as \(\mathscr {D}(-)(X)\).

If \({\cal C}\) is a category with binary products, we can define for every \(X\) the cartesian product functor \(X \times (-)\) : \({\cal C} \rightarrow {\cal C}\), with the following action: \[ \begin {aligned} & (X \times (-))(Y)=X \times Y \\ & (X \times (-))(f)=\operatorname {id}_X \times f \end {aligned} \]

If for \(X \in {\cal C}\), a cartesian product functor \(X \times (-)\) has a right adjoint, it is called an exponential or the exponential object, denoted \((-)^X\).

Explicitly, \(X \times (-) \dashv (-)^X\) means there is a natural isomorphism of bifunctors \(\operatorname {Hom}(X \times (-),-) \cong \operatorname {Hom}(-, (-)^X)\), i.e. for any arrow \(f: X \times Y \to Z\) there is a unique arrow \(f^b: Y \to Z^X\), which is the transpose of the adjunction, called exponential transpose.

The arrow \(\operatorname {ev} : X \times (-)^X \to (-)\) is called the evaluation arrow of the exponential, and is the counit of the adjunction.

Diagramatically, the diagram

We say that category \({\cal C}\) has exponentials if for any \(X \in {\cal C}\), there exists an exponential \((-)^X\).

A category \({\cal C}\) is called cartesian closed iff \({\cal C}\) has exponentials and has finite products.

The power object \(P(X)\) of an object \(X\) in a cartesian closed category \({\cal C}\) with subobject classifier \(\Omega \) is defined as the exponential object \(\Omega ^X\).

If \(\Omega ^X\) exists for any \(X\) in \({\cal C}\), we say that \({\cal C}\) has power objects.

1. \(\mathrm {0} \times X \cong \mathrm {0}\) if \(\mathrm {0}\) exists in \({\cal C}\)
2. \(1 \times X \cong X\)
3. \(X^{\mathrm {0}} \cong \mathrm {1}\) if \(\mathrm {0}\) exists in \({\cal C}\)
4. \(X^1 \cong X\)
5. \(\mathrm {1}^X \cong 1\)
6. \(X \times Y \cong Y \times X\)
7. \((X \times Y) \times Z \cong X \times (Y \times Z)\)
8. \(Y^X \times Z^X \cong (Y \times Z)^X\)
9. \(Z^{X \times Y} \cong \left (Z^X\right )^Y\)
10. \(X+Y \cong Y+X\)
11. \((X+Y)+Z \cong X+(Y+Z)\)
12. \(Z^X \times Z^Y \cong Z^{X+Y}\) if \({\cal C}\) has binary coproducts
13. \((X \times Y)+(X \times Z) \cong X \times (Y+Z)\) if \({\cal C}\) has binary coproducts

Let \({\cal C}\) be a category and \(\mathscr {X} : {\cal C}^{op} \to \mathbf {Set}\) a presheaf on \({\cal C}\). The category of elements \({\cal E}(\mathscr {X})\) of \(\mathscr {X}\) is the category in which:

There is a projection functor \(\mathscr {P}: \mathbf {E}(\mathscr {X}) \rightarrow {\cal C}\) defined by \(\mathscr {P}(X, x) = X\) and \(\mathscr {P}(f) = f\).

The Yoneda lemma implies that for a presheaf \(\mathscr {X}\), the generalized elements of \(\mathscr {X}\) of representable shape correspond to objects of the category of elements.

Let \({\cal C}\) be a small category and \(\mathscr {X}\) a presheaf on \({\cal C}\). Then \(\mathscr {X}\) is the colimit of the diagram \[ {\cal E}(\mathscr {X}) \xrightarrow {\mathscr {P}} \mathbf {{\cal C}} \xrightarrow {H_{\bullet }}\left [\mathbf {{\cal C}}^{op}, \text { Set }\right ] \] in \(\left [\mathbf {{\cal C}}^{op}, \mathbf {Set} \right ]\), i.e. \[\mathscr {X} \cong \lim \limits _{\rightarrow {\cal E}(\mathscr {X})}\left (\mathscr {P} \mathbin {\bullet } H_{\bullet } \right )\] where \({\cal E}(\mathscr {X})\) is the category of elements, \(\mathscr {P}\) the projection functor in it, and \(H_{\bullet }\) the (contravariant) Yoneda embedding.

This theorem states that every presheaf is a colimit of representables in a canonical way. It is secretly dual to the Yoneda lemma. This becomes apparent if one expresses both in suitably lofty categorical language (that of ends, or that of bimodules).

A subobject classifier is an object \(\Omega \) in \({\cal C}\), together with an arrow \(\top : \mathbf {1} \to \Omega \), called the true arrow, such that for each monic arrow \(m: Y \mapsto X\) there is a unique arrow \(\chi : X \to \Omega \), called the characteristic arrow of \(m\) (or of \(Y\)), such that the diagram

\(\Omega \) is also called a generalized truth-value object.

The arrow \((! \mathbin {\bullet } T) : Y \stackrel {!}{\to } \mathbf {1} \rightarrowtail \Omega \) is often denoted as \(\top _Y: Y \to \Omega \).

In any category \({\cal C}\) with a subobject classifier \(\Omega \), \[ \operatorname {Sub}(X) \cong {\cal C}(X, \Omega ) \] i.e. the class of subobjects of an object \(X\) in \({\cal C}\) is isomorphic to the class of arrows from \(X\) to \(\Omega \).

The contravariant power object functor \(\mathscr {P}: {\cal C}^{o p} \to {\cal C}\), given by \[\mathscr {P}: X \mapsto \Omega ^X\] for \(X \in \mathrm {Ob}({\cal C})\) and such that \(\mathscr {P}(f): \Omega ^Y \mapsto \Omega ^X\) for \(f: X \to Y\) in \({\cal C}\) is given by \[\mathscr {P}(f)(Y)=\{x \in X \mid f(x) \in Y\}\]

When power object is defined for cartesian closed categories, we have \[ \frac {X \times Y \to \Omega }{Y \to \Omega ^X} \] thus for every category with power objects \[ \operatorname {Hom}(X \times Y, \Omega ) \cong \operatorname {Hom}\left (Y, \Omega ^X\right ) \] This equation, together with Lemma [tt-004K] written in the form \(\operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(X \times Y, \Omega )\), gives the isomorphism \[ \operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(Y, \mathscr {P}(X)) \]

In this document, we unify the informal mathematical language for a definition to:

Let \(X\) be a concept \(X\).

A concept \(Z\) is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

1. \(Z\) is a concept \(Y\) over \(X\) under op .
2. formula for all elements in \(Z\) ( property ).
3. for each element in concept \(X\), there exists element such that formula for all elements in concept \(Z\).
4. op is called op name, for all elements in \(Z\), we have
   1. formula
   2. formula
   ( property ).

By default, \(X\) is a set, op is a binary operation on \(X\).

A group is a pair \((G, *)\), satisfying:

1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
2. there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
3. for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

\(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

A monoid is a pair \((R, *)\), satisfying:

1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
2. there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)
i.e. \(1\) is the multiplicative identity (neutral element).

A ring is a triple \((R, +, *)\), satisfying:

1. \(R\) is a commutative group under \(+\).
2. \(R\) is a monoid under \(*\).
3. for all \(a, b, c \in R\), we have
   1. \(a * (b + c) = a * b + a * c\)
   2. \((a + b) * c = a * c + b * c\)
   (left and right distributivity over \(+\)).

In applications to Clifford algebras \(R\) will be always assumed to be commutative.

A division ring is a ring \((R, +, *)\), satisfying:

1. \(R\) contains at least 2 elements.
2. for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that
\[ a * a^{-1} = a^{-1} * a = 1 \]

Let \(R\) be a commutative ring with identity \(1_R\). A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

1. \(M\) is an abelian group under \(+\).
2. \(\bullet : R \to M \to M\) is called scalar multiplication, acting on the left. For every \(a, b \in R\), \(x, y \in M\), we have
   1. \(a \bullet (x + y) = a \bullet x + a \bullet y\)
   2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
   3. \(a \bullet (b \bullet x)=(a * b) \bullet x\)
   4. \(1_R \bullet x = x\)

The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).

Let \((\alpha , +_\alpha , *_\alpha )\) and \((\beta , +_\beta , *_\beta )\) be rings. A ring homomorphism from \(\alpha \) to \(\beta \) is a map \(\mathit {1} : \alpha \to _{+*} \beta \) such that

1. \(\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
2. \(\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
3. \(\mathit {1}(1_{\alpha }) = 1_{\beta }\).

Fix the algebraic structures and the homomorphisms under consideration. An Isomorphism \(\phi :A\to B\) is an iso: a homomorphism admitting an inverse homomorphism \(\phi ^{-1}:B\to A\), so that \(\phi ^{-1}\circ \phi =\operatorname {id}_A\) and \(\phi \circ \phi ^{-1}=\operatorname {id}_B\). We write \(A\cong B\) when such an isomorphism exists. This is the invertible-morphism definition of [stacks2017stacks, Definition 4.2.4 and the following paragraph, Tag 0013].

An Endomorphism of \(A\) is a homomorphism \(\phi :A\to A\). The set of all such homomorphisms is denoted \(\operatorname {End}(A)\). Thus an individual endomorphism satisfies \(\phi \in \operatorname {End}(A)\).

An Automorphism of \(A\) is an endomorphism that is an isomorphism. The set of all automorphisms is denoted \(\operatorname {Aut}(A)\). These notations always refer to the chosen kind of homomorphism; for modules over \(R\), the notation \(\operatorname {End}_R(M)\) specifies \(R\)-linear maps.

Let \(R\) be a commutative ring with identity. An algebra \(A\) over \(R\) is an associative ring with identity, equipped with a ring homomorphism \(\mathit {1} : R \to _{+*} A\) and a scalar multiplication \(\bullet : R \to A \to A\), such that for every \(r \in R\) and \(x \in A\), \[ \mathit {1}(r) * x = x * \mathit {1}(r), \qquad r \bullet x = \mathit {1}(r) * x. \] The ring homomorphism preserves the identity; multiplication in \(A\) need not be commutative.

This is the central-map convention of [stacks2017stacks, Section 22.2, Tag 09JF]. It is equivalent to the module formulation in [jadczyk2019notes, Definition 1.6, p. 4]; see the comparison.

Following literatures, for \(r \in R\), usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted, while they are written as a call to algebraMap _ _ r in \(\textsf {Mathlib}\), which is defined to be Algebra.toRingHom r.

For a commutative ring \(R\), the algebra structure is equivalently an \(R\)-module structure on an associative ring \(A\) with identity, with the same addition, such that \[ r \bullet (x * y) = (r \bullet x) * y = x * (r \bullet y) \qquad (r \in R,\ x,y \in A). \] This is the formulation of [jadczyk2019notes, Definition 1.6, p. 4]. Both formulations require associativity and an identity.

The corresponding Mathlib constructions are Algebra.toModule and Algebra.ofModule. Mathlib also permits semirings; under the ring hypotheses here, the two formulations describe the same structures.

What's simply called algebra is actually associative algebra with identity, a.k.a. associative unital algebra. See the red herring principle for more about such phenomenon for naming, particularly the example of (possibly) nonassociative algebra.

Let \(A\) and \(B\) be \(R\)-algebras. \(\mathit {1}_A\) and \(\mathit {1}_B\) are ring homomorphisms from \(R\) to \(A\) and \(B\), respectively. A algebra homomorphism from \(A\) to \(B\) is a map \(f : \alpha \to _{a} \beta \) such that

1. \(f\) is a ring homomorphism
2. \(f(\mathit {1}_{A}(r)) = \mathit {1}_{B}(r)\) for each \(r \in R\)

Let \(R\) be a non-commutative ring, \(r\) an arbitrary equivalence relation on \(R\). The ring quotient of \(R\) by \(r\) is the quotient of \(R\) by the strengthen equivalence relation of \(r\) such that for all \(a, b, c\) in \(R\):

1. \(a + c \sim b + c\) if \(a \sim b\)
2. \(a * c \sim b * c\) if \(a \sim b\)
3. \(a * b \sim a * c\) if \(b \sim c\)

As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.

Let \(X\) be an arbitrary set. An free \(R\)-algebra on \(X\) (or "generated by \(X\)"), named \(A\), is the ring quotient of the following inductively constructed set \(A_{\mathtt {pre}}\)

1. for all \(x\) in \(X\), there exists a map \(X \to A_{\mathtt {pre}}\).
2. for all \(r\) in \(R\), there exists a map \(R \to A_{\mathtt {pre}}\).
3. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a + b\) is in \(A_{\mathtt {pre}}\).
4. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a * b\) is in \(A_{\mathtt {pre}}\).

1. there exists a ring homomorphism from \(R\) to \(A_{\mathtt {pre}}\), denoted \(R \to _{+*} A_{\mathtt {pre}}\).
2. \(A\) is a commutative group under \(+\).
3. \(A\) is a monoid under \(*\).
4. left and right distributivity under \(*\) over \(+\).
5. \(0 * a \sim a * 0 \sim 0\).
6. for all \(a, b, c\) in \(A\), if \(a \sim b\), we have
   1. \(a + c \sim b + c\)
   2. \(c + a \sim c + b\)
   3. \(a * c \sim b * c\)
   4. \(c * a \sim c * b\)
   (compatibility with the ring operations \(+\) and \(*\))

Similar to Remark [ca-0019], what we defined here is the free (associative, unital) \(R\)-algebra on \(X\), it can be denoted \(R\langle X \rangle \), expressing that it's freely generated by \(R\) and \(X\), where \(X\) is the set of generators.

Let \(R, S\) be rings, \(M\) an \(R\)-module, \(N\) an \(S\)-module. A linear map from \(M\) to \(N\) is a function \(f : M \to _{l} N\) over a ring homomorphism \(\sigma : R \to _{+*} S\), satisfying:

1. \(f(x + y) = f(x) + f(y)\) for all \(x, y \in M\).
2. \(f(r \bullet x) = \sigma (r) \bullet f(x)\) for all \(r \in R\), \(x \in M\).

Let \(R\) be a commutative ring and let \(M,M'\) be \(R\)-modules. The set of all \(R\)-linear maps \(M\to M'\) is denoted \[ \operatorname {Lin}_R(M,M')=\operatorname {Hom}_R(M,M'). \] Here linear map means that the scalar homomorphism is \(\sigma =\operatorname {id}_R\). For this notation and scalar convention, see [stacks2017stacks, Section 10.10, Tag 0581].

For \(M'=M\), write \[ \operatorname {Lin}_R(M)=\operatorname {End}_R(M). \] This is the set of linear endomorphisms of \(M\); its elements are the individual endomorphisms. When the coefficient ring is understood, we omit \(R\) and write \(\operatorname {Lin}(M,M')\) and \(\operatorname {Lin}(M)\).

Let \(A\) be a free \(R\)-algebra generated by module \(M\), let \(\iota : M \to A\) denote the map from \(M\) to \(A\). An tensor algebra over \(M\) (or "of \(M\)") \(T\) is the ring quotient of the free \(R\)-algebra generated by \(M\), by the equivalence relation satisfying:

1. for all \(a, b\) in \(M\), \(\iota (a + b) \sim \iota (a) + \iota (b)\).
2. for all \(r\) in \(R\), \(a\) in \(M\), \(\iota (r \bullet a) \sim r * \iota (a)\).

The definition above is equivalent to the following definition in literature (e.g. [jadczyk2019notes, 1.7]):

Let \(M\) be a module over \(R\). An algebra \(T\) is called a tensor algebra over \(M\) (or "of \(M\)") if it satisfies the following universal properties:

1. \(T\) is an algebra containing \(M\) as a submodule, and it is generated by \(M\),
2. Every linear mapping \(\lambda \) of \(M\) into an algebra \(A\) over \(R\), can be extended to
a homomorphism \(\theta \) of \(T\) into \(A\).

Let \(R\) be a ring, \(M\) an \(R\)-module.

An bilinear form \(B\) over \(M\) is a map \(B : M \to M \to R\), satisfying:

1. \( B(x + y, z) = B(x, z) +B(y, z) \)
2. \( B(x, y + z) = B(x, y) +B(x, z) \)
3. \( B(a \bullet x, y) = a * B(x, y)\)
4. \( B(x, a \bullet y) = a * B(x, y)\)

Let \(R\) be a commutative ring, \(M\) a \(R\)-module.

An quadratic form \(Q\) over \(M\) is a map \(Q : M \to R\), satisfying:

1. \( Q(a \bullet x) = a * a * Q(x)\) for all \(a \in R, x \in M\).
2. there exists a companion bilinear form \(B : M \to M \to R\), such that \(Q(x + y) = Q(x) + Q(y) + B(x, y)\)

In [jadczyk2019notes], the bilinear form is denoted \(\Phi \), and called the polar form associated with the quadratic form \(Q\), or simply the polar form of \(Q\).

This notion generalizes to commutative semirings using the approach in [izhakian2016supertropical].

Let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

Let \(\iota : M \to _{l[R]} T(M)\) be the canonical \(R\)-linear map for the tensor algebra \(T(M)\).

Let \(\mathit {1} : R \to _{+*} T(M)\) be the canonical map from \(R\) to \(T(M)\), as a ring homomorphism.

A Clifford algebra over \(Q\), denoted \(\mathcal {C}\kern -2pt\ell (Q)\), is the ring quotient of the tensor algebra \(T(M)\) by the equivalence relation satisfying \(\iota (m)^2 \sim \mathit {1}(Q(m))\) for all \(m \in M\).

The natural quotient map is denoted \(\pi : T(M) \to \mathcal {C}\kern -2pt\ell (Q)\) in some literatures, or \(\pi _\Phi \)/\(\pi _Q\) to emphasize the bilinear form \(\Phi \) or the quadratic form \(Q\), respectively.

In literatures, \(M\) is often written \(V\), and the quotient is taken by the two-sided ideal \(I_Q\) generated from the set \(\{ v \otimes v - Q(v) \vert v \in V \}\). See also Clifford algebra [pr-spin].

As of writing, \(\textsf {Mathlib}\) does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the ring quotient by a suitable closure of a relation like \(v \otimes v \sim Q(v)\).

Hence the definition above.

This definition and what follows in \(\textsf {Mathlib}\) is initially presented in [wieser2022formalizing], some further developments are based on [grinberg2016clifford], and in turn based on [bourbaki2007algebra] which is in French and never translated to English.

The most informative English reference on [bourbaki2007algebra] is [jadczyk2019notes], which has an updated exposition in [jadczyk2023bundle].

Let \(V\) be a vector space \(\mathbb R^n\) over \(\mathbb R\), equipped with a quadratic form \(Q\).

Since \(\mathbb R\) is a commutative ring and \(V\) is a module, the definition above applies.

We denote the canonical \(R\)-linear map to the Clifford algebra \(\mathcal {C}\kern -2pt\ell (M)\) by \(\iota : M \to _{l[R]} \mathcal {C}\kern -2pt\ell (M)\).

It's denoted \(i_\Phi \) or just \(i\) in some literatures.

Given a linear map \(f : M \to _{l[R]} A\) into an \(R\)-algebra \(A\), satisfying \(f(m)^2 = Q(m)\) for all \(m \in M\), called is Clifford, the canonical lift of \(f\) is defined to be a algebra homomorphism from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(A\), denoted \(\operatorname {lift} f : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\).

Given \(f : M \to _{l[R]} A\), which is Clifford, \(F = \operatorname {lift} f\) (denoted \(\bar {f}\) in some literatures), we have:

1. \(F \circ \iota = f\), i.e. the following diagram commutes:

   

2. \(\operatorname {lift}\) is unique, i.e. given \(G : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\), we have: \[ G \circ \iota = f \iff G = \operatorname {lift} f\]

The universal property of the Clifford algebras is now proven, and should be used instead of the definition that is subject to change.

An Exterior algebra over \(M\) is the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\) where \(Q(m) = 0\) for all \(m \in M\).

Same as the previous section, let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

We also use \(m\) or \(m_1, m_2, \dots \) to denote elements of \(M\), i.e. vectors, and \(x, y, z\) to denote elements of \(\mathcal {C}\kern -2pt\ell (Q)\).

Grade involution, intuitively, is negating each basis vector.

Formally, it's an algebra homomorphism \(\alpha : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), satisfying:

1. \(\alpha \circ \alpha = \operatorname {id}\)
2. \(\alpha (\iota (m)) = - \iota (m)\)

for all \(m \in M\).

That is, the following diagram commutes:

It's called main involution \(\alpha \) or main automorphism in [jadczyk2019notes], the canonical automorphism in [gallier2008clifford].

It's denoted \(\hat {m}\) in [lounesto2001clifford], \(\alpha (m)\) in [jadczyk2019notes], \(m^*\) in [chisolm2012geometric].

Grade reversion, intuitively, is reversing the multiplication order of basis vectors. Formally, it's an algebra homomorphism \(\tau : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)^{\mathtt {op}}\), satisfying:

1. \(\tau (m_1 m_2) = \tau (m_2) \tau (m_1)\)
2. \(\tau \circ \tau = \operatorname {id}\)
3. \(\tau (\iota (m)) = \iota (m)\)

That is, the following diagram commutes:

It's called anti-involution \(\tau \) in [jadczyk2019notes], the canonical anti-automorphism in [gallier2008clifford], also called transpose/transposition in some literature, following tensor algebra or matrix.

It's denoted \(\tilde {m}\) in [lounesto2001clifford], \(m^\tau \) in [jadczyk2019notes] (with variants like \(m^t\) or \(m^\top \) in other literatures), \(m^\dagger \) in [chisolm2012geometric].

Clifford conjugate is an algebra homomorphism \({*} : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), denoted \(x^{*}\) (or even \(x^\dagger \), \(x^v\) in some literatures), defined to be: \[ x^{*} = \operatorname {reverse}(\operatorname {involute}(x)) = \tau (\alpha (x)) \] for all \(x \in \mathcal {C}\kern -2pt\ell (Q)\), satisfying (as a \(*\)-ring):

1. \((x + y)^{*} = (x)^{*} + (y)^{*}\)
2. \((x y)^{*} = (y)^{*} (x)^{*}\)
3. \({*} \circ {*} = \operatorname {id}\)
4. \(1^{*} = 1\)

Note: In our current formalization in \(\textsf {Mathlib}\), the application of the involution on \(r\) is ignored, as there appears to be nothing in the literature that advocates doing this.

Clifford conjugate is denoted \(\bar {m}\) in [lounesto2001clifford] and most literatures, \(m^\ddagger \) in [chisolm2012geometric].

The uniqueness of \(\bar {f}\) results from the fact that \(C(Q)\) is generated by \(\rho _{\tiny Q}(E)\). Let \(h\) be the unique homomorphism of \(T(E)\) into \(D\) which extends \(f\) (\(h\) is defined by \(h(x_{1} \otimes \cdots \otimes x_{n}) = f(x_{1}) \ldots f(x_{n})\)). We have \[h(x \otimes x - Q(x) . 1) = (f(x)^{2} - Q(x)) . 1 = 0 , \notag\] and then \(h\) cancels on \(I(Q)\) and defines the homomorphism \(\bar {f}\) through the quotient. 🇫🇷 L'unicité de \(\bar {f}\) résulte de ce que \(C(Q)\) est engendrée par \(\rho _{\tiny Q}(E)\). Soit \(h\) l'unique homomorphisme de \(T(E)\) dans \(D\) qui prolonge \(f\) (\(h\) est défini par \(h(x_{1} \otimes \cdots \otimes x_{n}) = f(x_{1}) \ldots f(x_{n})\)). On a \[h(x \otimes x - Q(x) . 1) = (f(x)^{2} - Q(x)) . 1 = 0 , \notag\] et par suite \(h\) s'annule sur \(I(Q)\) et définit par passage au quotient l'homomorphisme \(\bar {f}\) cherché.

It is sufficient to show that the algebra \(C'\) = \(A' \otimes C(Q)\) and the mapping \(1 \otimes \rho _{\tiny Q}\) of \(E'\) into \(C'\) form a solution to the same problem of universal (mapping) property as \(C(Q')\) and \(\rho _{\tiny Q'}\). 🇫🇷 Il suffit de démontrer que l'algèbre \(C'\) = \(A' \otimes C(Q)\) et l'application \(1 \otimes \rho _{\tiny Q}\) de \(E'\) dans \(C'\) forment une solution du même problème d'application universelle que \(C(Q')\) et \(\rho _{\tiny Q'}\).

Now, let \(D'\) be an algebra on \(A'\), and \(f'\) be a \(A'\)-linear application of \(E'\) in \(D'\) such that \(f'(x')^{2} = Q'(x') . 1\) for all \(x' \in E'\). The mapping \(g: x \to f'(1 \otimes x)\) of \(E\) into \(D'\) (considered as \(A\)-module thanks to the homomorphism \(\varphi \)) is \(A\)-linear, and we have \(g(x)^{2} = Q'(1 \otimes x) . 1 = Q(x) . 1\) for all \(x \in E\). There is thus one and only one \(A\)-homomorphism \(\bar {g}\) of \(C(Q)\) into \(D'\) such that \(\bar {g}(\rho _{\tiny Q}(x)) = f'(1 \otimes x)\). Therefore, there is one and only one \(A'\)-homomorphism \(\bar {f'}\) of \(C'\) into \(D'\) such that \(\bar {f'}(1 \otimes \rho _{\tiny Q }(x)) = f'(1 \otimes x)\) for all \(x \in E\); by linearity, it results that \(\bar {f'}((1 \otimes \rho _{\tiny Q})(x')) = f'(x')\) for all \(x' \in E'\). Q.E.D. 🇫🇷 Or, soient \(D'\) une algèbre sur \(A'\), et \(f'\) une application \(A'\)-linéaire de \(E'\) dans \(D'\) telle que \(f'(x')^{2} = Q'(x') . 1\) pour tout \(x' \in E'\). L'application \(g: x \to f'(1 \otimes x)\) de \(E\) dans \(D'\) (considéré comme \(A\)-module grâce à l'homomorphisme \(\varphi \)) est \(A\)-linéaire, et on a \(g(x)^{2} = Q'(1 \otimes x) . 1 = Q(x) . 1\) pour tout \(x \in E\). Il existe donc un \(A\)-homomorphisme \(\bar {g}\) et un seul de \(C(Q)\) dans \(D'\) tel que \(\bar {g}(\rho _{\tiny Q}(x)) = f'(1 \otimes x)\). Par suite, il existe un \(A'\)-homomorphisme \(\bar {f'}\) et un seul de \(C'\) dans \(D'\) tel que \(\bar {f'}(1 \otimes \rho _{\tiny Q }(x)) = f'(1 \otimes x)\) pour tout \(x \in E\); par linéarité, il en résulte que \(\bar {f'}((1 \otimes \rho _{\tiny Q})(x')) = f'(x')\) pour tout \(x' \in E'\). CQFD.