Enriched categories · The Lumenary

Lens

MotivationH

Hom-sets with structure

In many categories the morphisms between two objects form more than a set. Linear maps $V \to W$ form a vector space, and composition is bilinear. Homomorphisms between abelian groups form an abelian group. Continuous maps between nice spaces form a space, and composition is continuous. Functors between two categories, with natural transformations between them, form a category. In each case the extra structure is not decoration: composition respects it.

In 1973 F. William Lawvere pushed this idea to an extreme. Take as the "hom-object" from $x$ to $y$ a single number: the distance $d(x, y) \in [0, \infty]$ . Composing a route from $x$ to $y$ with a route from $y$ to $z$ gives a route from $x$ to $z$ , and the inequality $d(x, z) \le d(x, y) + d(y, z)$ is exactly what composition says. The identity on $x$ is the statement $d(x, x) = 0$ . A metric space is a category — of a new kind, enriched in the numbers $[0, \infty]$ — and categorical ideas such as functors, the Yoneda lemma and completeness acquire metric meanings.

This lesson develops enriched category theory: categories whose hom-objects live in a monoidal category $\mathcal{V}$ .

IntuitionH

Replace the set of arrows by an object of arrows

An ordinary category has, for objects $A, B, C$ , a composition function $\mathcal{C}(B, C) \times \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ and an identity element $\mathrm{id}_A \in \mathcal{C}(A, A)$ , i.e. a function $1 \to \mathcal{C}(A, A)$ from a one-point set. Both are phrased using only the cartesian product $\times$ and the unit $1$ of $\cat{Set}$ . Replace $(\cat{Set}, \times, 1)$ by any monoidal category $(\mathcal{V}, \otimes, I)$ , and the definition still makes sense:

base $\mathcal{V}$	a hom-object is	composition $\mathcal{C}(B, C) \otimes \mathcal{C}(A, B) \to \mathcal{C}(A, C)$	a $\mathcal{V}$ -category is
$(\cat{Set}, \times, 1)$	a set	a function	a locally small category
truth values $(\{0 \le 1\}, \wedge, 1)$	true or false	$(x \le y) \wedge (y \le z) \Rightarrow (x \le z)$	a preorder
$([0, \infty], \ge, +, 0)$	a number	$d(x, y) + d(y, z) \ge d(x, z)$	a Lawvere metric space
$(\cat{Ab}, \otimes, \Z)$	an abelian group	a bilinear map	a preadditive category
$(\cat{Vect}_k, \otimes, k)$	a vector space	a bilinear map	a $k$ -linear category
$(\cat{Cat}, \times, 1)$	a category	a functor	a strict 2-category

Two features are essential. Composition must be a morphism of $\mathcal{V}$ — a bilinear map, a continuous map, a functor, an inequality — and there may be no underlying elements: a number has no "arrows in it", so a Lawvere metric space has no individual morphisms at all, only hom-objects.

In a Lawvere metric space the hom-objects are distances, and composition is the triangle inequality

d(x,z) \le d(x,y) + d(y,z)

DefinitionsH

Enriched categories, functors and transformations

Fix a monoidal category $(\mathcal{V}, \otimes, I, \alpha, \lambda, \rho)$ .

Definition— V-category

A $\mathcal{V}$ -category $\mathcal{C}$ consists of a collection of objects; for objects $A, B$ a hom-object $\mathcal{C}(A, B) \in \mathcal{V}$ ; for $A, B, C$ a composition morphism $M_{A,B,C} : \mathcal{C}(B, C) \otimes \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ in $\mathcal{V}$ ; and for each $A$ an identity morphism $j_A : I \to \mathcal{C}(A, A)$ in $\mathcal{V}$ , such that composition is associative (the diagram below commutes) and unital: $M_{A,B,B} \circ (j_B \otimes 1) = \lambda$ and $M_{A,A,B} \circ (1 \otimes j_A) = \rho$ as maps $I \otimes \mathcal{C}(A, B) \to \mathcal{C}(A, B)$ and $\mathcal{C}(A, B) \otimes I \to \mathcal{C}(A, B)$ .

Associativity of composition in a

\mathcal{V}

-category.

Definition— V-functor and V-natural transformation

A $\mathcal{V}$ -functor $F : \mathcal{C} \to \mathcal{D}$ assigns to each object $A$ an object $FA$ , and to each pair $A, B$ a morphism $F_{A,B} : \mathcal{C}(A, B) \to \mathcal{D}(FA, FB)$ of $\mathcal{V}$ , compatible with composition and identities. For $\mathcal{V}$ -functors $F, G : \mathcal{C} \to \mathcal{D}$ , a $\mathcal{V}$ -natural transformation $\theta : F \Rightarrow G$ is a family of morphisms $\theta_A : I \to \mathcal{D}(FA, GA)$ in $\mathcal{V}$ such that, for all $A, B$ , the two composites $\mathcal{C}(A, B) \to \mathcal{D}(FA, GB)$ — "apply $G$ , then precompose with $\theta_A$ " and "apply $F$ , then postcompose with $\theta_B$ " — are equal.

Definition— underlying category

The underlying category $\mathcal{C}_0$ of a $\mathcal{V}$ -category has the same objects and $\mathcal{C}_0(A, B) = \mathcal{V}(I, \mathcal{C}(A, B))$ , with composition $g \circ f = M \circ (g \otimes f) \circ \lambda_I^{-1}$ . For $\mathcal{V} = \cat{Set}$ , $\cat{Set}(1, X) \cong X$ recovers $\mathcal{C}$ ; for $\mathcal{V} = \cat{Ab}$ it forgets the group structure on hom-sets; for $\mathcal{V} = [0, \infty]$ there is one arrow $x \to y$ when $d(x, y) = 0$ and none otherwise.

Definition— Lawvere metric space

A Lawvere metric space is a set $X$ with distances $d(x, y) \in [0, \infty]$ such that $d(x, x) = 0$ and $d(x, z) \le d(x, y) + d(y, z)$ . Unlike a metric, $d$ need not be symmetric, may take the value $\infty$ , and may vanish for $x \neq y$ .

Closedness. $\mathcal{V}$ is closed if each $- \otimes A$ has a right adjoint $[A, -]$ . For symmetric closed $\mathcal{V}$ , $\mathcal{V}$ itself is a $\mathcal{V}$ -category with hom-objects $[A, B]$ , and (if $\mathcal{V}$ is also complete) $\mathcal{V}$ -functors $\mathcal{C} \to \mathcal{D}$ between small $\mathcal{V}$ -categories form a $\mathcal{V}$ -category $[\mathcal{C}, \mathcal{D}]$ , whose hom-object is the end $\int_A \mathcal{D}(FA, GA)$ . For $[0, \infty]$ , $a + c \ge b \iff c \ge b \mathbin{\dot-} a$ , where $b \mathbin{\dot-} a = \max(b - a, 0)$ (with $\infty \mathbin{\dot-} \infty = 0$ ), so $[a, b] = b \mathbin{\dot-} a$ and ends are suprema.

Worked examplesH

Examples and non-examples

Example— Metric spaces, and asymmetric ones

Every metric space, and every pseudo- or extended metric space, is a Lawvere metric space. Asymmetric examples arise whenever the cost of going depends on the direction:

heights: on $\R$ , $d(x, y) = \max(y - x, 0)$ — climbing from height $x$ to $y$ costs $y - x$ , descending is free;
travel times in a hilly town, along one-way streets, or against a river current; the experiment below computes one;
the base itself: $[0, \infty]$ with $d(a, b) = b \mathbin{\dot-} a$ (truncated subtraction) is a Lawvere metric space — $\mathcal{V}$ enriched over itself;
subsets: for subsets $S, T$ of a Lawvere metric space, $d(S, T) = \sup_{s \in S} \inf_{t \in T} d(s, t)$ (the one-sided Hausdorff distance) is a Lawvere metric; it is $0$ when $S \subseteq T$ , and symmetrising with $\max$ gives the usual Hausdorff distance.

A preorder becomes a Lawvere metric space with $d(x, y) = 0$ if $x \le y$ and $\infty$ otherwise.

Example— Rings and linear categories

An $\cat{Ab}$ -enriched category with one object $*$ is an abelian group $R = \mathcal{C}(*, *)$ with a bilinear associative composition and an identity: a ring. With several objects it is a "ring with several objects" (Mitchell): for instance the category of finitely generated free $R$ -modules, with hom-groups of matrices. Additive categories (abelian categories in particular) are $\cat{Ab}$ -enriched by definition. Over a field $k$ , one-object $\cat{Vect}_k$ -categories are $k$ -algebras, and the path category of a quiver, made $k$ -linear, has the path algebra as its total algebra (see path algebras).

Example— Strict 2-categories

A $\cat{Cat}$ -enriched category has, for objects $A, B$ , a hom-category $\mathcal{C}(A, B)$ whose objects are 1-cells $f : A \to B$ and whose morphisms are 2-cells $\sigma : f \Rightarrow g$ ; composition is a functor $\mathcal{C}(B, C) \times \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ . The prime example is $\cat{Cat}$ itself (categories, functors, natural transformations). Weakening the associativity and unit equations to coherent isomorphisms gives bicategories (Bénabou 1967), the first step towards higher categories.

Example— Spaces of maps and chain complexes

Categories enriched in topological spaces (or simplicial sets) have mapping spaces with continuous (simplicial) composition: compactly generated spaces with $\mathrm{Map}(X, Y)$ , or simplicial sets with $\underline{\mathrm{Hom}}(X, Y)$ . Categories enriched in chain complexes are dg-categories: chain complexes of modules with the Hom complex, whose differential is $d f = d_Y f - (-1)^{|f|} f d_X$ .

Example— A non-example: structure that composition ignores

Let $\mathcal{C}$ have abelian groups as objects and all functions as morphisms. Each hom-set $\mathcal{C}(A, B) = B^A$ is an abelian group under pointwise addition, and $(f + g) \circ h = f \circ h + g \circ h$ . But $h \circ (f + g) \neq h \circ f + h \circ g$ when $h$ is not additive (take $h(x) = x^2$ on $\Z$ , as a function $\Z \to \Z$ ). Composition is not bilinear, hence not a morphism $\mathcal{C}(B, C) \otimes \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ of $\cat{Ab}$ , so this is not an $\cat{Ab}$ -enriched category, despite having an abelian group of arrows between any two objects.

ProofH

Theorems

Theorem— Proposition 1 (Set-enriched categories)

Categories enriched in $(\cat{Set}, \times, 1)$ are exactly locally small categories.

Proof

A morphism $1 \to \mathcal{C}(A, A)$ is an element $\mathrm{id}_A$ ; a function $\mathcal{C}(B, C) \times \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ is a composition law. Evaluating the unit and associativity diagrams of $\cat{Set}$ on elements $(g, f)$ , $(h, g, f)$ gives $\mathrm{id} \circ f = f = f \circ \mathrm{id}$ and $h \circ (g \circ f) = (h \circ g) \circ f$ . Conversely these equations make the diagrams commute. (Mathlib: enrichedCategoryTypeEquivCategory.)

∎

Theorem— Proposition 2 (preorders)

Categories enriched in truth values $(\{\bot \le \top\}, \wedge, \top)$ are exactly preordered sets.

Proof

Write $x \le y$ for " $\mathcal{C}(x, y) = \top$ ". A morphism $\top \to \mathcal{C}(x, x)$ exists iff $x \le x$ ; a morphism $\mathcal{C}(y, z) \wedge \mathcal{C}(x, y) \to \mathcal{C}(x, z)$ exists iff $(x \le y \text{ and } y \le z) \Rightarrow x \le z$ . Since the truth-value category has at most one morphism between two objects, the associativity and unit diagrams commute automatically. So the data are a reflexive, transitive relation, and nothing else.

∎

Theorem— Theorem 3 (Lawvere 1973)

Let $\mathcal{V} = ([0, \infty], \ge, +, 0)$ , the poset $[0, \infty]$ ordered by $\ge$ (so there is an arrow $a \to b$ iff $a \ge b$ ), with $\otimes = +$ and unit $0$ . Then:

$\mathcal{V}$ -categories are exactly Lawvere metric spaces;
$\mathcal{V}$ -functors $X \to Y$ are exactly the non-expansive maps, $d(fx, fx') \le d(x, x')$ ;
a $\mathcal{V}$ -natural transformation $f \Rightarrow g$ exists (and is unique) iff $d(fx, gx) = 0$ for all $x$ ;
the $\mathcal{V}$ -category of $\mathcal{V}$ -functors $X \to Y$ has hom-objects $d(f, g) = \sup_x d(fx, gx)$ , a Lawvere metric.

Proof

$\mathcal{V}$ is a monoidal category: $+$ is monotone, so it is a functor, and associativity and unit laws of $+$ give the (identity) associator and unitors; coherence is automatic because $\mathcal{V}$ is a preorder.

(1) An identity $0 \to X(x, x)$ is the inequality $0 \ge d(x, x)$ , i.e. $d(x, x) = 0$ . A composition $X(y, z) + X(x, y) \to X(x, z)$ is the inequality $d(y, z) + d(x, y) \ge d(x, z)$ . Since $\mathcal{V}$ is a preorder, the associativity and unit axioms hold automatically.

(2) $F_{x,x'} : X(x, x') \to Y(fx, fx')$ is the inequality $d(x, x') \ge d(fx, fx')$ ; the functor axioms are equations between parallel morphisms of a preorder, so they hold.

(3) A component $\theta_x : 0 \to Y(fx, gx)$ is the inequality $d(fx, gx) \le 0$ ; naturality is again automatic.

(4) For each $x$ , $d(fx, hx) \le d(fx, gx) + d(gx, hx) \le \sup d(f, g) + \sup d(g, h)$ ; take the supremum over $x$ . And $d(f, f) = \sup_x 0 = 0$ . This supremum is the end $\int_x Y(fx, gx)$ , since limits in $\mathcal{V}$ (ordered by $\ge$ ) are suprema.

∎

Theorem— Theorem 4 (enriched Yoneda embedding for Lawvere metric spaces)

For every Lawvere metric space $X$ and all $x, y \in X$ ,

d(x, y) = \sup_{z \in X} \big( d(z, y) \mathbin{\dot-} d(z, x) \big).

Hence $x \mapsto d(-, x)$ is an isometric embedding of $X$ into the Lawvere metric space of functions $X \to [0, \infty]$ with the distance $\sup_z \big(\psi(z) \mathbin{\dot-} \varphi(z)\big)$ from $\varphi$ to $\psi$ .

Proof

For every $z$ , the triangle inequality $d(z, y) \le d(z, x) + d(x, y)$ is equivalent, by the adjunction $a + c \ge b \iff c \ge b \mathbin{\dot-} a$ , to $d(z, y) \mathbin{\dot-} d(z, x) \le d(x, y)$ . So the supremum is at most $d(x, y)$ , and $z = x$ attains it: $d(x, y) \mathbin{\dot-} d(x, x) = d(x, y) \mathbin{\dot-} 0 = d(x, y)$ .

∎

This is the Yoneda lemma in miniature: "an object is determined by the arrows into it", with "arrows into $x$ " replaced by "distances to $x$ ". For symmetric metric spaces it is the classical Kuratowski–Fréchet embedding into a space of functions.

Theorem— Proposition 5 (one-object Ab-categories are rings)

$\cat{Ab}$ -enriched categories with one object correspond exactly to rings.

Proof

With one object $*$ , the data are an abelian group $R = \mathcal{C}(*, *)$ , a homomorphism $R \otimes R \to R$ — equivalently a biadditive map $R \times R \to R$ , a multiplication satisfying both distributive laws — and a homomorphism $\Z \to R$ , determined by the element $1$ . Associativity and unit diagrams, evaluated on pure tensors, are associativity of multiplication and $1 \cdot r = r = r \cdot 1$ . Conversely a ring gives this data.

∎

Theorem— Proposition 6 (Cat-enriched categories and the interchange law)

In a $\cat{Cat}$ -enriched category, horizontal and vertical composition of 2-cells satisfy the interchange law $(\tau' \cdot \tau) \ast (\sigma' \cdot \sigma) = (\tau' \ast \sigma') \cdot (\tau \ast \sigma)$ .

Proof

Vertical composition $\cdot$ is composition inside the hom-categories, and horizontal composition $\ast$ is the action of the composition functor $M : \mathcal{C}(B, C) \times \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ on morphisms: $\tau \ast \sigma = M(\tau, \sigma)$ . In the product category, $(\tau', \sigma') \cdot (\tau, \sigma) = (\tau' \cdot \tau, \sigma' \cdot \sigma)$ . Functoriality of $M$ gives $M(\tau' \cdot \tau, \sigma' \cdot \sigma) = M(\tau', \sigma') \cdot M(\tau, \sigma)$ , which is the interchange law.

∎

Formal mathematicsF

Enriched categories in Lean

Mathlib has EnrichedCategory V C for any monoidal category V, with composition written in diagrammatic order, Hom X Y ⊗ Hom Y Z ⟶ Hom X Z. We construct Lawvere's base as a monoidal category. Mathlib makes every preorder a category with an arrow $a \to b$ iff $a \le b$ ; we take the order dual of $[0, \infty]$ so that arrows go "downhill" ( $a \ge b$ ):

DistLean 4Formally verified

/-- **Lawvere's monoidal category `([0, ∞], ≥, +, 0)`.** Its objects are the extended
non-negative reals; we use the order dual of `ℝ≥0∞`, so that (by Mathlib's category structure on
a preorder) there is exactly one arrow `a ⟶ b` when `a ≥ b` as distances, and none otherwise. -/
abbrev Dist : Type := ℝ≥0∞ᵒᵈ

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

distMonoidalLean 4Formally verified

/-- The monoidal structure on `Dist`: `a ⊗ b = a + b`, unit `0`. Addition is monotone, so it
acts on arrows, and the associator and unitors are the equalities `(a + b) + c = a + (b + c)`,
`0 + a = a`, `a + 0 = a`. In a category with at most one arrow between two objects every diagram
commutes, so the pentagon and triangle axioms hold automatically. -/
instance distMonoidal : MonoidalCategory Dist where
  tensorObj a b := a + b
  whiskerLeft a _ _ f := homOfLE (add_le_add_right (leOfHom f) a)
  whiskerRight f b := homOfLE (add_le_add_left (leOfHom f) b)
  tensorUnit := 0
  associator a b c := eqToIso (add_assoc a b c)
  leftUnitor a := eqToIso (zero_add a)
  rightUnitor a := eqToIso (add_zero a)
  id_tensorHom_id _ _ := Subsingleton.elim _ _
  tensorHom_comp_tensorHom _ _ _ _ := Subsingleton.elim _ _
  whiskerLeft_id _ _ := Subsingleton.elim _ _
  id_whiskerRight _ _ := Subsingleton.elim _ _
  associator_naturality _ _ _ := Subsingleton.elim _ _
  leftUnitor_naturality _ := Subsingleton.elim _ _
  rightUnitor_naturality _ := Subsingleton.elim _ _
  pentagon _ _ _ _ := Subsingleton.elim _ _
  triangle _ _ := Subsingleton.elim _ _

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

The central theorem: on any type, Dist-enriched categories in Mathlib's sense are the same as Lawvere metrics. The identity morphism is the statement $d(x, x) = 0$ and the composition morphism is the triangle inequality.

LawvereMetricLean 4Formally verified

/-- A **Lawvere metric** on `X`: distances `d x y ∈ [0, ∞]` with `d x x = 0` and the triangle
inequality. Symmetry, finiteness and "`d x y = 0 → x = y`" are *not* required. -/
structure LawvereMetric (X : Type u) where
  /-- The distance from `x` to `y`. -/
  d : X → X → ℝ≥0∞
  /-- Every point is at distance `0` from itself. -/
  self : ∀ x, d x x = 0
  /-- The triangle inequality. -/
  triangle : ∀ x y z, d x z ≤ d x y + d y z

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

lawvereEquivEnrichedLean 4Proved here from basic factsFormally verified

/-- **Lawvere's observation: metric spaces are enriched categories.** On any type `X`,
`Dist`-enriched category structures (in Mathlib's sense) correspond exactly to Lawvere metrics.
* the hom-object `X(x, y)` is the distance `d x y`;
* an identity `0 ⟶ X(x, x)` exists iff `0 ≥ d x x`, i.e. `d x x = 0`;
* a composition `X(x, y) ⊗ X(y, z) ⟶ X(x, z)` exists iff `d x y + d y z ≥ d x z` — the
  triangle inequality *is* composition;
* the unit and associativity axioms hold automatically, since `Dist` is thin. -/
def lawvereEquivEnriched (X : Type u) : LawvereMetric X ≃ EnrichedCategory Dist X where
  toFun M :=
    { Hom := fun x y => OrderDual.toDual (M.d x y)
      id := fun x => homOfLE (by
        show M.d x x ≤ 0
        rw [M.self])
      comp := fun x y z => homOfLE (M.triangle x y z)
      id_comp := fun _ _ => Subsingleton.elim _ _
      comp_id := fun _ _ => Subsingleton.elim _ _
      assoc := fun _ _ _ _ => Subsingleton.elim _ _ }
  invFun E :=
    { d := fun x y => OrderDual.ofDual (E.Hom x y)
      self := fun x => le_antisymm (leOfHom (E.id x)) zero_le
      triangle := fun x y z => leOfHom (E.comp x y z) }
  left_inv M := by
    ext x y
    rfl
  right_inv E := by
    -- the hom-objects agree definitionally, and identities and compositions are arrows in a
    -- thin category, so `congr` closes the goal (using `Subsingleton`)
    rcases E with ⟨Hom, id, comp, _, _, _⟩
    congr

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

Examples, the underlying preorder, and the Yoneda embedding (Theorem 4):

ofPseudoEMetricLean 4Applies a library theoremFormally verified

/-- **Every (pseudo-extended) metric space is a Lawvere metric space**, using Mathlib's
`edist_self` and `edist_triangle`. Lawvere's notion drops symmetry and allows `d x y = 0` for
`x ≠ y`. -/
def ofPseudoEMetric (X : Type u) [PseudoEMetricSpace X] : LawvereMetric X where
  d := edist
  self := edist_self
  triangle := edist_triangle

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

uphillLean 4Formally verified

/-- The **uphill distance** on `ℝ` (think of heights): going from `x` up to `y` costs `y - x`,
going down is free. In `ℝ≥0∞`, `d x y = ofReal (y - x)`, where `ofReal` truncates negative
numbers to `0`. -/
noncomputable def uphill : LawvereMetric ℝ where
  d x y := ENNReal.ofReal (y - x)
  self x := by simp
  triangle x y z := by
    calc ENNReal.ofReal (z - x) = ENNReal.ofReal ((y - x) + (z - y)) := by ring_nf
      _ ≤ ENNReal.ofReal (y - x) + ENNReal.ofReal (z - y) := ENNReal.ofReal_add_le

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

uphill_not_symmetricLean 4Proved here from basic factsFormally verified

/-- **Lawvere metrics need not be symmetric**: in the uphill distance, `d 0 1 = 1` but
`d 1 0 = 0`. -/
theorem uphill_not_symmetric : uphill.d 0 1 = 1 ∧ uphill.d 1 0 = 0 := by
  constructor
  · simp [uphill]
  · simp [uphill]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

underlying_preorderLean 4Proved here from basic factsFormally verified

/-- **The underlying ordinary category of a Lawvere metric space** is a preorder: there is an
arrow `x → y` (an arrow `0 ⟶ X(x, y)` in `Dist`) exactly when `d x y = 0`, and this relation is
reflexive and transitive by `d x x = 0` and the triangle inequality. -/
theorem underlying_preorder {X : Type u} (M : LawvereMetric X) :
    (∀ x, M.d x x = 0) ∧ (∀ x y z, M.d x y = 0 → M.d y z = 0 → M.d x z = 0) := by
  refine ⟨M.self, fun x y z hxy hyz => ?_⟩
  apply le_antisymm _ zero_le
  calc M.d x z ≤ M.d x y + M.d y z := M.triangle x y z
    _ = 0 := by rw [hxy, hyz, add_zero]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

yoneda_isometryLean 4Proved here from basic factsFormally verified

/-- **The enriched Yoneda lemma for Lawvere metric spaces.** Send `x` to the "distance-to"
function `d(-, x)`. Comparing these functions with the closed structure of `Dist` (truncated
subtraction) recovers the metric:
`d x y = sup_z (d z y - d z x)`.
So `x ↦ d(-, x)` is an isometric embedding of `X` into a space of functions — the Yoneda
embedding, which for symmetric metric spaces is the Kuratowski–Fréchet embedding.
Proof: each term is `≤ d x y` because `d z y ≤ d z x + d x y` (triangle inequality, via
`tsub_le_iff_left`), and the term `z = x` equals `d x y - 0 = d x y`. -/
theorem yoneda_isometry {X : Type u} (M : LawvereMetric X) (x y : X) :
    ⨆ z, (M.d z y - M.d z x) = M.d x y := by
  apply le_antisymm
  · exact iSup_le fun z => tsub_le_iff_left.mpr (M.triangle z x y)
  · exact le_iSup_of_le x (by rw [M.self, tsub_zero])

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

Enriched functors are non-expansive maps, and maps into a Lawvere metric space carry the supremum metric; the closed structure is truncated subtraction:

nonExpansiveEquivLean 4Proved here from basic factsFormally verified

/-- **`Dist`-enriched functors are exactly non-expansive (1-Lipschitz) maps.** A `Dist`-functor
`F : X → Y` consists of a map on points with an arrow `X(x, y) ⟶ Y(F x, F y)` in `Dist` for all
`x, y`, i.e. `d (F x) (F y) ≤ d x y`; the functor axioms are automatic. -/
def nonExpansiveEquiv {X : Type u} {Y : Type v} [EnrichedCategory Dist X]
    [EnrichedCategory Dist Y] :
    { f : X → Y // ∀ x x', OrderDual.ofDual (EnrichedCategory.Hom (V := Dist) (f x) (f x')) ≤
        OrderDual.ofDual (EnrichedCategory.Hom (V := Dist) x x') } ≃
      EnrichedFunctor Dist X Y where
  toFun f :=
    { obj := f.1
      map := fun x x' => homOfLE (f.2 x x')
      map_id := fun _ => Subsingleton.elim _ _
      map_comp := fun _ _ _ => Subsingleton.elim _ _ }
  invFun F := ⟨F.obj, fun x x' => leOfHom (F.map x x')⟩
  left_inv _ := rfl
  right_inv F := by
    rcases F with ⟨obj, map, _, _⟩
    simp only [EnrichedFunctor.mk.injEq, heq_eq_eq, true_and]
    funext x x'
    exact Subsingleton.elim _ _

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

supMetricLean 4Proved here from basic factsFormally verified

/-- **The enriched functor category.** For a Lawvere metric `N` on `Y`, the maps `X → Y` carry the
Lawvere metric `d(f, g) = sup_x d(f x, g x)`. Self-distance: `sup_x 0 = 0`. Triangle:
`d(f x, h x) ≤ d(f x, g x) + d(g x, h x) ≤ d(f, g) + d(g, h)` for each `x`, and take the
supremum. (This is the hom-object of the `Dist`-enriched category of `Dist`-functors.) -/
noncomputable def supMetric (X : Type u) {Y : Type v} (N : LawvereMetric Y) :
    LawvereMetric (X → Y) where
  d f g := ⨆ x, N.d (f x) (g x)
  self f := by simp [N.self]
  triangle f g h := by
    apply iSup_le
    intro x
    calc N.d (f x) (h x) ≤ N.d (f x) (g x) + N.d (g x) (h x) := N.triangle _ _ _
      _ ≤ (⨆ x, N.d (f x) (g x)) + ⨆ x, N.d (g x) (h x) :=
        add_le_add (le_iSup (fun x => N.d (f x) (g x)) x) (le_iSup (fun x => N.d (g x) (h x)) x)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

dist_closedLean 4Applies a library theoremFormally verified

/-- **`Dist` is closed**: the internal hom is truncated subtraction, `[a, b] = b - a`, because
`a + c ≥ b ↔ c ≥ b - a` (Mathlib's `tsub_le_iff_left` in `ℝ≥0∞`). So `Dist`-categories can be
enriched over themselves, which is what makes `supMetric` a hom-object. -/
theorem dist_closed (a b c : ℝ≥0∞) : b - a ≤ c ↔ b ≤ a + c :=
  tsub_le_iff_left

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

The same construction for truth values gives preorders, and Mathlib supplies the $\cat{Set}$ - and $\cat{Ab}$ -enriched cases:

truthMonoidalLean 4Formally verified

/-- **Truth values as a monoidal category.** `Prop` is a preorder under implication, hence a
category with an arrow `p ⟶ q` exactly when `p → q`; the tensor is `∧` and the unit is `True`.
Again all coherence axioms hold because the category is thin. -/
instance truthMonoidal : MonoidalCategory Prop where
  tensorObj p q := p ∧ q
  whiskerLeft p _ _ f := homOfLE fun h => ⟨h.1, leOfHom f h.2⟩
  whiskerRight f q := homOfLE fun h => ⟨leOfHom f h.1, h.2⟩
  tensorUnit := True
  associator p q r := eqToIso (propext and_assoc)
  leftUnitor p := eqToIso (true_and p)
  rightUnitor p := eqToIso (and_true p)
  id_tensorHom_id _ _ := Subsingleton.elim _ _
  tensorHom_comp_tensorHom _ _ _ _ := Subsingleton.elim _ _
  whiskerLeft_id _ _ := Subsingleton.elim _ _
  id_whiskerRight _ _ := Subsingleton.elim _ _
  associator_naturality _ _ _ := Subsingleton.elim _ _
  leftUnitor_naturality _ := Subsingleton.elim _ _
  rightUnitor_naturality _ := Subsingleton.elim _ _
  pentagon _ _ _ _ := Subsingleton.elim _ _
  triangle _ _ := Subsingleton.elim _ _

Axioms used: propextformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

preorderEquivEnrichedLean 4Proved here from basic factsFormally verified

/-- **Preorders are exactly the categories enriched in truth values.** A `Prop`-enriched category
on `X` is a relation `x ≤ y` (the hom-object) with an identity `True → (x ≤ x)` (reflexivity)
and a composition `(x ≤ y) ∧ (y ≤ z) → (x ≤ z)` (transitivity). -/
def preorderEquivEnriched (X : Type u) :
    { r : X → X → Prop // (∀ x, r x x) ∧ ∀ x y z, r x y → r y z → r x z } ≃
      EnrichedCategory Prop X where
  toFun r :=
    { Hom := r.1
      id := fun x => homOfLE fun _ => r.2.1 x
      comp := fun x y z => homOfLE fun h => r.2.2 x y z h.1 h.2
      id_comp := fun _ _ => Subsingleton.elim _ _
      comp_id := fun _ _ => Subsingleton.elim _ _
      assoc := fun _ _ _ _ => Subsingleton.elim _ _ }
  invFun E :=
    ⟨E.Hom, fun x => leOfHom (E.id x) trivial, fun x y z h₁ h₂ => leOfHom (E.comp x y z) ⟨h₁, h₂⟩⟩
  left_inv _ := rfl
  right_inv E := by
    -- the hom-objects agree definitionally, and identities and compositions are arrows in a
    -- thin category, so `congr` closes the goal (using `Subsingleton`)
    rcases E with ⟨Hom, id, comp, _, _, _⟩
    congr

Axioms used: propextformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

set_enrichedLean 4Applies a library theoremFormally verified

/-- **Locally small categories are exactly the categories enriched in `(Type, ×, PUnit)`**
(Mathlib's `enrichedCategoryTypeEquivCategory`). -/
theorem set_enriched (C : Type u) : Nonempty (EnrichedCategory (Type v) C ≃ Category.{v} C) :=
  ⟨enrichedCategoryTypeEquivCategory C⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

end_ringLean 4Applies a library theoremFormally verified

/-- **In an `Ab`-enriched (preadditive) category, the endomorphisms of an object form a ring**,
with addition from the enrichment and multiplication given by composition (Mathlib's instance
`CategoryTheory.End` ring). A one-object `Ab`-enriched category is therefore a ring. -/
theorem end_ring {C : Type u} [Category.{v} C] [Preadditive C] (X : C) :
    Nonempty (Ring (End X)) :=
  ⟨inferInstance⟩

Axioms used: propext, Quot.soundformal/Lumenary/EnrichedCategories.leanTry it in the Lean web editor

What is and is not formalised. Independently proved: the monoidal structures on $[0, \infty]$ and on truth values, the equivalences "Lawvere metrics = Dist-categories", "non-expansive maps = Dist-functors" and "preorders = Prop-categories", the supremum metric, the uphill example and the Yoneda isometry. From Mathlib: the definition of enriched categories and functors, the Set case, and rings of endomorphisms in preadditive categories. Not formalised: strict 2-categories as Cat-enriched categories, $\mathcal{V}$ -natural transformations for general $\mathcal{V}$ (Mathlib defines them, but we do not use them), ends, and Cauchy completion.

ComputationC

Shortest paths: free enriched categories

A directed graph freely generates a category, whose morphisms are paths. A directed graph with lengths freely generates a Lawvere metric space, whose distance is the length of the shortest path: composition in $[0, \infty]$ is $+$ , and "the best of all paths" is the infimum, so composing hom-matrices is min-plus (tropical) matrix multiplication, and a Lawvere metric is precisely a matrix $D$ with zero diagonal and $D \otimes D = D$ . The experiment computes walking times in a small hill town, where uphill paths are slower, checks every axiom on every triple, runs the same algorithm with $(\vee, \wedge)$ to get the free preorder (reachability), and checks that the one-sided Hausdorff distance between sets of places is again a Lawvere metric.

Shortest paths as free Lawvere metric spacesPythonExact computationExhaustive finite checkComputationally tested

"""Shortest paths are free enriched categories.

A Lawvere metric space is a category enriched in ([0, inf], >=, +, 0):
hom-objects are distances, composition is the triangle inequality and
identities say d(x, x) = 0. Just as a directed graph generates a free
category (whose morphisms are paths), a directed graph with lengths generates
a free Lawvere metric: the shortest-path distance. Composition of hom-objects
becomes "min-plus" (tropical) matrix multiplication, and a Lawvere metric is
exactly a matrix D with zero diagonal and D (x) D = D.

We compute this for walking times in a small hill town, where going uphill
takes longer than coming down, check every axiom on every triple, and
measure the asymmetry. Replacing (min, +) by (or, and) computes the free
preorder (reachability) - the same algorithm for truth-value enrichment.
Finally we check that the asymmetric Hausdorff distance between sets of
places is again a Lawvere metric. Exact integer arithmetic; exhaustive.
"""

import itertools

INF = float("inf")
PLACES = ["Market", "School", "Clinic", "Spring", "Ridge"]
# Walking times in minutes along footpaths (directed: uphill is slower).
PATHS = {
    ("Market", "School"): 6, ("School", "Market"): 4,
    ("School", "Clinic"): 9, ("Clinic", "School"): 5,
    ("Market", "Spring"): 3, ("Spring", "Market"): 3,
    ("Spring", "Clinic"): 12, ("Clinic", "Spring"): 7,
    ("Clinic", "Ridge"): 15, ("Ridge", "Clinic"): 8,
    ("Ridge", "Market"): 20,
}

def weight_matrix(places, paths):
    """Direct walking times: 0 on the diagonal, inf where there is no path."""
    n = len(places)
    idx = {p: i for i, p in enumerate(places)}
    w = [[0 if i == j else INF for j in range(n)] for i in range(n)]
    for (a, b), t in paths.items():
        w[idx[a]][idx[b]] = min(w[idx[a]][idx[b]], t)
    return w

def min_plus(a, b):
    """Tropical matrix product: (A (x) B)[i][k] = min_j A[i][j] + B[j][k]."""
    n = len(a)
    return [[min(a[i][j] + b[j][k] for j in range(n)) for k in range(n)]
            for i in range(n)]

def closure(w, product=min_plus):
    """Iterate D -> D (x) D until it stabilises (the free enriched category)."""
    d = w
    while True:
        nxt = product(d, d)
        if nxt == d:
            return d
        d = nxt

def is_lawvere_metric(d):
    """d(x, x) = 0 and d(x, z) <= d(x, y) + d(y, z) for all x, y, z."""
    n = len(d)
    if any(d[i][i] != 0 for i in range(n)):
        return False
    return all(d[i][k] <= d[i][j] + d[j][k]
               for i, j, k in itertools.product(range(n), repeat=3))

def asymmetric_pairs(d):
    """Unordered pairs {x, y} with d(x, y) != d(y, x)."""
    n = len(d)
    return [(i, j) for i in range(n) for j in range(i + 1, n)
            if d[i][j] != d[j][i]]

def or_and(a, b):
    """Boolean matrix product: (A (x) B)[i][k] = OR_j A[i][j] AND B[j][k]."""
    n = len(a)
    return [[any(a[i][j] and b[j][k] for j in range(n)) for k in range(n)]
            for i in range(n)]

def hausdorff(d, s, t):
    """Asymmetric Hausdorff distance: max over s of the distance to t."""
    if not s:
        return 0
    return max(min((d[x][y] for y in t), default=INF) for x in s)

def main():
    w = weight_matrix(PLACES, PATHS)
    d = closure(w)
    n = len(PLACES)
    print("Shortest walking times d(x, y) in minutes (row x, column y):")
    print("          " + "".join(f"{p[:6]:>8}" for p in PLACES))
    for name, row in zip(PLACES, d):
        print(f"  {name:<8}" + "".join(f"{v:>8}" for v in row))
    triples = n ** 3
    print(f"d(x, x) = 0 and triangle inequality on all {triples} triples: "
          f"{is_lawvere_metric(d)}")
    print(f"D (x) D = D (composition is idempotent):        "
          f"{min_plus(d, d) == d}")
    print(f"direct paths are never shorter than d:          "
          f"{all(d[i][j] <= w[i][j] for i in range(n) for j in range(n))}")
    asym = asymmetric_pairs(d)
    i, j = asym[0]
    print(f"asymmetric pairs: {len(asym)} of {n * (n - 1) // 2}, e.g. "
          f"d({PLACES[i]}, {PLACES[j]}) = {d[i][j]}, "
          f"d({PLACES[j]}, {PLACES[i]}) = {d[j][i]}")
    reach = closure([[v < INF for v in row] for row in w], product=or_and)
    print(f"truth-value enrichment (reachability) agrees: "
          f"{reach == [[v < INF for v in row] for row in d]}")
    subsets = [s for k in range(1, n + 1)
               for s in itertools.combinations(range(n), k)]
    h = [[hausdorff(d, s, t) for t in subsets] for s in subsets]
    print(f"asymmetric Hausdorff distance, {len(subsets)} nonempty sets of "
          f"places: Lawvere metric? {is_lawvere_metric(h)}")
    print()
    print("Epistemic status: exact computation, exhaustive over this one "
          "small graph\n(every triple of places, every triple of sets). It "
          "illustrates, but does\nnot prove, the general facts in the lesson: "
          "shortest-path distance is the\nfree Lawvere metric on a weighted "
          "graph, and Hausdorff distances obey the\ntriangle inequality.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exercises

1. Enriched categories

Warm-upHuman

In a category enriched in $([0, \infty], \ge, +, 0)$ , the hom-object from $x$ to $y$ is a number $d(x, y)$ . What does the composition morphism $X(y, z) \otimes X(x, y) \to X(x, z)$ say?

Choose one

d(x, z) \le d(x, y) + d(y, z)

d(x, x) = 0

d(x, y) = d(y, x)

d(x, z) \ge d(x, y) + d(y, z)

2. Enriched categories

CoreComputational

Directed footpaths between four places take these times (minutes): $A \to B$ : 4, $B \to C$ : 3, $C \to D$ : 5, $A \to C$ : 9, $D \to A$ : 2, $B \to D$ : 10. In the free Lawvere metric space on this weighted graph (shortest-path distance), what is $d(A, D)$ ?

3. Enriched categories

CoreHuman

Replace $+$ by $\max$ : let $\mathcal{V} = ([0, \infty], \ge, \max, 0)$ . What is a $\mathcal{V}$ -category?

Choose one

A set with

d(x, x) = 0

and

d(x, z) \le \max(d(x, y), d(y, z))

— a generalised ultrametric spaceAn ordinary metric spaceA preorderNothing:

\max

is not a monoidal structure

4. Enriched categories

CoreHuman

Which statement about one-object enriched categories is correct?

Choose one

A one-object

\mathbf{Ab}

-category is a ringA one-object

\mathbf{Vect}_k

-category is a field extension of

k

A one-object

\mathbf{Set}

-category is a groupA one-object

[0, \infty]

-category is any number

d \ge 0

5. Enriched categories

CoreHuman

The category with abelian groups as objects and all functions as morphisms has an abelian group $B^A$ of morphisms from $A$ to $B$ (pointwise addition). Why is it not an $\mathbf{Ab}$ -enriched category?

Choose one

Composition is not bilinear:

h \circ (f + g) \neq h \circ f + h \circ g

when

h

is not additive

B^A

is not an abelian groupThere are no identity morphismsThere are too many objects

6. Enriched categories

StretchHuman

Let $f, g : X \to Y$ be non-expansive maps between Lawvere metric spaces, viewed as $[0, \infty]$ -functors. When is there a $[0, \infty]$ -natural transformation $f \Rightarrow g$ ?

Choose one

Exactly when

d(f x, g x) = 0

for every

x

, and then it is uniqueAlways, since naturality is automaticExactly when

\sup_x d(fx, gx) < \infty

Only when

f = g

7. Enriched categories

CoreFormal

In the Lean file, Dist is the order dual of ℝ≥0∞, so a ⟶ b holds when a ≥ b as distances, and Mathlib writes the composition of an enriched category as comp x y z : Hom x y ⊗ Hom y z ⟶ Hom x z. In lawvereEquivEnriched, what does homOfLE (M.triangle x y z) provide?

Choose one

The composition morphism, from the triangle inequality M.d x z ≤ M.d x y + M.d y zThe identity morphism 𝟙_ Dist ⟶ Hom x xA proof of the associativity axiomA proof that M.d is symmetric

8. Enriched categories

StretchHuman

Theorem 4 says $d(x, y) = \sup_z \big(d(z, y) \mathbin{\dot-} d(z, x)\big)$ in any Lawvere metric space. Which $z$ attains the supremum, and why is no term larger?

Choose one

z = x

; each term is

\le d(x, y)

by the triangle inequality

d(z, y) \le d(z, x) + d(x, y)

z = y

; by symmetry of

d

No single

z

; the supremum is a limitEvery

z

attains it, because the terms are all equal

9. Enriched categories

StretchComputational

Write free_metric(w): given a square matrix w (list of lists) of direct path lengths, with 0 on the diagonal and float('inf') where there is no path, return the shortest-path distance matrix — the free Lawvere metric. Use repeated min-plus squaring $D \mapsto D \otimes D$ , $(D \otimes D)_{ik} = \min_j (D_{ij} + D_{jk})$ , until the matrix stops changing.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Enrichment means putting some extra structure on each hom-set." Composition and identities must be morphisms of $\mathcal{V}$ . Abelian groups with all functions between them have an abelian group of arrows between any two objects, but composition is not bilinear, so this is not an $\cat{Ab}$ -category. Likewise a topology on hom-sets is not a $\cat{Top}$ -enrichment unless composition is continuous.

Misconception

"Lawvere metric spaces are symmetric." Nothing in the definition of a $[0, \infty]$ -category forces $d(x, y) = d(y, x)$ : the hom-object from $x$ to $y$ and the one from $y$ to $x$ are unrelated, just as $\mathcal{C}(A, B)$ and $\mathcal{C}(B, A)$ are in an ordinary category. The uphill distance $d(0, 1) = 1$ , $d(1, 0) = 0$ is an example. Lawvere also drops " $d(x, y) = 0 \Rightarrow x = y$ " (like a preorder versus a partial order) and allows $d = \infty$ (like a category with empty hom-sets).

Misconception

"The underlying category remembers the enriched category." $\mathcal{C}_0(A, B) = \mathcal{V}(I, \mathcal{C}(A, B))$ can lose almost everything: for a Lawvere metric space it only records which distances are $0$ . Different $\mathcal{V}$ -categories can have the same underlying category, and enriched notions (limits, functor categories, Yoneda) must be formed in $\mathcal{V}$ , not in $\mathcal{C}_0$ .

Misconception

"Enrichment needs a concrete $\mathcal{V}$ with underlying sets." The definition only uses morphisms of $\mathcal{V}$ and its tensor product. In $[0, \infty]$ or truth values there are no elements of hom-objects to speak of — which is why Mathlib's EnrichedCategory makes no concreteness assumption.

ViewpointsH

Viewpoints

Geometry— Asymmetric distances and Hausdorff distance

Asymmetric distances are natural in geometry: Finsler metrics in which the length of a velocity vector $v$ differs from that of $-v$ (Randers metrics, which model travel time with a wind or current — Zermelo's navigation problem), and directed path metrics on graphs. Lawvere's framework treats them uniformly, with symmetry as an optional extra property (a "symmetric" $\mathcal{V}$ -category). Constructions on $\mathcal{V}$ -categories give familiar geometric objects: the one-sided Hausdorff distance $\sup_{s \in S} \inf_{t \in T} d(s, t)$ between subsets is the hom-object of a power-set construction, and its symmetrisation is the Hausdorff distance used to compare shapes and compact sets (see metric spaces).

Analysis— Completeness is a Yoneda-type property

Lawvere (1973) showed that Cauchy completeness of a metric space is an enriched-categorical property: a symmetric Lawvere metric space is Cauchy complete (every Cauchy sequence converges) if and only if every pair of adjoint $[0, \infty]$ -bimodules (distributors) into it is representable by a point — and the Cauchy completion is obtained from the Yoneda embedding of Theorem 4 by adding the "limits" of such bimodules. The same notion of Cauchy completion, applied to $\cat{Ab}$ -categories, gives the idempotent-split additive closure of a ring ("Karoubi envelope"): a single categorical idea with an analytic and an algebraic face. The Yoneda isometry itself is the categorical form of the embedding of a metric space into a space of bounded functions with the supremum norm (see real analysis and functional analysis).

Topology— Mapping spaces and homotopy theory

A category enriched in topological spaces or simplicial sets has mapping spaces in place of hom-sets, so homotopies between morphisms are paths in mapping spaces. Simplicially enriched categories whose mapping spaces are Kan complexes are one of the standard models of $(\infty, 1)$ -categories (Dwyer–Kan localisation; Bergner's model structure, 2007; the homotopy coherent nerve connects them to quasi-categories). Homotopy-coherent algebra — $A_\infty$ - and $E_\infty$ -structures — is phrased in categories enriched in spaces or chain complexes, and dg-categories (enriched in chain complexes) are the standard enhancement of derived categories (see ∞-categories and homotopy theory).

Algebra— Rings with several objects

Mitchell's slogan "rings with several objects" (1972) says that $\cat{Ab}$ -categories are to rings what categories are to monoids. Many ring-theoretic constructions generalise: modules over an $\cat{Ab}$ -category $\mathcal{R}$ are additive functors $\mathcal{R} \to \cat{Ab}$ ; Morita equivalence becomes equivalence of Cauchy completions; and a $k$ -linear category with finitely many objects is the same as a $k$ -algebra with a chosen complete set of orthogonal idempotents ( $A = \bigoplus_{x,y} \mathcal{R}(x, y)$ ). Representations of quivers are $k$ -linear functors out of the free $k$ -linear category on the quiver (see modules and representation theory).

Logic— Generalised truth values

The title of Lawvere's paper — "Metric spaces, generalized logic, and closed categories" — is meant literally: $[0, \infty]$ is a generalised object of truth values in which " $\top$ " is $0$ , conjunction is $+$ , implication is truncated subtraction ( $b \mathbin{\dot-} a$ plays the role of $a \Rightarrow b$ , by the same adjunction as $a \wedge c \le b \iff c \le (a \Rightarrow b)$ ), and a Lawvere metric is a "generalised preorder" in which $d(x, y)$ measures how far $x \le y$ is from being true. Replacing $[0, \infty]$ by any quantale (a complete lattice with an associative, join-preserving multiplication) gives quantale-enriched categories, used in fuzzy and many-valued logics and in the semantics of programs with quantitative information.

Computation— Tropical algebra and shortest paths

Over the "tropical" semiring $([0, \infty], \min, +)$ , matrix multiplication computes best routes, and the shortest-path distance of a weighted graph is the closure $D = I \oplus W \oplus W^{2} \oplus \cdots$ , computable by repeated squaring or by the Floyd–Warshall algorithm in $O(n^3)$ operations. In enriched language, this is the free $[0, \infty]$ -category on a weighted graph, and the Boolean semiring $(\{0, 1\}, \vee, \wedge)$ gives transitive closure — the free preorder — by the same algorithm. Path problems over other semirings (widest paths with $(\max, \min)$ , reliability with $(\max, \times)$ ) are free categories enriched in other bases.

History & global context

History and global context

Samuel Eilenberg and G. Max Kelly set out the theory of closed categories and enriched ("relative") categories at the 1965 La Jolla conference (published 1966); Jean Bénabou introduced related ideas in Paris at the same time, and bicategories in 1967. Strict 2-categories go back to Charles Ehresmann's work on double categories in the early 1960s.
F. William Lawvere's "Metric spaces, generalized logic, and closed categories" (Rendiconti del Seminario Matematico e Fisico di Milano, 1973) recognised metric spaces as enriched categories.
Barry Mitchell's "Rings with several objects" (1972) developed $\cat{Ab}$ -categories as generalised rings. Kelly's Basic Concepts of Enriched Category Theory (1982), written in Sydney, became the standard reference.
Enrichment in chain complexes (dg-categories) appears in Kelly's work of the mid-1960s and became central as an enhancement of triangulated categories through Alexei Bondal and Mikhail Kapranov (1990); enrichment in simplicial sets underlies William Dwyer and Daniel Kan's homotopy theory of categories (1980) and Julia Bergner's model structure (2007).

Hom-sets with structure

Replace the set of arrows by an object of arrows

Enriched categories, functors and transformations

Examples and non-examples

Theorems

Enriched categories in Lean

Shortest paths: free enriched categories

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading