Category theory

ClassCategory#

A category consists of objects and of arrows, called morphisms, between them, together with a rule for composing arrows end to end that is associative and has an identity arrow at every object. Sets with functions, groups with homomorphisms, and topological spaces with continuous maps are all categories. The notion lets constructions and arguments that recur across algebra, topology and logic be stated once, in terms of how objects relate to one another rather than what they are made of, and it is the starting point of category theory.

Definition

A category \(\mathcal{C}\) consists of

• a collection of objects;
• for every two objects \(X\) and \(Y\), a collection \(\operatorname{Hom}(X, Y)\) of morphisms from \(X\) to \(Y\), a morphism \(f\) in it being written \(f\colon X \to Y\);
• for every object \(X\), an identity morphism \(1_X\colon X \to X\);
• for every three objects \(X, Y, Z\), a composition rule sending \(f\colon X \to Y\) and \(g\colon Y \to Z\) to a morphism \(g \circ f\colon X \to Z\).

These are required to satisfy three axioms. For \(f\colon X \to Y\), the identities are neutral: \(f \circ 1_X = f\) and \(1_Y \circ f = f\). For \(f\colon W \to X\), \(g\colon X \to Y\) and \(h\colon Y \to Z\), composition is associative: \(h \circ (g \circ f) = (h \circ g) \circ f\).

The objects of a category need not form a set; the objects of the category of all sets do not. A category whose objects and morphisms together form a set is called a small category, and one in which each \(\operatorname{Hom}(X, Y)\) is a set is called locally small.

Examples

• Sets. Sets as objects and functions as morphisms, with the usual composition of functions, form a category.
• Algebraic and topological structures. Groups with group homomorphisms, rings with ring homomorphisms, modules over a ring with linear maps, and topological spaces with continuous maps each form a category; see the category of rings, the category of modules and the category of topological spaces.
• Monoids. A monoid \(M\) gives a category with a single object whose morphisms are the elements of \(M\), in which the composite of \(f\) followed by \(g\) is the product \(g f\) and the identity morphism is the unit. When \(M\) is a group every morphism has an inverse.
• Preorders. A preordered set \((P, \le)\) is a category with a morphism from \(x\) to \(y\) exactly when \(x \le y\); composition expresses transitivity and the identities express reflexivity, and there is at most one morphism between two objects.
• Discrete categories. Any set becomes a category whose only morphisms are the identities.
• Opposite categories. Keeping the objects of \(\mathcal{C}\) and reversing the direction of every morphism gives a category, the opposite category \(\mathcal{C}^{\mathrm{op}}\).
• Products. For categories \(\mathcal{C}\) and \(\mathcal{D}\), pairs of objects and pairs of morphisms, composed componentwise, form the product category \(\mathcal{C} \times \mathcal{D}\).

Basic notions

• Uniqueness of identities. If a morphism \(e\colon X \to X\) satisfies \(g \circ e = g\) for every morphism \(g\) out of \(X\), then \(e\) is the identity \(1_X\). So the identities are determined by the composition.
• Isomorphisms. An isomorphism is a morphism \(f\colon X \to Y\) together with a morphism \(g\colon Y \to X\) such that \(g \circ f = 1_X\) and \(f \circ g = 1_Y\). The inverse is unique: if \(f\) is an isomorphism and \(g \circ f = 1_X\), then \(g\) is the inverse of \(f\). In the category of sets, a function is an isomorphism exactly when it is bijective.
• Monomorphisms and epimorphisms. A morphism \(f\colon X \to Y\) is a monomorphism if \(f \circ g = f \circ h\) implies \(g = h\) for all morphisms \(g, h\) into \(X\), and an epimorphism if \(g \circ f = h \circ f\) implies \(g = h\) for all morphisms \(g, h\) out of \(Y\). In the category of sets the monomorphisms are exactly the injective functions and the epimorphisms are exactly the surjective functions. In other categories the analogy can fail: in the category of rings the inclusion of the integers into the rationals is an epimorphism without being surjective.
• Duality. A monomorphism in \(\mathcal{C}\) is the same thing as an epimorphism in \(\mathcal{C}^{\mathrm{op}}\). More generally, each statement expressed in terms of objects, morphisms, composition and identities has a dual, obtained by reversing every arrow and the order of every composite, and if a statement holds in every category then so does its dual.

Related concepts

Maps between categories that preserve identities and composition are functors, and maps between functors are natural transformations. These lead to the Yoneda embedding, adjunctions, limits and monads. Categories with extra structure include monoidal categories and abelian categories, and new categories are built from old ones as comma categories.

In Mathlib

Mathlib makes a category structure on a type of objects: for each pair of objects there is a type of morphisms, so every category is locally small with respect to the universe in which its morphisms live, and the universes of objects and of morphisms are independent parameters. The structure is split in two: the data of identities and composition, which extends a quiver (a directed graph that may have several arrows between two vertices), and the three axioms on top of it. Composition is written in diagrammatic order, first \(f\) then \(g\), so Mathlib's form of \(f \circ 1_X = f\) puts the identity first. An isomorphism is a structure carrying its inverse as data, while being invertible is a separate property of a morphism, the one used in the statement about bijections above; the two are interchangeable, since an invertible morphism determines its inverse. The category of sets is modelled by the category of types of a fixed universe, whose morphisms are functions wrapped in a one-field structure, so that they correspond exactly to functions. In the one-object category of a monoid, following first \(f\) and then \(g\) is the product \(g f\), which agrees with the convention used above.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Category
• Source of CategoryTheory.Category in Mathlib/CategoryTheory/Category/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Category

Uses 1 · Used by 20

Statement usesSet

Used byThe category of algebras over a ring · Abelian category · Adjunction · Cartesian closed · Comma category · Functor · Grothendieck topology · Isomorphism · Limits · Monad · Monoidal category · Natural transformation · Presheafed space · Sheafed space · Small category · Yoneda embedding · Chain complex · Functorial homology · Category of finite-dimensional representations · The category of rings

AbbreviationSmall category#

A small category is a category whose objects form a set and whose morphisms form a set, rather than a proper class. Smallness is the size condition under which a category can be handled like any other set-sized mathematical object: diagrams are indexed by small categories, functors from a small category to a locally small category form a locally small category, and categories of presheaves on a small category are the setting of sheaf theory. The categories that collect every structure of a given kind, such as all sets or all groups, are not small, and the distinction between the two kinds of category runs through the whole subject.

Definition

A category \(C\) is small if its objects form a set and the collection of all its morphisms forms a set. Since the morphisms are the union of the hom-sets \(\operatorname{Hom}(X, Y)\) over all pairs of objects, this is the same as asking that the objects form a set and that each \(\operatorname{Hom}(X, Y)\) is a set. A category is locally small if every \(\operatorname{Hom}(X, Y)\) is a set, with no condition on the objects, and large if it is not small.

The words set and class depend on the foundations. In a set theory with classes, small means set-sized. In a framework with a Grothendieck universe \(\mathcal U\), a category is \(\mathcal U\)-small when its objects and morphisms form sets that are elements of \(\mathcal U\). Mathlib's type theory has a hierarchy of universes that plays the same role: there a small category is one whose objects and morphisms lie in the same universe \(u\), while a large category has its objects one universe higher than its morphisms.

Examples

• Finite categories. Any category with finitely many morphisms is small, for instance the category with two objects and a single non-identity arrow between them.
• Preorders. A set \(P\) with a preorder \(\le\) is a small category with a morphism from \(x\) to \(y\) exactly when \(x \le y\); reflexivity gives the identities, transitivity gives composition, and there is at most one morphism between two objects.
• Monoids. A monoid \(M\) gives a category with one object whose morphisms are the elements of \(M\), the composite \(g \circ f\) being the product \(gf\) and the identity being the unit. A group gives in this way a one-object category in which every morphism is invertible.
• Sets. Any set \(S\) is a small category whose only morphisms are identities, the discrete category on \(S\).
• Functor categories. For categories \(C\) and \(D\), the functors from \(C\) to \(D\) and the natural transformations between them form a category. When \(C\) and \(D\) are small, so is this category: a functor between small categories is a set-sized piece of data, and a natural transformation is a family of morphisms indexed by the set of objects of \(C\).

The category of all sets, the category of all groups and the category of all topological spaces are locally small but not small, since their objects form a proper class. In Mathlib's terms, the types of a universe \(u\) with functions between them form a category whose morphisms lie in \(u\) while the collection of objects lies in the next universe, so this category is large.

Properties

• The category of small categories. Small categories and functors form a category. It is not itself small, because it contains the discrete category on every set.
• Small limits. A category is complete when every diagram indexed by a small category has a limit. The categories of sets and of groups are complete. Mathlib asks for limits of every diagram indexed by a small category in the universe of the target's morphisms.
• Small complete categories are preorders. If a small category \(C\) has all products indexed by sets, then between two objects \(X\) and \(Y\) there is at most one morphism. Indeed, let \(\kappa\) be the cardinality of the set of all morphisms of \(C\) and suppose \(\operatorname{Hom}(X, Y)\) had two elements. Morphisms from \(X\) to the product of \(\kappa\) copies of \(Y\) correspond to \(\kappa\)-tuples of morphisms from \(X\) to \(Y\), so there would be at least \(2^\kappa\) of them, more than \(\kappa\) by Cantor's theorem, although all of them are among the \(\kappa\) morphisms of \(C\). Completeness is therefore a severe restriction on small categories, and the interesting complete categories are large.
• Presheaves. For a small category \(C\) the presheaves on \(C\), the functors from the opposite category of \(C\) to sets, form a locally small category, since a natural transformation between two presheaves is a family of functions indexed by a set. The Yoneda embedding embeds \(C\) into this category, and sheaves for a Grothendieck topology on a small category form a full subcategory of it.

Essentially small categories

Many large categories are small up to equivalence. A category is essentially small if it is equivalent to a small category. The category of finite sets is an example: its objects form a proper class, but every finite set is isomorphic to \(\{1, \dots, n\}\) for some \(n\), so the full subcategory on these sets is small and equivalent to the whole. In general, relative to a universe, a category is essentially small if and only if its isomorphism classes of objects form a small set and it is locally small, where locally small means that every hom-set is small. Since smallness is measured against a universe, every category is essentially small relative to a universe that contains its objects and its morphisms.

In Mathlib

A category in Mathlib carries two independent universe levels, one for the type of objects and one for the morphisms. A small category is not a separate structure but the name for a category in which the two levels agree, so every small category is a category without conversion. Most of the library is stated for an arbitrary pair of levels, and smallness appears only where a result needs it, for example for the shapes of diagrams. A small category is small relative to the universe of its own objects; essentially small and locally small take the universe they measure against as a universe parameter. The one-object category of a monoid keeps its single object in the lowest universe, so it fits the small pattern literally only for a monoid in that universe, although it is small in the set-theoretic sense in every case. Mathlib's category of categories is indexed by both levels, and the small categories of level \(u\) are the case where they coincide. The theorem on small complete categories is an unnamed instance stating that a small category with all products of its own size has at most one morphism between any two objects; it concludes this about the hom-sets rather than producing a preorder.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.SmallCategory
• Source of CategoryTheory.SmallCategory in Mathlib/CategoryTheory/Category/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.SmallCategory

Uses 5 · Used by 7

Statement usesCategory · Set

Proof usesCardinal · Cantor’s Theorem · Limits

Used byHall's marriage theorem · Locally ringed space · Structure theorem · Beck's monadicity theorem · Mitchell's embedding theorem · Nielsen–Schreier theorem · Schur's lemma (1000+ theorems)

StructureFunctor#

A functor is a structure-preserving map between two categories: it sends objects to objects and morphisms to morphisms, respecting identities and composition. Functors are the basic way of comparing categories, and many constructions of algebra and topology, such as taking the fundamental groupoid of a space, the homology of a chain complex or the underlying set of a group, are functors. Saying that a construction is functorial means that it acts on morphisms as well as on objects, compatibly with composition.

Definition

Let \(\mathcal{C}\) and \(\mathcal{D}\) be categories. A functor \(F\) from \(\mathcal{C}\) to \(\mathcal{D}\), written \(F \colon \mathcal{C} \to \mathcal{D}\), consists of

• for each object \(X\) of \(\mathcal{C}\), an object \(F(X)\) of \(\mathcal{D}\);
• for each morphism \(f \colon X \to Y\) of \(\mathcal{C}\), a morphism \(F(f) \colon F(X) \to F(Y)\) of \(\mathcal{D}\),

subject to two axioms: \(F\) preserves identities, and \(F\) preserves composition:

\[F(\mathrm{id}_X) = \mathrm{id}_{F(X)}, \qquad F(g \circ f) = F(g) \circ F(f)\]

for every object \(X\) and all composable morphisms \(f \colon X \to Y\) and \(g \colon Y \to Z\).

Every category has an identity functor, and functors \(F \colon \mathcal{C} \to \mathcal{D}\) and \(G \colon \mathcal{D} \to \mathcal{E}\) have a composite \(G \circ F\), acting by \(X \mapsto G(F(X))\) and \(f \mapsto G(F(f))\). Composition of functors is associative, and composing with an identity functor changes nothing: \(F \circ \mathrm{id}_{\mathcal{C}} = F\) and \(\mathrm{id}_{\mathcal{D}} \circ F = F\). Consequently categories and functors themselves form a category, the category of categories, provided one restricts to categories of a bounded size so as to avoid set-theoretic paradoxes.

A contravariant functor from \(\mathcal{C}\) to \(\mathcal{D}\) reverses the direction of morphisms, sending \(f \colon X \to Y\) to \(F(f) \colon F(Y) \to F(X)\) and satisfying \(F(g \circ f) = F(f) \circ F(g)\). It is the same thing as an ordinary functor from the opposite category \(\mathcal{C}^{\mathrm{op}}\) to \(\mathcal{D}\), and this is how it is usually treated.

Examples

• Forgetful functors. Sending a group, ring or topological space to its underlying set, and a homomorphism or continuous map to its underlying function, is a functor to the category of sets. More generally every category whose objects are sets with structure carries a forgetful functor to sets.
• Monoids and groups. A monoid can be viewed as a category with a single object whose morphisms are its elements. For monoids \(M\) and \(N\), functors between these one-object categories correspond exactly to monoid homomorphisms from \(M\) to \(N\); in particular functors between groups viewed this way are group homomorphisms.
• Preorders. A preordered set can be viewed as a category with at most one morphism from \(x\) to \(y\), present exactly when \(x \le y\). Every monotone map gives a functor, and every functor between preorders is monotone on objects.
• Topology. Sending a topological space to its fundamental groupoid, and a continuous map to the induced map on homotopy classes of paths, is a functor from topological spaces to groupoids.
• Homology. In a category in which homology is defined, such as an abelian category, taking the \(i\)th homology of a chain complex is a functor from complexes to the category itself.
• Duality. Sending a vector space \(V\) over a field \(K\) to its dual space \(V^*\), and a linear map to its transpose, is a contravariant functor from \(K\)-vector spaces to themselves.
• Hom functors. In a category whose morphisms between any two objects form a set, fix an object \(A\). Sending \(X\) to the set of morphisms \(A \to X\) is a functor to sets, and sending \(X\) to the set of morphisms \(X \to A\) is a contravariant one; letting \(A\) vary in the second gives the Yoneda embedding.

Properties

An isomorphism is a morphism \(f\) with a two-sided inverse \(g\). A functor sends isomorphisms to isomorphisms, since it carries the equations \(g \circ f = \mathrm{id}\) and \(f \circ g = \mathrm{id}\) to the same equations for \(F(f)\) and \(F(g)\). The converse fails in general: the forgetful functor from topological spaces to sets sends a continuous bijection whose inverse is not continuous to an isomorphism of sets.

For objects \(X\) and \(Y\) of \(\mathcal{C}\), a functor induces a map from the morphisms \(X \to Y\) to the morphisms \(F(X) \to F(Y)\). The functor is faithful if each of these maps is injective, and full if each is surjective. Forgetful functors are typically faithful but not full. A composite of faithful functors is faithful, and a composite of full functors is full. A functor that is both full and faithful does detect isomorphisms: if \(F(f)\) is an isomorphism, so is \(f\).

A functor is essentially surjective if every object of \(\mathcal{D}\) is isomorphic to \(F(X)\) for some object \(X\) of \(\mathcal{C}\). A functor that is full, faithful and essentially surjective is an equivalence of categories: this is the appropriate notion of "sameness" for categories, weaker than isomorphism, and it holds exactly when there is a functor \(G\) in the other direction with \(G \circ F\) and \(F \circ G\) isomorphic to the identity functors.

Related concepts

Functors from \(\mathcal{C}\) to \(\mathcal{D}\) are themselves the objects of a category, the functor category, whose morphisms are natural transformations. Two functors in opposite directions related by a natural bijection of morphism sets form an adjunction, and a functor from a category to itself equipped with suitable natural transformations is a monad. Functors from a small index category are the diagrams whose limits are studied in category theory, and contravariant functors to sets are presheaves, the starting point of sheaf theory.

In Mathlib

Mathlib bundles a functor as a structure recording its action on objects, its action on morphisms, and proofs of the two axioms; a separate function recovers its underlying map of directed graphs, a prefunctor between the underlying quivers. Composition of morphisms is written in diagrammatic order, first \(f\) then \(g\), so the composition axiom reads with the factors in that order. Categories carry two universe levels, one for objects and one for morphisms, and a functor may join categories of different sizes. Functors are compared up to natural isomorphism rather than equality whenever possible, and the identity and associativity laws for composition hold by definition. A contravariant functor is formalized as a functor out of the opposite category. Mathlib has two forms of equivalence of categories: a structure recording a functor together with an inverse functor, unit and counit natural isomorphisms and a triangle law, and a property of a single functor, being an equivalence, defined as being full, faithful and essentially surjective. It shows that a functor with an inverse up to natural isomorphism is an equivalence. The category of categories is formed for each pair of universe levels, and its morphisms are functors wrapped in a thin structure.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Functor
• Source of CategoryTheory.Functor in Mathlib/CategoryTheory/Functor/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Functor

Uses 1 · Used by 12

Statement usesCategory

Used byAdjunction · Cartesian closed · Comma category · Grothendieck topology · Limits · Monad · Monoidal category · Natural transformation · Presheafed space · Sheafed space · Yoneda embedding · Functorial homology

StructureNatural transformation#

A natural transformation is a morphism between two functors with the same source and target categories. It assigns to each object of the source a morphism in the target, and these morphisms are compatible with every morphism of the source. The notion makes precise the informal idea of a construction that is "natural", one defined uniformly without arbitrary choices, and it is the basic ingredient of functor categories, adjunctions, limits and the Yoneda embedding.

Definition

Let \(C\) and \(D\) be categories and \(F, G : C \to D\) functors. A natural transformation \(\alpha : F \Rightarrow G\) consists of a morphism \(\alpha_X : F(X) \to G(X)\) in \(D\) for every object \(X\) of \(C\), called the component of \(\alpha\) at \(X\), such that for every morphism \(f : X \to Y\) of \(C\) the naturality square commutes:

\[G(f) \circ \alpha_X = \alpha_Y \circ F(f).\]

Both sides are morphisms \(F(X) \to G(Y)\), so the condition says that applying \(F\) and then the component at \(Y\) gives the same result as applying the component at \(X\) and then \(G\). A natural transformation is determined by its components: two natural transformations with the same components are equal.

Examples

• The double dual. For a vector space \(V\) over a field \(k\), let \(\mathrm{ev}_V : V \to V^{**}\) send \(v\) to the functional \(\varphi \mapsto \varphi(v)\) on the dual space. For a linear map \(f : V \to W\) one checks \(f^{**} \circ \mathrm{ev}_V = \mathrm{ev}_W \circ f\), so the maps \(\mathrm{ev}_V\) form a natural transformation from the identity functor to the double dual functor. Each component is injective, and it is an isomorphism exactly when \(V\) is finite-dimensional. By contrast, the isomorphisms between a finite-dimensional space and its dual that one usually writes down depend on a choice of basis, and since the dual is contravariant they do not form a natural transformation in this sense.
• The determinant. For a commutative ring \(R\), the determinant is a group homomorphism from the general linear group \(GL_n(R)\) to the group of units \(R^\times\). A ring homomorphism \(\varphi : R \to S\) satisfies \(\det(\varphi(A)) = \varphi(\det A)\), where \(\varphi\) is applied entrywise, because the determinant is a polynomial with integer coefficients in the entries. So the determinant is a natural transformation between two functors from commutative rings to groups.
• Abelianization. The quotient maps \(G \to G/[G,G]\) form a natural transformation from the identity functor on groups to the functor sending a group to its abelianization.
• Cones. A cone over a diagram \(F : J \to C\) with apex \(X\) is a family of morphisms from \(X\) to the objects \(F(j)\), compatible with the morphisms of \(J\). This is exactly a natural transformation from the constant functor at \(X\) to \(F\) (the functor sending every object of \(J\) to \(X\) and every morphism to \(\mathrm{id}_X\)), and limits are defined as universal cones.

Properties

• The functor category. Natural transformations can be composed componentwise: for \(\alpha : F \Rightarrow G\) and \(\beta : G \Rightarrow H\), the vertical composite has components \((\beta \circ \alpha)_X = \beta_X \circ \alpha_X\), and the identity transformation of \(F\) has components the identities of the objects \(F(X)\). With these operations, functors from \(C\) to \(D\) and the natural transformations between them form a category.
• Natural isomorphisms. A natural isomorphism is an isomorphism in the functor category. A natural transformation is an isomorphism if and only if each of its components is an isomorphism: the inverses of the components are automatically natural. Similarly, if every component is an epimorphism, the transformation is an epimorphism of the functor category, where a morphism \(e\) is an epimorphism when \(g \circ e = h \circ e\) implies \(g = h\).
• Whiskering. Given \(\alpha : G \Rightarrow H\) between functors \(D \to E\) and a functor \(F : C \to D\), the transformation with components \(\alpha_{F(X)}\) goes from \(GF\) to \(HF\). Given instead \(\alpha : G \Rightarrow H\) between functors \(C \to D\) and \(F : D \to E\), the components \(F(\alpha_X)\) give a natural transformation from \(FG\) to \(FH\).
• Horizontal composition. For \(\alpha : F \Rightarrow G\) between functors \(C \to D\) and \(\gamma : I \Rightarrow J\) between functors \(D \to E\), the horizontal composite \(\gamma * \alpha : IF \Rightarrow JG\) has components \(J(\alpha_X) \circ \gamma_{F(X)}\), which by naturality of \(\gamma\) also equal \(\gamma_{G(X)} \circ I(\alpha_X)\). For further transformations \(\beta : G \Rightarrow H\) and \(\delta : J \Rightarrow K\), the two compositions satisfy the interchange law

\[(\delta \circ \gamma) * (\beta \circ \alpha) = (\delta * \beta) \circ (\gamma * \alpha).\]

• Transformations of the identity functor. If \(\alpha\) and \(\beta\) are natural transformations from the identity functor of \(C\) to itself, the naturality of \(\alpha\) at the morphism \(\beta_X\) gives \(\alpha_X \circ \beta_X = \beta_X \circ \alpha_X\), so such transformations commute. On abelian groups, multiplication by a fixed integer is an example.
• The Yoneda lemma. The opposite category of \(C\) has the same objects as \(C\) and every morphism reversed, so a functor \(F\) from it to sets assigns a set \(F(X)\) to each object \(X\) of \(C\) and a map \(F(Y) \to F(X)\) to each morphism \(X \to Y\). For such \(F\) and an object \(X\), sending a natural transformation \(\eta\) from the represented functor \(\mathrm{Hom}(-, X)\) to \(F\) to the element \(\eta_X(\mathrm{id}_X)\) is a bijection onto \(F(X)\).

Related concepts

The unit and counit of an adjunction and the unit and multiplication of a monad are natural transformations. Two categories are equivalent when there are functors in both directions whose composites are naturally isomorphic to the identity functors. Categories, functors and natural transformations together form the prototypical 2-category, in which natural transformations are the 2-morphisms.

In Mathlib

Mathlib bundles a natural transformation as a structure with two fields: the family of components and a proof of the naturality square for every morphism. The square is written with composition in diagrammatic order, first \(F(f)\) and then \(\alpha_Y\), and the proof field is filled in by an automatic category-theory tactic when the author supplies none. The morphisms of the functor category are by definition the natural transformations, and its composition is vertical composition, so a natural isomorphism is not a separate notion: it is an isomorphism in that category, and the criterion via components is a theorem. Horizontal composition is a separate operation, and its notation lists the factors in the opposite order from the one used here: the transformation between the first pair of functors comes first, so the composite written \(\gamma * \alpha\) above appears with \(\alpha\) first. An equivalence of categories also records one triangle identity relating the two natural isomorphisms; given any pair of natural isomorphisms, Mathlib adjusts one of them so that the identity holds. For a cone, Mathlib takes the definition by a natural transformation from a constant functor literally. In the Yoneda lemma the functor \(F\) takes values in types of the same universe as the morphisms of \(C\).

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.NatTrans
• Source of CategoryTheory.NatTrans in Mathlib/CategoryTheory/NatTrans.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.NatTrans

Uses 2 · Used by 6

Statement usesCategory · Functor

Used byAdjunction · Limits · Monad · Monoidal category · Presheafed space · Yoneda embedding

DefinitionYoneda embedding#

The Yoneda embedding of a category \(\mathcal{C}\) sends each object \(X\) to the presheaf of morphisms into \(X\), the contravariant functor \(Y \mapsto \mathrm{Hom}(Y, X)\) to sets. It is fully faithful, so \(\mathcal{C}\) sits inside the category of presheaves on \(\mathcal{C}\) without losing or gaining any morphisms. The underlying result, the Yoneda lemma, identifies the natural transformations from the presheaf of morphisms into \(X\) to any presheaf \(F\) with the elements of \(F(X)\). It implies that an object is determined up to isomorphism by the functor of morphisms into it; this justifies defining objects by the functors they represent, a method used throughout algebra, topology and algebraic geometry.

Definition

Let \(\mathcal{C}\) be a category in which the morphisms between any two objects form a set. For an object \(X\), write \(h_X\) for the functor from the opposite category \(\mathcal{C}^{\mathrm{op}}\) to sets given by

\[h_X(Y) = \mathrm{Hom}(Y, X), \qquad h_X(g)(f) = f \circ g\]

for a morphism \(g \colon Y' \to Y\) and \(f \in \mathrm{Hom}(Y, X)\). A morphism \(u \colon X \to X'\) induces a natural transformation \(h_u \colon h_X \to h_{X'}\) whose component at \(Y\) is composition with \(u\), sending \(f\) to \(u \circ f\). The assignments \(X \mapsto h_X\) and \(u \mapsto h_u\) form the Yoneda embedding, a functor from \(\mathcal{C}\) to the category of presheaves on \(\mathcal{C}\), that is, of functors \(\mathcal{C}^{\mathrm{op}} \to \mathbf{Set}\) with natural transformations as morphisms.

Reversing the roles of source and target gives the co-Yoneda embedding, which sends \(X\) to the covariant functor \(\mathrm{Hom}(X, -)\) and is a functor out of \(\mathcal{C}^{\mathrm{op}}\).

The Yoneda lemma

Let \(F\) be a presheaf on \(\mathcal{C}\) and \(X\) an object. A natural transformation \(\eta \colon h_X \to F\) determines the element \(\eta_X(\mathrm{id}_X)\) of \(F(X)\), and naturality forces \(\eta_Y(f) = F(f)\bigl(\eta_X(\mathrm{id}_X)\bigr)\) for every \(f \colon Y \to X\). Conversely every element \(x\) of \(F(X)\) defines a natural transformation by \(f \mapsto F(f)(x)\). Hence natural transformations from \(h_X\) to \(F\) correspond bijectively to elements of \(F(X)\), and this bijection is natural in both \(X\) and \(F\).

Taking \(F = h_{X'}\) shows that every natural transformation \(h_X \to h_{X'}\) is \(h_u\) for exactly one morphism \(u \colon X \to X'\), namely the image of \(\mathrm{id}_X\). In other words, the Yoneda embedding is fully faithful: it is full and faithful. The same argument shows that the co-Yoneda embedding is fully faithful.

Consequences

• Objects are determined by their morphisms. If there are bijections \(\mathrm{Hom}(Z, X) \cong \mathrm{Hom}(Z, Y)\) for all \(Z\), natural in \(Z\), then \(X\) and \(Y\) are isomorphic.
• Detecting isomorphisms. A morphism \(f \colon X \to Y\) is an isomorphism if and only if for every object \(T\), composition with \(f\) is a bijection from \(\mathrm{Hom}(T, X)\) to \(\mathrm{Hom}(T, Y)\).
• Representable functors. A presheaf \(F\) is representable if it is naturally isomorphic to \(h_X\) for some object \(X\). Such an isomorphism is the same as a choice of bijections \(\mathrm{Hom}(Y, X) \cong F(Y)\) natural in \(Y\), and by the Yoneda lemma it is determined by a single element of \(F(X)\), the universal element. Two objects representing the same presheaf are isomorphic. Universal properties are statements of representability: a product of \(A\) and \(B\), for instance, is an object representing \(Y \mapsto \mathrm{Hom}(Y, A) \times \mathrm{Hom}(Y, B)\), which is why products and other limits are unique up to a unique isomorphism compatible with their universal elements (for a product, with the two projections).
• Maps out of presheaves. Two morphisms of presheaves \(P \to Q\) are equal as soon as they agree after composing with every morphism \(h_X \to P\), so a presheaf is controlled by the representable presheaves mapping to it.

Examples

• Monoids. A monoid \(M\) can be regarded as a category with one object whose morphisms are the elements of \(M\), composed by multiplication. A presheaf on it is a set with a right action of \(M\), and the single representable presheaf is \(M\) acting on itself by right multiplication. The maps from \(M\) to itself that commute with this action are exactly the left multiplications, and full faithfulness says that \(m \mapsto (x \mapsto mx)\) identifies \(M\) with them. So every monoid is isomorphic to a monoid of maps from a set to itself under composition; for a group this is Cayley's theorem, that every group is isomorphic to a group of permutations.
• Partial orders. A partially ordered set can be regarded as a category with one morphism from \(y\) to \(x\) when \(y \le x\) and none otherwise. Then \(h_x(y)\) is a one-point set when \(y \le x\) and empty otherwise, so \(h_x\) records the set of elements below \(x\). Full faithfulness says that \(x \le x'\) exactly when every element below \(x\) lies below \(x'\).
• Subsets. On the category of sets, the presheaf sending a set \(Y\) to its set of subsets, and a map to the operation of taking preimages, is represented by a two-element set \(\{0, 1\}\): a subset corresponds to its indicator function, and the universal element is the subset \(\{1\}\).

Related concepts

Representability of the functor \(Y \mapsto \mathrm{Hom}(F(Y), Z)\) for each \(Z\) is what it means for a functor \(F\) to have a right adjoint, and much of the theory of adjunctions is the Yoneda lemma applied with parameters. On a small category every presheaf is a colimit of representable ones, and the presheaf category is the free completion of \(\mathcal{C}\) under colimits. Replacing presheaves by sheaves for a Grothendieck topology gives the setting in which schemes and other geometric objects can be studied through the functors of morphisms into them.

In Mathlib

Mathlib defines the Yoneda embedding for every category, with presheaves valued in the types of the same universe as the morphisms of \(\mathcal{C}\); this plays the role of the hypothesis that morphisms between two objects form a set, so no separate smallness assumption is needed, and a variant raising the universe of the values is also provided. Composition is written in diagrammatic order, so the formulas above appear with their factors reversed. The Yoneda lemma is given both as a plain bijection for fixed \(X\) and \(F\) and as a natural isomorphism between two functors of the pair \((X, F)\); because the second ranges over all presheaves, its values are lifted to a larger universe. Full faithfulness is recorded as data, an explicit inverse to the action on morphisms, from which fullness and faithfulness follow. A representation of a presheaf is likewise data, a family of bijections natural in the argument, while representability is the proposition that some representation exists; presheaves valued in any universe may be representable.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.yoneda
• Source of CategoryTheory.yoneda in Mathlib/CategoryTheory/Yoneda.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.yoneda

Uses 3 · Used by 2

Statement usesCategory · Functor · Natural transformation

Used byScheme · Mitchell's embedding theorem

StructureIsomorphism#

An isomorphism in a category is a morphism that can be undone: a morphism \(f\colon X \to Y\) for which there is a morphism back from \(Y\) to \(X\) whose composites with \(f\), in either order, are identities. Two objects joined by an isomorphism are indistinguishable by anything the category can express, so isomorphism, rather than equality, is the natural notion of sameness for objects. It specializes to bijections of sets, isomorphisms of groups and rings, and homeomorphisms of spaces.

Definition

Let \(X\) and \(Y\) be objects of a category \(\mathcal{C}\). An isomorphism from \(X\) to \(Y\) is a morphism \(f\colon X \to Y\) for which there is a morphism \(g\colon Y \to X\) with \(g \circ f = 1_X\) and \(f \circ g = 1_Y\). The morphism \(g\) is the inverse of \(f\), written \(f^{-1}\). The objects \(X\) and \(Y\) are called isomorphic, written \(X \cong Y\), when some isomorphism between them exists.

The inverse is determined by \(f\), and even one of the two equations pins it down: if \(f\) is an isomorphism and a morphism \(h\colon Y \to X\) satisfies \(h \circ f = 1_X\), then \(h\) is the inverse of \(f\). Consequently two isomorphisms with the same forward morphism are equal, and being an isomorphism is a property of a morphism rather than extra data.

Examples

• Sets. In the category of sets and functions, a function is an isomorphism exactly when it is bijective; its inverse is the inverse function.
• Algebraic structures. In a concrete category whose forgetful functor to sets reflects isomorphisms, as for groups with group homomorphisms or rings with ring homomorphisms, a morphism is an isomorphism exactly when its underlying function is bijective. For groups this recovers the usual notion: a bijective group morphism has a homomorphic inverse.
• Topological spaces. In the category of topological spaces, with continuous maps as morphisms, the isomorphisms are exactly the homeomorphisms (see homeomorphism). Here bijectivity is not enough: the identity function from a two-point set with the discrete topology to the same set with the indiscrete topology is a continuous bijection whose inverse is not continuous.
• Preorders. In a category with at most one morphism between any two objects, such as a preordered set viewed as a category, a morphism from \(x\) to \(y\) is an isomorphism exactly when some morphism from \(y\) to \(x\) exists. So \(x \cong y\) means \(x \le y\) and \(y \le x\), and in a partially ordered set isomorphic objects are equal.
• Monoids. In the one-object category of a monoid \(M\), the isomorphisms are the invertible elements of \(M\).

Properties

• Identities, inverses and composites. For each object \(X\), the identity \(1_X\) is an isomorphism; the inverse \(f^{-1}\) of an isomorphism is an isomorphism with inverse \(f\); and if \(f\colon X \to Y\) and \(g\colon Y \to Z\) are isomorphisms, so is \(g \circ f\), with \((g \circ f)^{-1} = f^{-1} \circ g^{-1}\). Hence being isomorphic is an equivalence relation on objects.
• Automorphisms. The isomorphisms from an object \(X\) to itself, its automorphisms, form a group under composition. The automorphism group of a set is its permutation group.
• Functors. Every functor \(F\) preserves isomorphisms: if \(f\) is an isomorphism then so is \(F(f)\), with inverse \(F(f^{-1})\). The converse fails in general, but if \(F\) is full and faithful and \(F(f)\) is an isomorphism, then \(f\) is an isomorphism.
• Cancellation. An isomorphism is both a monomorphism and an epimorphism: it can be cancelled from either side of an equation between composites. The converse fails in some categories: in the category of rings the inclusion of the integers into the rationals is a monomorphism and an epimorphism but not an isomorphism. A category in which every morphism that is both is an isomorphism is called balanced; there the isomorphisms are exactly the morphisms that are monomorphisms and epimorphisms. The category of sets is balanced.

Related concepts

A category in which every morphism is an isomorphism is a groupoid; a group amounts to a groupoid with a single object. An isomorphism in the category of functors from \(\mathcal{C}\) to \(\mathcal{D}\), whose morphisms are natural transformations, is a natural isomorphism, and a natural transformation is an isomorphism exactly when each of its components is. Weakening the equations \(g \circ f = 1\) and \(f \circ g = 1\) to natural isomorphisms between functors leads to equivalences of categories. The isomorphism theorems of algebra, such as the first isomorphism theorem, produce particular isomorphisms between groups.

In Mathlib

Mathlib treats an isomorphism as bundled data: a structure holding the forward morphism, the inverse morphism and the two equations. Separately, the property of a single morphism being an isomorphism is a proposition that only asserts that some inverse exists; the inverse is then recovered by choice, which is harmless because it is unique. Composition is written in diagrammatic order, first \(f\) then \(g\), so Mathlib's form of \((g \circ f)^{-1} = f^{-1} \circ g^{-1}\) lists \(g^{-1}\) first. Many familiar isomorphisms, such as bijections between types, group isomorphisms and homeomorphisms, are also defined directly as structures of their own, outside category theory, and Mathlib provides translations between those and isomorphisms in the corresponding categories. The dual statement that an isomorphism is a monomorphism is generated automatically from the one about epimorphisms.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Iso
• Source of CategoryTheory.Iso in Mathlib/CategoryTheory/Iso.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Iso

Uses 1 · Used by 7

Statement usesCategory

Used byMonoidal category · Scheme · Structure theorem · Beck's monadicity theorem · Mitchell's embedding theorem · Nielsen–Schreier theorem · Schur's lemma (Linear representations)

StructureAdjunction#

An adjunction is a relationship between two functors running in opposite directions between two categories, \(F \colon \mathcal{C} \to \mathcal{D}\) and \(G \colon \mathcal{D} \to \mathcal{C}\), in which morphisms \(F(X) \to Y\) in \(\mathcal{D}\) correspond exactly, naturally in \(X\) and \(Y\), to morphisms \(X \to G(Y)\) in \(\mathcal{C}\). The functor \(F\) is then called the left adjoint and \(G\) the right adjoint, and one writes \(F \dashv G\). Adjunctions occur throughout mathematics: free constructions, the discrete topology functor, currying of functions and Galois connections all give adjunctions. They are weaker than equivalences of categories but still strong enough to force preservation of limits and to produce monads.

Definition

Let \(F \colon \mathcal{C} \to \mathcal{D}\) and \(G \colon \mathcal{D} \to \mathcal{C}\) be functors. An adjunction \(F \dashv G\) consists of two natural transformations, the unit \(\eta \colon 1_{\mathcal{C}} \Rightarrow G F\) and the counit \(\varepsilon \colon F G \Rightarrow 1_{\mathcal{D}}\), satisfying the two triangle identities

\[\varepsilon_{F(X)} \circ F(\eta_X) = 1_{F(X)}, \qquad G(\varepsilon_Y) \circ \eta_{G(Y)} = 1_{G(Y)}\]

for every object \(X\) of \(\mathcal{C}\) and \(Y\) of \(\mathcal{D}\).

An equivalent description uses hom-sets. An adjunction yields a bijection

\[\operatorname{Hom}_{\mathcal{D}}(F(X), Y) \cong \operatorname{Hom}_{\mathcal{C}}(X, G(Y))\]

sending \(f \colon F(X) \to Y\) to \(G(f) \circ \eta_X\), with inverse sending \(g \colon X \to G(Y)\) to \(\varepsilon_Y \circ F(g)\). This bijection is natural in both variables: it is compatible with precomposition by morphisms of \(\mathcal{C}\) and with postcomposition by morphisms of \(\mathcal{D}\). Conversely, any family of bijections natural in this sense determines an adjunction, whose unit at \(X\) is the morphism corresponding to the identity of \(F(X)\), and whose counit at \(Y\) is the morphism corresponding to the identity of \(G(Y)\).

Examples

• Free and forgetful functors. Homomorphisms from the free group on a set \(S\) to a group \(H\) correspond exactly to functions from \(S\) to the underlying set of \(H\): every function extends uniquely to a homomorphism. This makes the free group functor left adjoint to the forgetful functor from groups to sets.
• Discrete and indiscrete topologies. Every function out of a discrete space is continuous, so the discrete topology functor is left adjoint to the forgetful functor from topological spaces to sets (see the category of topological spaces). Dually, every function into an indiscrete space is continuous, so the forgetful functor is left adjoint to the indiscrete topology functor.
• Galois connections. A preorder is a category with at most one morphism between any two objects, and a functor between preorders is a monotone map. An adjunction between monotone maps \(l\) and \(u\) is then the condition that \(l(x) \le y\) holds exactly when \(x \le u(y)\), so every Galois connection between preorders is an adjunction.
• Currying. In the category of sets, functions \(A \times X \to Y\) correspond to functions \(X \to Y^A\), so taking the product with \(A\) is left adjoint to taking functions out of \(A\). More generally, in a closed monoidal category, tensoring with \(A\) on the left is left adjoint to the internal hom out of \(A\).
• Equivalences. Every equivalence of categories is an adjunction, and conversely an adjunction whose unit and counit have invertible components is an equivalence.

Properties

• Uniqueness. Adjoints are unique up to natural isomorphism: if \(F\) and \(F'\) are both left adjoint to \(G\), then \(F\) and \(F'\) are naturally isomorphic, and likewise two right adjoints of the same functor are naturally isomorphic.
• Composition. If \(F \dashv G\) with \(F \colon \mathcal{C} \to \mathcal{D}\) and \(H \dashv I\) with \(H \colon \mathcal{D} \to \mathcal{E}\), then \(H F\) is left adjoint to \(G I\).
• Limits. A left adjoint preserves all colimits and a right adjoint preserves all limits (see limits). For instance, the underlying set of a product of groups is the product of the underlying sets, and the free group on a disjoint union of sets is the free product (the coproduct in the category of groups) of the free groups on the pieces.
• Monads. For an adjunction \(F \dashv G\), the composite \(G F\) is a functor from \(\mathcal{C}\) to itself, and it becomes a monad on \(\mathcal{C}\) with unit \(\eta\) and multiplication \(G \varepsilon F \colon G F G F \Rightarrow G F\); see monad.
• Fully faithful adjoints. If the right adjoint is full and faithful, the counit is an isomorphism, and if the counit is an isomorphism, the right adjoint is fully faithful. A full and faithful right adjoint is called reflective, its essential image is a reflective subcategory, and its left adjoint is called the reflector. For instance, the inclusion of abelian groups into groups is full and faithful, and abelianization is left adjoint to it.

Related concepts

An adjunction can also be described through universal arrows. Given \(F \dashv G\) and an object \(A\) of \(\mathcal{C}\), consider the comma category whose objects are pairs \((B, f)\) of an object \(B\) of \(\mathcal{D}\) and an arrow \(f \colon A \to G(B)\), with morphisms \((B, f) \to (B', f')\) the maps \(h \colon B \to B'\) satisfying \(G(h) \circ f = f'\). This category has the unit \(\eta_A \colon A \to G(F(A))\) as an initial object, and \(G\) has a left adjoint exactly when each of these categories has an initial object. Combining this with a smallness condition gives the general adjoint functor theorem: if \(\mathcal{D}\) is locally small and has all small limits, and \(G\) preserves them and satisfies the solution set condition (for each \(A\) there is a set of arrows \(A \to G(B_i)\) through which every arrow \(A \to G(X)\) factors), then \(G\) has a left adjoint. Representable functors give another reading (see Yoneda embedding): \(F \dashv G\) says that for each object \(X\) of \(\mathcal{C}\), the covariant functor \(Y \mapsto \operatorname{Hom}(X, G(Y))\) is corepresented by \(F(X)\), that is, it is naturally isomorphic to \(Y \mapsto \operatorname{Hom}(F(X), Y)\).

In Mathlib

Mathlib takes the unit and counit with the triangle identities as the definition, and derives the hom-set bijection from them. Other constructors build an adjunction from a natural bijection of hom-sets, or build the adjoint functor itself from its values on objects together with suitable bijections of hom-sets. An adjunction is data, not a proposition: a pair of functors can carry several adjunction structures, and the theorems above about uniqueness, composition and equivalences are constructions producing specific natural isomorphisms and adjunctions. The mere existence of an adjoint is recorded separately as the property of being a left or a right adjoint, from which a chosen adjoint can be extracted. Preservation of limits is proved for limits indexed by categories of every size, not only small ones. Smallness in the adjoint functor theorem is measured relative to a universe level, which plays the role of the class of sets; in that statement the solution sets, the limits and the hom-sets of \(\mathcal{D}\) are all small with respect to the same level.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Adjunction
• Source of CategoryTheory.Adjunction in Mathlib/CategoryTheory/Adjunction/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Adjunction

Uses 3 · Used by 3

Statement usesCategory · Functor · Natural transformation

Used byCartesian closed · Beck's monadicity theorem · Mitchell's embedding theorem

StructureMonad#

A monad on a category \(\mathcal{C}\) is an endofunctor \(T\) of \(\mathcal{C}\) together with two natural transformations, a unit \(\eta \colon 1_{\mathcal{C}} \to T\) and a multiplication \(\mu \colon T T \to T\), subject to associativity and unit laws that mirror those of a monoid. Monads arise from every adjunction, and conversely every monad arises from one. They give a uniform language for algebraic structure: groups, monoids, modules and compact Hausdorff spaces can all be described as algebras for a suitable monad. In computer science, monads model computational effects such as failure, nondeterminism and state.

Definition

Let \(\mathcal{C}\) be a category. A monad on \(\mathcal{C}\) consists of a functor \(T \colon \mathcal{C} \to \mathcal{C}\) and natural transformations \(\eta \colon 1_{\mathcal{C}} \to T\) and \(\mu \colon T \circ T \to T\) such that for every object \(X\)

\[\mu_X \circ T(\mu_X) = \mu_X \circ \mu_{TX} \colon T^3 X \to TX,\]

\[\mu_X \circ \eta_{TX} = \mathrm{id}_{TX}, \qquad \mu_X \circ T(\eta_X) = \mathrm{id}_{TX}.\]

The first equation is associativity: the two ways of collapsing three layers of \(T\) to one agree. The other two are the unit laws.

A morphism of monads \(\theta \colon T \to S\) is a natural transformation compatible with the structure, meaning \(\theta_X \circ \eta^T_X = \eta^S_X\) and \(\theta_X \circ \mu^T_X = \mu^S_X \circ \theta_{SX} \circ T(\theta_X)\) for all \(X\). Dually, a comonad is an endofunctor with a counit \(T \to 1_{\mathcal{C}}\) and a comultiplication \(T \to T T\) satisfying the reversed laws.

Examples

• Lists. On the category of sets, let \(T(X)\) be the set of finite lists of elements of \(X\). The unit sends \(x\) to the one-element list, and the multiplication concatenates a list of lists into a single list. This is the monad of the free monoid construction.
• Power set. Let \(T(X)\) be the set of subsets of \(X\), with \(\eta_X(x) = \{x\}\) and \(\mu_X\) sending a family of subsets to its union.
• Maybe. Let \(T(X) = X \sqcup \{\ast\}\), with \(\eta\) the inclusion and \(\mu\) identifying the two added points.
• Ultrafilters. Sending a set to its set of ultrafilters gives a monad whose unit sends a point to the principal ultrafilter at it, and whose multiplication sends an ultrafilter \(\mathcal{U}\) on the set of ultrafilters on \(X\) to the ultrafilter of those subsets \(A \subseteq X\) for which the set of ultrafilters containing \(A\) belongs to \(\mathcal{U}\).
• The Giry monad. On measurable spaces, sending a space to the space of measures on it gives a monad whose unit sends a point to its Dirac measure and whose multiplication sends a measure \(m\) on the space of measures to the measure assigning to each measurable set \(s\) the value \(\int \nu(s) \, dm(\nu) \in [0, \infty]\), a Lebesgue integral of the function \(\nu \mapsto \nu(s)\).
• Programming. Every lawful monad in the sense of functional programming defines a monad on the category of types.

Adjunctions and algebras

Every adjunction gives a monad. If \(F \colon \mathcal{C} \to \mathcal{D}\) is left adjoint to \(G \colon \mathcal{D} \to \mathcal{C}\), with unit \(\eta\) and counit \(\varepsilon\), then \(GF\) is a monad on \(\mathcal{C}\) with unit \(\eta\) and multiplication \(G \varepsilon F\), and \(FG\) is a comonad on \(\mathcal{D}\). The free group functor and the forgetful functor from groups to sets, for instance, give the monad sending a set to the underlying set of the free group on it.

Algebras. An algebra for \(T\), also called an Eilenberg–Moore algebra, is an object \(A\) with a morphism \(a \colon TA \to A\) satisfying \(a \circ \eta_A = \mathrm{id}_A\) and \(a \circ \mu_A = a \circ T(a)\). A homomorphism \(f \colon (A, a) \to (B, b)\) is a morphism \(f \colon A \to B\) with \(f \circ a = b \circ T(f)\). Algebras and homomorphisms form a category \(\mathcal{C}^T\). For the list monad the algebras are exactly the monoids, for the power set monad they are the complete join-semilattices, and for the maybe monad they are the pointed sets. The algebras for the ultrafilter monad are the compact Hausdorff spaces: their category is equivalent to the category of compact Hausdorff spaces.

Every monad comes from an adjunction. Sending \(X\) to the free algebra \((TX, \mu_X)\) gives a functor that is left adjoint to the forgetful functor \(\mathcal{C}^T \to \mathcal{C}\), and the monad of this adjunction is isomorphic to \(T\). The forgetful functor reflects isomorphisms: a homomorphism of algebras whose underlying morphism is invertible is itself invertible.

The Kleisli category. A second adjunction comes from the Kleisli category of \(T\), whose objects are those of \(\mathcal{C}\) and whose morphisms \(X \to Y\) are morphisms \(X \to TY\) in \(\mathcal{C}\); the composite of \(f \colon X \to TY\) and \(g \colon Y \to TZ\) is \(\mu_Z \circ T(g) \circ f\). There is an adjunction between \(\mathcal{C}\) and the Kleisli category whose composite functor is naturally isomorphic to \(T\). For the maybe monad, Kleisli morphisms are partial functions. Consider the category whose objects are the adjunctions inducing \(T\) and whose morphisms are functors between their middle categories that commute with both the left and the right adjoints. In it the Kleisli adjunction is initial and the Eilenberg–Moore adjunction is terminal.

Monadic functors

Given an adjunction \(F \dashv G\) with \(G \colon \mathcal{D} \to \mathcal{C}\), each object \(Y\) of \(\mathcal{D}\) gives an algebra \((GY, G\varepsilon_Y)\) for the monad \(GF\), and this defines a comparison functor \(\mathcal{D} \to \mathcal{C}^{GF}\). The functor \(G\) is monadic when the comparison functor is an equivalence of categories (this does not depend on the choice of the left adjoint \(F\)), so that objects of \(\mathcal{D}\) are, up to equivalence, the algebras of the monad. The forgetful functors from groups, rings and modules to sets are monadic; the forgetful functor from topological spaces to sets is not, since its monad is the identity and its algebras are just sets. Beck's monadicity theorem characterizes monadic functors: a right adjoint \(G\) is monadic exactly when it reflects isomorphisms and \(\mathcal{D}\) has, and \(G\) preserves, coequalizers of those parallel pairs whose image under \(G\) has a split coequalizer.

Monads as monoids

The endofunctors of \(\mathcal{C}\) form a monoidal category with composition as the tensor product and the identity functor as the unit. A monad is precisely a monoid object there: \(\mu\) is the multiplication and \(\eta\) the unit. Accordingly, the category of monads on \(\mathcal{C}\) is equivalent to the category of monoid objects in the category of endofunctors of \(\mathcal{C}\).

In Mathlib

Mathlib bundles a monad as a structure extending an endofunctor with its unit and multiplication, and states the three laws one object at a time. Comonads are a separate structure, dual to monads. The category-theoretic notion is distinct from the monad type class of Lean's programming library; the two are linked by the construction above for lawful monads, and their Kleisli categories are equivalent. Being monadic is recorded as extra structure on a functor that includes a chosen left adjoint. Mathlib defines its category of compacta directly as the category of algebras for the ultrafilter monad on types, and then proves the equivalence with compact Hausdorff spaces. Its Giry monad uses all measures, not only probability measures.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Monad
• Source of CategoryTheory.Monad in Mathlib/CategoryTheory/Monad/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Monad

Uses 3 · Used by 1

Statement usesCategory · Functor · Natural transformation

Used byBeck's monadicity theorem

StructureComma category#

A comma category is a category built from two functors with a common target: its objects are morphisms from the image of the first functor to the image of the second, and its morphisms are commutative squares relating them. The construction packages many familiar categories in one definition, among them slice and coslice categories, arrow categories and categories of structured arrows, and it gives a uniform language for universal properties: a functor has a left adjoint exactly when certain comma categories have initial objects. The name comes from the comma in the notation \((L, R)\) for the comma category of \(L\) and \(R\); this article writes \((L \downarrow R)\), which is also common.

Definition

Let \(L \colon \mathcal A \to \mathcal T\) and \(R \colon \mathcal B \to \mathcal T\) be functors. The comma category \((L \downarrow R)\) has as objects the triples \((a, b, h)\) where \(a\) is an object of \(\mathcal A\), \(b\) is an object of \(\mathcal B\), and \(h \colon L(a) \to R(b)\) is a morphism of \(\mathcal T\). A morphism \((a, b, h) \to (a', b', h')\) is a pair \((f, g)\) of morphisms \(f \colon a \to a'\) in \(\mathcal A\) and \(g \colon b \to b'\) in \(\mathcal B\) such that the square

\[h' \circ L(f) = R(g) \circ h\]

commutes in \(\mathcal T\). Composition and identities are taken componentwise; the composite of two commutative squares placed side by side is again commutative, so this is a category.

Examples

• Slice categories. Take \(L\) to be the identity functor of a category \(\mathcal C\) and \(R\) the functor from the one-object category picking out an object \(X\). The result is the slice category \(\mathcal C / X\), whose objects are morphisms \(Y \to X\) and whose morphisms are morphisms \(Y \to Y'\) making the triangle over \(X\) commute. In it, the identity of \(X\) is a terminal object.
• Coslice categories. Exchanging the roles gives the coslice category \(X / \mathcal C\) of morphisms out of \(X\), in which the identity of \(X\) is an initial object. For instance, the category of commutative algebras over a commutative ring \(k\) is equivalent to the coslice category of commutative rings under \(k\): a commutative algebra over \(k\) is the same thing as a commutative ring together with a ring homomorphism from \(k\).
• Arrow categories. When both functors are the identity of \(\mathcal C\), the comma category is the arrow category of \(\mathcal C\): objects are morphisms of \(\mathcal C\) and morphisms are commutative squares.
• Structured arrows. For a functor \(G \colon \mathcal D \to \mathcal C\) and an object \(c\) of \(\mathcal C\), taking \(L\) to pick out \(c\) and \(R = G\) gives the category of structured arrows \((c \downarrow G)\), whose objects are pairs \((d, h)\) with \(h \colon c \to G(d)\). The dual construction, with morphisms \(G(d) \to c\), is the category of costructured arrows.
• Products. If \(\mathcal T\) is the category with one object and one morphism, every square commutes, and the comma category is equivalent to the product category \(\mathcal A \times \mathcal B\).

Properties

• Projections. There are forgetful functors \(P_1\) from \((L \downarrow R)\) to \(\mathcal A\) and \(P_2\) to \(\mathcal B\); the first is the projection \((a, b, h) \mapsto a\). The morphisms \(h\) themselves are the components of a natural transformation from \(L \circ P_1\) to \(R \circ P_2\).
• Duality. Reversing all arrows exchanges the two sides: \((L \downarrow R)\) is equivalent to the opposite of \((R^{\mathrm{op}} \downarrow L^{\mathrm{op}})\). In particular the coslice category of \(X\) in \(\mathcal C^{\mathrm{op}}\) is equivalent to the opposite of the slice category \(\mathcal C / X\).
• Limits. If \(\mathcal A\) and \(\mathcal B\) have all limits of a given shape \(J\) and \(R\) preserves them, then \((L \downarrow R)\) has all limits of shape \(J\); no condition on \(L\) is needed, and the limit is computed separately in each component. Slice categories also have limits that this theorem does not give: the functor picking out \(X\) does not preserve products, but if \(\mathcal C\) has pullbacks, then every slice category \(\mathcal C / X\) has binary products, the product of \(Y \to X\) and \(Z \to X\) being the pullback \(Y \times_X Z\) with its map to \(X\).
• Adjunctions. Universal arrows are initial objects of structured arrow categories. If \(F\) is left adjoint to \(G \colon \mathcal D \to \mathcal C\), then for each object \(c\) of \(\mathcal C\) the unit \(c \to G(F(c))\) is an initial object of \((c \downarrow G)\). Conversely, if every category \((c \downarrow G)\) has an initial object, then \(G\) has a left adjoint; see adjunction.

Related concepts

Slice categories over an object \(X\) of the category of topological spaces or of schemes are categories of spaces or schemes "over \(X\)", the setting of relative geometry, and coslice categories under a one-point set or space give pointed sets and pointed spaces. A presheaf \(P\) on \(\mathcal C\), viewed as a functor on \(\mathcal C^{\mathrm{op}}\), has a category of elements whose objects are the pairs \((c, x)\) with \(x \in P(c)\), and the opposite of this category of elements is equivalent to the category of costructured arrows from the Yoneda embedding to \(P\) (see Yoneda embedding). When the functors land in a 2-category, such as the 2-category of categories, one may allow the squares to commute only up to a specified 2-cell (a natural transformation, in the case of categories); this leads to lax comma constructions in higher category theory.

In Mathlib

Mathlib defines the comma category of two functors into a common category for categories in arbitrary universes, as a structure whose data are the two objects and the connecting morphism; morphisms are pairs of morphisms with the square condition as a field. Slice and coslice categories, arrow categories and the categories of structured and costructured arrows are not separate constructions but are defined as comma categories, with the one-object category represented by a discrete category on a one-element type. As a result, every general theorem about comma categories, such as the existence of limits and the duality equivalence, applies to all of these special cases at once.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Comma
• Source of CategoryTheory.Comma in Mathlib/CategoryTheory/Comma/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Comma

Uses 2

Statement usesCategory · Functor

StructureLimits#

A limit of a diagram in a category is an object equipped with morphisms to every object of the diagram, compatible with the arrows of the diagram, through which every other such compatible family factors in exactly one way. Products, equalizers, pullbacks, terminal objects and inverse limits are all special cases, so the single notion lets one state and prove facts about all of them at once. The dual notion, obtained by reversing every arrow, is a colimit.

Definition

A diagram of shape \(J\) in a category \(C\) is a functor \(F \colon J \to C\), where \(J\) is a category whose objects index the objects \(F(j)\) of the diagram. A cone over \(F\) with vertex \(X\) is a family of morphisms \(\pi_j \colon X \to F(j)\), one for each object \(j\) of \(J\), such that

\[F(u) \circ \pi_i = \pi_j \quad \text{for every morphism } u \colon i \to j \text{ in } J.\]

Equivalently, a cone is an object \(X\) together with a natural transformation from the constant functor at \(X\) to \(F\) (see natural transformation).

A cone \((L, \pi)\) is a limit cone if for every cone \((X, \sigma)\) over \(F\) there is a unique morphism \(h \colon X \to L\) with \(\pi_j \circ h = \sigma_j\) for all \(j\). The object \(L\) is then called a limit of \(F\).

A morphism of cones \((X, \sigma) \to (L, \pi)\) is a morphism \(h \colon X \to L\) with \(\pi_j \circ h = \sigma_j\) for all \(j\); cones over \(F\) and these morphisms form a category. An object of a category is terminal if every object has exactly one morphism to it. Said differently, then, a cone is a limit exactly when every cone admits exactly one cone morphism to it, that is, a limit cone is the same as a terminal object of the category of cones over \(F\).

Dually, a cocone consists of morphisms \(F(j) \to X\) compatible with the diagram, and a colimit cocone is one from which there is a unique compatible morphism to the vertex of every other cocone.

Examples

• Terminal objects. When \(J\) is empty, a cone is just an object, and an object is a limit of the empty diagram exactly when every object has exactly one morphism to it, that is, when it is a terminal object.
• Products. When \(J\) has no morphisms besides identities, a diagram is a family of objects, a cone over it is a family of morphisms from one object to each member of the family, and a product of the family is a limit cone; in particular the family has a product exactly when that diagram has a limit. In sets, the Cartesian product \(X \times Y\) with its two projections is a product of \(X\) and \(Y\).
• Equalizers. For two parallel maps \(f, g \colon Y \to Z\) of sets, the subset \(\{y \in Y : f(y) = g(y)\}\) with its inclusion is a limit of the pair, called their equalizer.
• Pullbacks. For maps \(f \colon X \to Z\) and \(g \colon Y \to Z\) of sets, the set \(\{(x, y) \in X \times Y : f(x) = g(y)\}\) with its two projections is a limit of the diagram formed by \(f\) and \(g\).
• Diagrams of sets in general. A compatible family for \(F \colon J \to \mathbf{Set}\) is a choice of \(x_j \in F(j)\) for every \(j\) with \(F(u)(x_i) = x_j\) for every \(u \colon i \to j\). A cone over \(F\) is a limit exactly when every compatible family is the image of exactly one element of its vertex. The ring of \(p\)-adic integers, for instance, is the limit of the rings \(\mathbb{Z}/p^n\mathbb{Z}\) along the reduction maps.
• Complete lattices. A partially ordered set is a category with one morphism \(a \to b\) when \(a \le b\). In a complete lattice, the infimum of the values of any diagram is its limit.

Dually, colimits include coproducts (disjoint unions of sets), coequalizers, pushouts, initial objects and direct limits.

Properties

• Uniqueness. Any two limit cones over the same diagram are isomorphic as cones, by the unique cone morphisms between them; in particular their vertices are isomorphic (see isomorphism). For this reason one speaks of "the" limit.
• Morphisms into a limit. Two morphisms into the vertex of a limit cone are equal when their composites with every projection \(\pi_j\) agree, and morphisms \(W \to L\) correspond bijectively to cones over \(F\) with vertex \(W\).
• Representability. The bijection above is natural in \(W\), so the vertex of a limit cone represents the functor sending \(W\) to the set of cones over \(F\) with vertex \(W\); conversely, a representing object of that functor is the vertex of a limit cone. This links limits to the Yoneda embedding.
• Construction from products and equalizers. For a diagram \(F\) indexed by a small category \(J\), if the product of all \(F(j)\) exists, the product of the objects \(F(j)\) indexed by the morphisms \(u \colon i \to j\) of \(J\) (one factor \(F(j)\) for each \(u\)) exists, and \(C\) has all equalizers, then \(F\) has a limit. The limit is the equalizer of two maps between these products.
• Sets are complete. Every diagram of sets has a limit, provided its indexing category has no more objects than a set (in Mathlib: its objects are in bijection with a type in the universe of the sets, see below); the limit is the set of compatible families.
• Adjoints. A functor with a left adjoint preserves all limits: it sends limit cones to limit cones. See adjunction.
• Functor categories. For a diagram of functors \(J \to (K \to C)\), a cone is a limit as soon as, for each object \(k\) of \(K\), its evaluation at \(k\) is a limit cone in \(C\), so limits of functors can be computed objectwise.

Related concepts

The category of cones over \(F\) is equivalent to the comma category of the diagonal functor \(C \to C^J\) over \(F\), so a limit is a terminal object of a comma category. Kernels in an abelian category are equalizers with a zero morphism, hence limits. The word "limit" also names a different notion in analysis and topology, the limit of a map along a filter; the two are not instances of one another in general.

In Mathlib

Mathlib defines being a limit as a structure on a cone that carries, for each other cone, the chosen factoring morphism, its compatibility, and its uniqueness. This is data rather than a mere proposition, but a cone carries at most one such structure. The mere existence of a limit is a separate property, the existence of some limit cone, and from it a limit object is picked by choice. Colimits are defined by their own dual structure rather than as limits in the opposite category. Size is tracked by universe levels, a hierarchy of ever larger collections of types, each type living in some universe: the indexing category and the hom-sets of \(C\) may live in different universes, and "having all limits" refers to indexing categories of a given size. For sets, Mathlib's instance asks only that the objects of the indexing category be in bijection with a type in the sets' universe; the size of its hom-sets does not matter. That condition is sufficient but not necessary: a diagram of sets has a limit exactly when its compatible families are in bijection with a type in the sets' universe. Mathlib writes composition in diagrammatic order, so its compatibility conditions read left to right.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Limits.IsLimit
• Source of CategoryTheory.Limits.IsLimit in Mathlib/CategoryTheory/Limits/IsLimit.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Limits.IsLimit

Uses 3 · Used by 5

Statement usesCategory · Functor · Natural transformation

Used byAbelian category · Cartesian closed · Small category · Functorial homology · Schur's lemma (1000+ theorems)

StructurePresheafed space#

A presheafed space is a topological space together with a presheaf on it, an assignment of an object of a fixed category \(\mathcal{C}\) to each open set, with restriction maps between them. It is a very general setting for "a space with functions on it", with the functions replaced by objects of an arbitrary category, and the structures of geometry are built from it by adding conditions: a sheafed space asks the presheaf to be a sheaf, a locally ringed space further asks for commutative rings with local stalks and for morphisms inducing local homomorphisms on stalks, and a scheme is a locally ringed space that is locally isomorphic to the spectrum of a commutative ring. Many constructions, such as gluing, colimits and restriction to open subsets, are simplest at the level of presheafed spaces, and the richer notions are often built from them by checking that the extra conditions survive.

Definition

Let \(\mathcal{C}\) be a category. For a topological space \(X\), the open sets of \(X\) ordered by inclusion form a category, and a presheaf on \(X\) with values in \(\mathcal{C}\) is a contravariant functor \(\mathcal{O}\) from it to \(\mathcal{C}\): it gives an object \(\mathcal{O}(U)\) for each open \(U\) and a restriction morphism \(\mathcal{O}(U) \to \mathcal{O}(V)\) whenever \(V \subseteq U\), compatible with composition and identities.

A presheafed space over \(\mathcal{C}\) is a pair \((X, \mathcal{O}_X)\) of a topological space \(X\) and a presheaf \(\mathcal{O}_X\) on \(X\) with values in \(\mathcal{C}\).

A continuous map \(f \colon X \to Y\) pushes a presheaf \(\mathcal{F}\) on \(X\) forward to the presheaf \(f_*\mathcal{F}\) on \(Y\) given by \((f_*\mathcal{F})(V) = \mathcal{F}(f^{-1}(V))\). A morphism of presheafed spaces \((X, \mathcal{O}_X) \to (Y, \mathcal{O}_Y)\) is a pair \((f, f^\#)\) of a continuous map \(f \colon X \to Y\) and a morphism of presheaves on \(Y\)

\[f^\# \colon \mathcal{O}_Y \to f_*\mathcal{O}_X,\]

called the comorphism of the morphism, that is, a natural transformation with components \(\mathcal{O}_Y(V) \to \mathcal{O}_X(f^{-1}(V))\). The map on spaces goes forward while the map on presheaves goes backward, as pulling back functions along a map does. Morphisms compose by \((g, g^\#) \circ (f, f^\#) = (g \circ f,\ g_*(f^\#) \circ g^\#)\), and with this composition presheafed spaces over \(\mathcal{C}\) form a category.

Examples

• Continuous functions. Any topological space \(X\) carries the presheaf of commutative rings sending \(U\) to the ring of continuous real-valued functions on \(U\), with restriction of functions as the restriction maps. A continuous map \(f \colon X \to Y\) gives a morphism whose comorphism sends a function \(h\) on \(V\) to \(h \circ f\) on \(f^{-1}(V)\).
• Manifolds and schemes. A smooth manifold with its presheaf of smooth functions, and the spectrum of a commutative ring with its structure sheaf, are presheafed spaces over commutative rings; in both cases the presheaf is in fact a sheaf.
• Constant presheaves. For a space \(X\) and an object \(Z\) of \(\mathcal{C}\), the presheaf with \(\mathcal{O}(U) = Z\) for every open \(U\) and identity restriction maps gives a presheafed space. It is not a sheaf unless \(Z\) is a terminal object, because the sheaf condition forces the value on the empty set to be terminal; this is a typical example of a presheafed space that is not a sheafed space.

Properties

• Underlying space. Forgetting the presheaf gives a functor to the category of topological spaces (see the category of topological spaces).
• Isomorphisms. If \(f\) is a homeomorphism and \(f^\#\) is an isomorphism of presheaves, then \((f, f^\#)\) is an isomorphism of presheafed spaces. Conversely, for an isomorphism of presheafed spaces the underlying continuous map is an isomorphism of spaces, that is, a homeomorphism, and the comorphism is an isomorphism of presheaves.
• Global sections. Sending \((X, \mathcal{O}_X)\) to \(\mathcal{O}_X(X)\) and \((f, f^\#)\) to the component of \(f^\#\) at \(Y\) defines a contravariant functor from presheafed spaces to \(\mathcal{C}\).
• Restriction. For an open embedding \(j \colon U \to X\), setting \(\mathcal{O}_U(V) = \mathcal{O}_X(j(V))\) gives the restriction of \((X, \mathcal{O}_X)\) to \(U\), which comes with a morphism to \((X, \mathcal{O}_X)\).
• Stalks. When \(\mathcal{C}\) has colimits, the stalk \(\mathcal{O}_{X,x}\) at a point \(x\) is the colimit of \(\mathcal{O}_X(U)\) over the open neighbourhoods \(U\) of \(x\), and a morphism \((f, f^\#)\) induces a morphism of stalks \(\mathcal{O}_{Y,f(x)} \to \mathcal{O}_{X,x}\). These maps are functorial: the stalk map of \(g \circ f\) at \(x\) is the stalk map of \(f\) at \(x\) composed after that of \(g\) at \(f(x)\). Restriction to an open subset does not change stalks: the morphism from a restriction induces isomorphisms on all stalks.
• Colimits. If \(\mathcal{C}\) has all limits, then the category of presheafed spaces over \(\mathcal{C}\) has all colimits, and the underlying space of a colimit is the colimit of the underlying spaces. The colimit presheaf is the limit of the pushforwards of the given presheaves to the colimit space. Applied to diagrams whose maps are open embeddings, this construction glues presheafed spaces.
• Change of values. A functor \(F \colon \mathcal{C} \to \mathcal{D}\) applied to every value of the presheaf gives a functor from presheafed spaces over \(\mathcal{C}\) to presheafed spaces over \(\mathcal{D}\); for instance, forgetting ring structure turns a presheaf of rings into a presheaf of sets.

Related concepts

A sheafed space is a presheafed space whose presheaf satisfies the sheaf condition: sections that agree on overlaps glue uniquely. Ringed spaces are sheafed spaces over commutative rings, locally ringed spaces are those whose stalks are local rings and whose morphisms induce local homomorphisms on stalks, and schemes are a further special case. Each of these notions keeps the morphisms of presheafed spaces, adding at most a condition on them.

In Mathlib

Mathlib bundles a presheafed space as an object of the category of topological spaces together with a presheaf on it, where a presheaf is a functor out of the opposite of the category of open sets. The value category is arbitrary. A morphism stores the continuous map and the comorphism into the pushforward, in the direction used above. Two morphisms with the same underlying continuous map can differ in their comorphisms, so Mathlib deliberately gives presheafed spaces no structure of a concrete category over sets. Restriction is defined along any open embedding, not only the inclusion of an open subset. For the results on stalks and colimits, the points of the spaces are taken in the same universe as the morphisms of \(\mathcal{C}\), and "all limits" and "all colimits" mean those indexed by categories of that size. Sheafed spaces and locally ringed spaces are built as extensions of this structure, so the constructions above apply to their underlying presheafed spaces; Mathlib provides separate versions of restriction and colimits that stay within the richer categories.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: AlgebraicGeometry.PresheafedSpace
• Source of AlgebraicGeometry.PresheafedSpace in Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
• Mathlib overview: General algebra › Category theory

MathlibAlgebraicGeometry.PresheafedSpace

Uses 5 · Used by 1

Statement usesTopological space · Continuous function · Category · Functor · Natural transformation

Used bySheafed space

StructureSheafed space#

A sheafed space is a topological space together with a sheaf on it with values in a fixed category \(\mathcal{C}\): an object of \(\mathcal{C}\) for each open set, with restriction maps, such that data given locally on an open cover and agreeing on overlaps glue uniquely. It is the common frame for spaces described by their local functions. Smooth manifolds with their smooth functions, and spectra of commutative rings with their structure sheaves, are sheafed spaces over commutative rings. The sheafed spaces over commutative rings are the ringed spaces, and locally ringed spaces and schemes are ringed spaces with further conditions.

Definition

Let \(\mathcal{C}\) be a category and \(X\) a topological space. A presheaf \(\mathcal{F}\) on \(X\) with values in \(\mathcal{C}\) assigns to each open set \(U\) an object \(\mathcal{F}(U)\) and to each inclusion \(V \subseteq U\) a restriction morphism \(\mathcal{F}(U) \to \mathcal{F}(V)\), compatibly with identities and composition. When \(\mathcal{C}\) is the category of sets, or of groups or rings, elements of \(\mathcal{F}(U)\) are called sections over \(U\), and the restriction of a section \(s\) to \(V\) is written \(s|_V\).

Such a presheaf is a sheaf if, for every open set \(U\) and every cover \(U = \bigcup_i U_i\) by open sets, each family of sections \(s_i \in \mathcal{F}(U_i)\) that is compatible, meaning

\[s_i|_{U_i \cap U_j} = s_j|_{U_i \cap U_j} \quad \text{for all } i, j,\]

comes from exactly one section \(s \in \mathcal{F}(U)\) with \(s|_{U_i} = s_i\) for every \(i\). For presheaves of sets, Mathlib's sheaf condition is equivalent to this unique gluing condition. For a general category \(\mathcal{C}\) there are no elements to glue, and the condition is imposed on morphisms instead: for every object \(A\) of \(\mathcal{C}\), the presheaf of sets \(U \mapsto \mathrm{Hom}(A, \mathcal{F}(U))\) must satisfy unique gluing. When \(\mathcal{C}\) has products, this says that \(\mathcal{F}(U)\) is the equalizer of the two restriction maps from \(\prod_i \mathcal{F}(U_i)\) to \(\prod_{i,j} \mathcal{F}(U_i \cap U_j)\).

A sheafed space over \(\mathcal{C}\) is a presheafed space \((X, \mathcal{O}_X)\) whose presheaf \(\mathcal{O}_X\) is a sheaf. A morphism \((X, \mathcal{O}_X) \to (Y, \mathcal{O}_Y)\) is a pair \((f, f^\#)\) of a continuous map \(f \colon X \to Y\) and a morphism of presheaves

\[f^\# \colon \mathcal{O}_Y \to f_*\mathcal{O}_X, \qquad (f_*\mathcal{O}_X)(V) = \mathcal{O}_X(f^{-1}(V)),\]

so no condition is added to morphisms: forgetting the sheaf condition is a fully faithful functor from sheafed spaces to presheafed spaces. The sheafed spaces over commutative rings are called ringed spaces.

Examples

• Continuous functions. For spaces \(X\) and \(T\), sending an open set \(U \subseteq X\) to the set of continuous maps \(U \to T\) gives a sheaf of sets on \(X\): continuous maps that agree on overlaps glue to a unique continuous map, because continuity is a local property.
• Smooth manifolds. On a smooth manifold \(M\), the smooth functions on open subsets with values in a fixed smooth commutative ring, such as \(\mathbb{R}\), form a sheaf of commutative rings, which makes \(M\) a ringed space.
• Spectra of rings. The prime spectrum of a commutative ring \(R\), with its Zariski topology and structure sheaf, is a sheafed space over commutative rings. A ring homomorphism \(R \to S\) induces a morphism in the opposite direction, from the spectrum of \(S\) to that of \(R\), and this makes the spectrum a contravariant functor from commutative rings to sheafed spaces.
• The trivial sheaf. Over the category with one object and one morphism, every presheaf is a sheaf, so any topological space becomes a sheafed space over that category.

The empty set is covered by the empty family, and gluing the empty family uniquely forces the value of a sheaf on the empty set to be a terminal object. So a presheaf whose value on the empty set is not terminal, such as a constant presheaf with value a nonzero ring, is not a sheaf.

Properties

• Underlying space and global sections. Forgetting the sheaf gives a functor to the category of topological spaces (see the category of topological spaces), and taking sections over the whole space gives a contravariant functor to \(\mathcal{C}\).
• Restriction. The restriction of a sheaf to an open subset is again a sheaf, so for an open embedding \(j \colon U \to X\) the presheafed space restriction is a sheafed space on \(U\), and restricting to all of \(X\) gives back \((X, \mathcal{O}_X)\) up to isomorphism.
• Stalks determine sections and morphisms. Suppose \(\mathcal{C}\) is a category of algebraic structures such as sets, abelian groups or commutative rings; precisely, a concrete category with all limits and colimits whose forgetful functor to sets preserves limits and filtered colimits and reflects isomorphisms. Then two sections of a sheaf over \(U\) are equal if their germs agree at every point of \(U\). Consequently, two morphisms of sheafed spaces are equal if they have the same continuous map and induce the same maps on all stalks. Under the same hypotheses, a morphism whose continuous map is injective and whose maps on stalks are epimorphisms is a monomorphism, and a morphism whose continuous map is surjective and whose maps on stalks are monomorphisms is an epimorphism.
• Colimits. When \(\mathcal{C}\) has all limits, colimits of sheafed spaces exist and are formed as for presheafed spaces, since a limit of sheaves is a sheaf; gluing sheafed spaces along open subsets is a special case.

Related concepts

A presheafed space drops the sheaf condition. A locally ringed space is a ringed space whose stalks are local rings, with morphisms required to induce local homomorphisms on stalks, and a scheme is a locally ringed space that is covered by open pieces isomorphic to spectra of commutative rings. On the other side, the sheaf condition on a topological space is the special case, for the open sets of \(X\) and their open covers, of the sheaf condition for a Grothendieck topology.

In Mathlib

Mathlib defines a sheafed space as a presheafed space carrying a proof that its presheaf is a sheaf, with the value category arbitrary. Its official sheaf condition is the one for the Grothendieck topology of open covers on the open sets of the space, phrased through morphisms out of each object of \(\mathcal{C}\) as above, so it needs no limits in \(\mathcal{C}\); the unique gluing and equalizer formulations are theorems with their own hypotheses. The category of sheafed spaces is defined as the full subcategory of presheafed spaces it determines, and ringed spaces are not a separate structure but the case of commutative rings. Restriction is taken along any open embedding, not only the inclusion of an open subset. In the equalizer formulation, the products are indexed by types of the same size as the points of the space. The stalk results require the points of the space to live in the same universe as the morphisms of \(\mathcal{C}\). Colimits of sheafed spaces are provided as instances, created by the forgetful functor to presheafed spaces, for sheafed spaces whose points live in that universe and for diagrams of that size.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: AlgebraicGeometry.SheafedSpace
• Source of AlgebraicGeometry.SheafedSpace in Mathlib/Geometry/RingedSpace/SheafedSpace.lean
• Mathlib overview: General algebra › Category theory

MathlibAlgebraicGeometry.SheafedSpace

Uses 5 · Used by 1

Statement usesPresheafed space · Topological space · Category · Functor · Continuous function

Used byLocally ringed space

ClassMonoidal category#

A monoidal category is a category equipped with a way of multiplying objects, a tensor product \(X \otimes Y\), together with a unit object \(I\), such that the product is associative and unital up to specified, well-behaved isomorphisms. The notion abstracts the cartesian product of sets, the tensor product of vector spaces and the composition of functors, and it is the setting in which one can speak of monoids and algebras inside a category rather than only among sets.

Definition

A monoidal structure on a category \(\mathcal{C}\) consists of

• a tensor product, which assigns to objects \(X, Y\) an object \(X \otimes Y\) and to morphisms \(f \colon X \to X'\) and \(g \colon Y \to Y'\) a morphism \(f \otimes g \colon X \otimes Y \to X' \otimes Y'\);
• a unit object \(I\);
• an associator, an isomorphism \(\alpha_{X,Y,Z} \colon (X \otimes Y) \otimes Z \to X \otimes (Y \otimes Z)\) for all objects \(X, Y, Z\);
• left and right unitors, isomorphisms \(\lambda_X \colon I \otimes X \to X\) and \(\rho_X \colon X \otimes I \to X\).

The tensor product must respect identities and composition, \(1_X \otimes 1_Y = 1_{X \otimes Y}\) and \((g_1 \circ f_1) \otimes (g_2 \circ f_2) = (g_1 \otimes g_2) \circ (f_1 \otimes f_2)\), so that it is a functor from \(\mathcal{C} \times \mathcal{C}\) to \(\mathcal{C}\) (here \(\mathcal{C} \times \mathcal{C}\) is the product category, whose objects and morphisms are pairs). The associator and unitors must be natural transformations; for the associator this means \(\alpha_{X',Y',Z'} \circ ((f \otimes g) \otimes h) = (f \otimes (g \otimes h)) \circ \alpha_{X,Y,Z}\) for all morphisms \(f \colon X \to X'\), \(g \colon Y \to Y'\), \(h \colon Z \to Z'\). Finally, two coherence conditions must hold. The pentagon identity says that the two ways of rebracketing \(((W \otimes X) \otimes Y) \otimes Z\) into \(W \otimes (X \otimes (Y \otimes Z))\) agree:

\[(1_W \otimes \alpha_{X,Y,Z}) \circ \alpha_{W,X \otimes Y,Z} \circ (\alpha_{W,X,Y} \otimes 1_Z) = \alpha_{W,X,Y \otimes Z} \circ \alpha_{W \otimes X,Y,Z}.\]

The triangle identity says that the two ways of removing the unit from \((X \otimes I) \otimes Y\) agree:

\[(1_X \otimes \lambda_Y) \circ \alpha_{X,I,Y} = \rho_X \otimes 1_Y.\]

Examples

• Sets. The category of types, which plays the role of sets, is monoidal with the cartesian product \(X \times Y\) as tensor product and a one-element set as unit.
• Finite products. More generally, every category with finite products is monoidal, with the binary product as tensor product and a terminal object as unit. Dually, finite coproducts and an initial object give a monoidal structure.
• Modules. For a commutative ring \(R\), the category of \(R\)-modules is monoidal under the tensor product over \(R\), with unit \(R\) (see tensor product). Vector spaces over a field \(K\) are the case \(R = K\).
• Monoids. A monoid \(M\) can be read as a discrete monoidal category: the objects are the elements of \(M\), the only morphisms are identities, the tensor product is the multiplication and the unit is \(1\).
• Endofunctors. For any category \(\mathcal{C}\), the functors from \(\mathcal{C}\) to itself form a monoidal category under composition, with the identity functor as unit. This tensor product is in general not commutative, even up to isomorphism.

Properties

The left and right unitors of the unit object coincide, \(\lambda_I = \rho_I\) as maps \(I \otimes I \to I\). Tensoring with identities on either side commutes: for \(f \colon W \to X\) and \(g \colon Y \to Z\), the two orders agree,

\[(f \otimes 1_Z) \circ (1_W \otimes g) = (1_X \otimes g) \circ (f \otimes 1_Y),\]

and both equal \(f \otimes g\). The endomorphisms of the unit object form a commutative monoid under composition. Transported along \(\lambda_I = \rho_I\), the tensor product of two such endomorphisms is a second multiplication with the same unit \(1_I\) that satisfies the interchange law with composition, and an Eckmann–Hilton argument shows that the two multiplications agree and are commutative.

The central structural fact is the coherence theorem. Its formal version says that in the free monoidal category generated by a collection of objects, any two morphisms with the same source and target are equal. Consequently, in any monoidal category, two morphisms built from associators, unitors, their inverses and identities by composition and tensor product agree whenever they relate the same two formal bracketed words. This licenses the common practice of omitting brackets and units from tensor products. Every monoidal category is also equivalent, through monoidal functors, to a strict one, in which the associators and unitors are identities.

Related concepts

• A monoid object is an object \(M\) with a multiplication \(M \otimes M \to M\) and a unit \(I \to M\) satisfying associativity and unit laws. Monoid objects in sets under the cartesian product are monoids, in abelian groups under the tensor product they are rings, in \(R\)-modules under the tensor product over \(R\) they are \(R\)-algebras, and among endofunctors they are monads.
• A monoidal functor preserves the tensor product and unit up to coherent isomorphism; a lax monoidal functor comes only with comparison maps \(F(X) \otimes F(Y) \to F(X \otimes Y)\) and \(I \to F(I)\), natural and compatible with the associators and unitors, which need not be invertible.
• A braided monoidal category adds a natural isomorphism \(X \otimes Y \cong Y \otimes X\) satisfying two hexagon identities, and a symmetric monoidal category is a braided one in which swapping twice is the identity. Sets and modules over a commutative ring are symmetric.
• A monoidal category is monoidal closed when each functor \(X \otimes -\) has a right adjoint, an internal hom. For the monoidal structure given by finite products this is a cartesian closed category.

In Mathlib

Mathlib treats a monoidal structure as data on a category, not as a property: the tensor product, the unit object, the associator and both unitors are specified, and a category may carry several monoidal structures. Alongside the tensor product of morphisms, Mathlib takes as basic the two whiskerings, tensoring a morphism with an identity on the left or on the right, and requires the tensor product of two morphisms to equal a whiskering on the right followed by one on the left; most of the axioms are stated in terms of whiskerings. The category of types stands in for the category of sets, and its cartesian structure, like that of any category with finite products, comes with a chosen product and terminal object. Mathlib writes composition of functors in diagrammatic order, so in its monoidal category of endofunctors the tensor product of \(F\) and \(G\) applies \(F\) first; this is the reverse of the usual convention, and Mathlib's structure is the monoidal opposite of the one common in the literature. The coherence theorem is formalized as the statement that the free monoidal category on any type has at most one morphism between any two objects; the strictification theorem is not formalized.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.MonoidalCategory
• Source of CategoryTheory.MonoidalCategory in Mathlib/CategoryTheory/Monoidal/Category.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.MonoidalCategory

Uses 4 · Used by 1

Statement usesCategory · Functor · Natural transformation · Isomorphism

Used byCartesian closed

ClassCartesian closed#

A cartesian closed category is a category with finite products in which, for any two objects \(A\) and \(B\), there is an object \(B^A\) of "morphisms from \(A\) to \(B\)" that behaves like a function space: morphisms \(A \times Y \to B\) correspond exactly to morphisms \(Y \to B^A\). The category of sets is the basic example, with \(B^A\) the set of all functions. Cartesian closed categories are a natural setting for currying functions of several variables, which is why they serve as models of the simply typed lambda calculus, and every topos is one.

Definition

Let \(C\) be a category with finite products, that is, with a terminal object \(1\) and a product \(A \times Y\) for every pair of objects. An object \(A\) is called exponentiable if the functor \(Y \mapsto A \times Y\) has a right adjoint, written \(X \mapsto X^A\). Spelled out, there is a bijection

\[\operatorname{Hom}(A \times Y, X) \cong \operatorname{Hom}(Y, X^A),\]

natural in \(X\) and \(Y\). The map from left to right is called currying and its inverse uncurrying. The object \(X^A\) is the exponential, or internal hom, and the morphism \(A \times X^A \to X\) corresponding to the identity of \(X^A\) is evaluation. The category \(C\) is cartesian closed if every object is exponentiable.

This is the special case of a closed monoidal category in which the tensor product is the categorical product: a monoidal category is monoidal closed when every object is closed, meaning that tensoring with it on the left has a right adjoint, called its internal hom functor. For a general tensor product the same definition yields currying and uncurrying, and uncurrying undoes currying while currying undoes uncurrying.

Examples

• Sets. In the category of sets, taking the product with \(X\) is left adjoint to the functor of functions out of \(X\): a function of two variables \(X \times Y \to Z\) is the same as a function from \(Y\) to the set of functions \(X \to Z\).
• Presheaves. For any small category \(D\), the category of functors from \(D\) to sets, with the pointwise product, is cartesian closed. Mathlib proves this without smallness, for functors into any universe of sets at least as large as the objects and morphisms of \(D\). Applied to the opposite category, this covers presheaves; applied to a group viewed as a one-object category, it shows that the category of sets with an action of a group is cartesian closed.
• Preorders and posets. A preordered set, viewed as a category, is cartesian closed exactly when it has a greatest element, binary meets, and for each \(a, b\) an element \(a \Rightarrow b\) with \(c \le (a \Rightarrow b)\) if and only if \(c \wedge a \le b\). A lattice with a least element and this structure is a Heyting algebra; every Boolean algebra is one.
• Non-examples. The category of topological spaces is not cartesian closed. Neither is the category of vector spaces over a field, although it is monoidal closed for the tensor product: it has a zero object, and in a cartesian closed category with a zero object every hom-set has exactly one element, so such a category is equivalent to the category with one object and one morphism. In particular a nontrivial abelian category is never cartesian closed.

Properties

• Since \(A \times (-)\) is a left adjoint, it preserves all colimits that exist. In particular products distribute over coproducts, \(A \times (B + B') \cong (A \times B) + (A \times B')\), and the product of \(A\) with an initial object \(0\) is initial.
• Initial objects are strict: every morphism from an exponentiable object into an initial object is an isomorphism. Consequently every morphism out of an initial object is a monomorphism.
• The usual laws of exponents hold up to natural isomorphism, for instance \((X^B)^A \cong X^{A \times B}\) and \((X \times X')^A \cong X^A \times X'^A\). For the terminal object, the exponential \(X^1\) is isomorphic to \(X\).
• Being cartesian closed is invariant under equivalence: a category with finite products that is equivalent to a cartesian closed category is cartesian closed.
• A full subcategory \(D\) of a cartesian closed category \(C\), closed under isomorphism, is called an exponential ideal if \(X^A\) lies in \(D\) whenever \(X\) lies in \(D\), for every object \(A\) of \(C\). If \(D\) is moreover reflective, then it is again cartesian closed, with any choice of finite products.

Generalizations

Replacing the product by an arbitrary tensor product gives closed monoidal categories, whose internal homs include the space of linear maps between vector spaces, or between modules over a commutative ring. Locally cartesian closed categories ask that every slice category be cartesian closed; toposes are cartesian closed categories with finite limits and a subobject classifier.

In Mathlib

Mathlib has no separate class for cartesian closed categories: a cartesian closed category is a category carrying a chosen cartesian monoidal structure (a chosen terminal object and chosen binary products, used as the tensor product) together with a monoidal closed structure. The closed structure is data rather than a property: each object comes with a specified right adjoint, unique only up to isomorphism. The convention is right closedness, adjoining on the side of \(A \otimes Y\) as above; for a cartesian product the two sides agree up to the symmetry of the product. Several basic results are stated with weaker hypotheses than full cartesian closedness, for instance the strictness of initial objects, which needs only the one object to be exponentiable. Likewise, exponential ideals are defined for an arbitrary functor into \(C\), an object counting as lying in the subcategory when it is isomorphic to an image of that functor.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.MonoidalClosed
• Source of CategoryTheory.MonoidalClosed in Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.MonoidalClosed

Uses 5

Statement usesCategory · Functor · Adjunction · Limits · Monoidal category

ClassAbelian category#

An abelian category is a category whose morphisms can be added and in which kernels, cokernels, images and exact sequences behave as they do for modules over a ring. The notion isolates the formal properties of abelian groups and modules that homological algebra actually uses, so that constructions such as chain complexes, homology and derived functors can be carried out once, uniformly, for modules, sheaves, representations and many other settings.

Definition

A category \(\mathcal{A}\) is abelian when it satisfies the following conditions.

1. It is preadditive: every set of morphisms \(\mathrm{Hom}(X, Y)\) carries the structure of an abelian group, and composition is additive in each variable, so that \((f + f') \circ g = f \circ g + f' \circ g\) and \(h \circ (f + f') = h \circ f + h \circ f'\).
2. It has all finite products, including the empty product, which is a terminal object.
3. Every morphism has a kernel and a cokernel.
4. Every monomorphism is the kernel of some morphism, and every epimorphism is the cokernel of some morphism.

In a preadditive category a terminal object is also initial, so an abelian category has a zero object, and its finite products are at the same time coproducts: an abelian category has finite biproducts, usually written as direct sums \(X \oplus Y\).

For a morphism \(f \colon X \to Y\), the image of \(f\) is the kernel of its cokernel and the coimage is the cokernel of its kernel. The morphism factors as \(X \to \operatorname{coim} f \to \operatorname{im} f \to Y\), and in an abelian category the middle map is a canonical isomorphism from the coimage to the image. This gives an equivalent definition: a preadditive category with kernels, cokernels and finite products in which the comparison from coimage to image is always an isomorphism is abelian.

A sequence \(X \xrightarrow{f} Y \xrightarrow{g} Z\) with \(g \circ f = 0\) is exact at \(Y\) when the image of \(f\) and the kernel of \(g\) are the same subobject of \(Y\). For modules this is the familiar condition that the range of \(f\) equals the kernel of \(g\).

Examples

• For any ring \(R\), commutative or not, the category of \(R\)-modules is abelian. Taking \(R = \mathbb{Z}\) gives the category of abelian groups, and taking \(R\) a field gives vector spaces. Kernels and cokernels are the usual kernel and quotient by the range.
• If \(\mathcal{A}\) is abelian and \(\mathcal{C}\) is any category, then the category of functors from \(\mathcal{C}\) to \(\mathcal{A}\) is abelian, with kernels and cokernels computed objectwise. In particular presheaves of abelian groups form an abelian category.
• If \(\mathcal{A}\) is abelian, then for a Grothendieck topology on a category for which sheafification with values in \(\mathcal{A}\) exists, the category of sheaves with values in \(\mathcal{A}\) is abelian. The classical case is sheaves of abelian groups on a topological space.
• The opposite of an abelian category is abelian: the opposite of a preadditive category is preadditive, and the other conditions turn into their duals, which abelian categories also satisfy. Chain complexes in an abelian category again form an abelian category.

Not every additive setting is abelian. In the category of free abelian groups, multiplication by \(2\) on \(\mathbb{Z}\) is both a monomorphism and an epimorphism but has no inverse, which is impossible in an abelian category (see below). The category of all groups is not abelian either: the trivial group is a zero object, but for nontrivial groups \(G\) and \(H\) the product \(G \times H\) is not a coproduct (the coproduct is the free product \(G * H\)), whereas in an abelian category finite products and coproducts coincide.

Properties

• A morphism that is both a monomorphism and an epimorphism is an isomorphism; in other words, abelian categories are balanced, where a category is balanced when every morphism that is both a monomorphism and an epimorphism is an isomorphism.
• An abelian category has all finite limits and all finite colimits (see limits).
• The pullback of an epimorphism along any morphism is an epimorphism, and dually the pushout of a monomorphism along any morphism is a monomorphism.
• Exactness as defined above agrees with the homological definition: for \(X \xrightarrow{f} Y \xrightarrow{g} Z\) with \(g \circ f = 0\), the homology at \(Y\) vanishes exactly when the image of \(f\) and the kernel of \(g\) are the same subobject of \(Y\).
• The standard diagram lemmas hold. The five lemma says that, given a map between two exact rows of five objects whose first component is an epimorphism, whose second and fourth are isomorphisms and whose fifth is a monomorphism, the middle component is an isomorphism. The snake lemma says that a map from an exact row \(A \to B \to C \to 0\) to an exact row \(0 \to A' \to B' \to C'\), with vertical maps \(a\), \(b\), \(c\), gives an exact sequence $\(\ker a \to \ker b \to \ker c \to \operatorname{coker} a \to \operatorname{coker} b \to \operatorname{coker} c.\)$

Many such arguments are first checked with elements in module categories and then transferred. Mitchell's embedding theorem justifies this: every abelian category admits a fully faithful functor into the modules over some ring that preserves finite limits and finite colimits, so it is equivalent to a full subcategory of a module category, compatibly with kernels, cokernels and exactness.

In Mathlib

Mathlib defines an abelian category as a structure placed on a category, extending its preadditive structure, rather than as a property of the category. A category usually comes with its own addition of morphisms, and requiring this addition as data lets each example supply it directly. Exactness is defined for any category with zero morphisms, by the vanishing of homology, and in an abelian category it agrees with the condition on images and kernels above. That abelian categories are balanced is likewise not stated in one place but derived in steps: every epimorphism in an abelian category is normal, hence regular, hence strong, and a category in which every epimorphism is strong is balanced. Mathlib also shows that the addition is not extra information in principle: a category with a zero object, and hence zero morphisms, with finite products and coproducts, kernels and cokernels, in which every monomorphism and every epimorphism is normal, carries an abelian structure, the addition being constructed from the other axioms. Mathlib's embedding theorem needs no smallness hypothesis on the category: the ring and its modules are taken in a universe large enough to contain the objects of the category, whereas textbook statements usually assume a small category.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.Abelian
• Source of CategoryTheory.Abelian in Mathlib/CategoryTheory/Abelian/Basic.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.Abelian

Uses 3 · Used by 2

Statement usesCategory · Group · Limits

Used byFunctorial homology · Mitchell's embedding theorem

StructureGrothendieck topology#

A Grothendieck topology on a category specifies, for each object, which collections of morphisms into it count as coverings of that object. It abstracts the way the open subsets of a topological space cover larger open sets, keeping only the formal properties that the notion of a sheaf needs. A category equipped with a Grothendieck topology is called a site, and sheaves on sites are the setting for étale cohomology, for descent theory and for topos theory.

Definition

Let \(C\) be a category and \(X\) an object of \(C\). A sieve on \(X\) is a collection \(S\) of morphisms with target \(X\) that is closed under precomposition: if \(f \colon Y \to X\) lies in \(S\), then so does \(f \circ g\) for every morphism \(g \colon Z \to Y\). The maximal sieve on \(X\) consists of all morphisms into \(X\). For a morphism \(h \colon Y \to X\), the pullback of \(S\) along \(h\) is the sieve on \(Y\)

\[h^*S = \{\, g \colon Z \to Y \;:\; h \circ g \in S \,\}.\]

A Grothendieck topology \(J\) on \(C\) assigns to each object \(X\) a set \(J(X)\) of sieves on \(X\), the covering sieves, subject to three axioms:

1. the maximal sieve on \(X\) belongs to \(J(X)\);
2. if \(S \in J(X)\) and \(h \colon Y \to X\), then \(h^*S \in J(Y)\);
3. if \(S \in J(X)\) and \(R\) is a sieve on \(X\) such that \(h^*R \in J(Y)\) for every \(h \colon Y \to X\) in \(S\), then \(R \in J(X)\).

The first axiom says that the identity of \(X\) alone covers \(X\), the second that coverings restrict, and the third that a sieve which covers locally on a covering covers outright.

A presheaf of sets on \(C\) is a functor \(P\) from the opposite category of \(C\) to sets. It is a sheaf for \(J\) when, for every covering sieve \(S\) on \(X\), each compatible family of elements \(x_f \in P(Y)\), one for each \(f \colon Y \to X\) in \(S\), comes from exactly one element \(t \in P(X)\), in the sense that \(P(f)(t) = x_f\) for all \(f\). Here compatible means that \(P(g)(x_f) = x_{f \circ g}\) for every \(f\) in \(S\) and every \(g \colon Z \to Y\); because \(S\) is a sieve, this is equivalent to the pairwise condition that \(P(g_1)(x_{f_1}) = P(g_2)(x_{f_2})\) whenever \(f_1 \circ g_1 = f_2 \circ g_2\), which is the form Mathlib uses. Sheaves form a category of their own.

Examples

• Open covers. The open subsets of a topological space \(T\), ordered by inclusion, form a category with a morphism \(V \to U\) exactly when \(V \subseteq U\). In the topology of open covers, a sieve on \(U\) covers when every point of \(U\) lies in some open \(V\) belonging to the sieve. For presheaves of sets, being a sheaf for this topology is the same as the classical gluing condition: every family of sections over a family of open sets that agree on pairwise intersections glues to a unique section over their union.
• Trivial and discrete topologies. In the trivial topology only the maximal sieves cover; it is the least topology, and for it every presheaf is a sheaf. In the discrete topology every sieve covers, including the empty one.
• Dense topology. In the dense topology a sieve \(S\) on \(X\) covers when every morphism \(f \colon Y \to X\) can be precomposed with some \(g \colon Z \to Y\) so that \(f \circ g\) lies in \(S\).
• Atomic topology. If any two morphisms with a common target can be completed to a commuting square, which holds in every category with pullbacks, then the nonempty sieves form the atomic topology.
• Canonical topology. The canonical topology is the finest topology for which every representable presheaf is a sheaf (see Yoneda embedding), where finest means having the most covering sieves: each representable presheaf is a sheaf for it, and any topology for which every representable presheaf is a sheaf is coarser than it. Topologies coarser than the canonical one are called subcanonical.
• Schemes. On the category of schemes, jointly surjective families of open immersions generate the Zariski topology, and jointly surjective families of étale morphisms generate the étale topology, which is finer than the Zariski topology: every Zariski-covering sieve is étale-covering.

Properties

A sieve containing a covering sieve is itself covering: if \(S \subseteq R\) and \(S\) covers, apply the third axiom to \(S\) and \(R\), using that \(h\) lies in a sieve exactly when the pullback of that sieve along \(h\) is maximal. The intersection of two sieves covers exactly when both of them do, so the covering sieves on each object are closed under enlargement and under finite intersections.

Topologies on a fixed category are ordered by inclusion: \(J \le K\) means that every \(J\)-covering sieve is \(K\)-covering, and \(K\) is then called finer. The intersection of any family of topologies is again a topology, so the topologies on \(C\) form a complete lattice, with the trivial topology as its least element and the discrete topology as its greatest. Refining a topology can only shrink the class of sheaves: a sheaf for a finer topology is a sheaf for a coarser one.

Topologies are rarely written down sieve by sieve. In a category with pullbacks, a pretopology prescribes covering families directly, and a sieve is declared covering when it contains a covering family. More generally, a coverage, a choice of covering families required only to be compatible with pullback, generates a topology by closing up under the axioms.

Related concepts

On a site whose underlying category is small, the inclusion of sheaves of sets into presheaves has a left adjoint, sheafification, which preserves finite limits. A category equivalent to the category of sheaves of sets on a small site is a Grothendieck topos. The sheaves used in sheafed spaces are sheaves for the topology of open covers.

In Mathlib

Mathlib follows the saturated convention: a topology is a bundled structure that lists covering sieves together with the three axioms, rather than covering families, and families enter only through precoverages, pretopologies and coverages. A precoverage is just a choice of covering families on each object, with no axioms, and it generates a topology, the smallest one in which the sieve generated by each covering family covers; the Zariski and étale topologies on schemes are produced this way. No smallness is assumed, so the category of all schemes carries its topologies directly. The names follow one common convention: the trivial topology, also called indiscrete, is the least, and the discrete topology is the greatest. Sheaves are defined for presheaves with values in any category, by asking that each functor of morphisms from a fixed object into the presheaf be a sheaf of sets.

Written for Trough, under CC BY-SA 4.0.

Sources

• Mathlib documentation: CategoryTheory.GrothendieckTopology
• Source of CategoryTheory.GrothendieckTopology in Mathlib/CategoryTheory/Sites/Grothendieck.lean
• Mathlib overview: General algebra › Category theory

MathlibCategoryTheory.GrothendieckTopology

Uses 3 · Used by 1

Statement usesCategory · Functor · Set

Used byScheme

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.