Representable functors · The Lumenary

Lens

MotivationH

Elements as arrows

Here are five ways of saying the same kind of thing.

An element of a set $X$ is the same as a function $\{\ast\} \to X$ from a one-point set.
An element $g$ of a group $G$ is the same as a group homomorphism $\Z \to G$ : send $n$ to $g^n$ .
A subset $S \subseteq X$ is the same as a function $\chi_S : X \to \{0, 1\}$ : send the points of $S$ to $1$ and the others to $0$ .
A solution $(x, y)$ of $x^2 + y^2 = 1$ in a commutative ring $R$ — say $\left(\tfrac{3}{5}, \tfrac{4}{5}\right)$ in $\Q$ , or $(2, 2)$ in $\Z/7$ — is the same as a ring homomorphism $\Z[x, y]/(x^2 + y^2 - 1) \to R$ .
An open set $U$ of a topological space $X$ is the same as a continuous map from $X$ to the two-point Sierpiński space.

In each case a construction $F$ — elements, subsets, solutions, open sets — turns out to be nothing but the arrows into or out of one fixed object: $\{\ast\}$ , $\Z$ , $\{0,1\}$ , a quotient of a polynomial ring, the Sierpiński space. Such an $F$ is called representable, and the fixed object is its representing object.

This is more than a curiosity. If $F(X)$ "is" $\Hom(A, X)$ , then everything about $F$ is encoded in the single object $A$ : to construct $A$ is to solve a whole family of problems at once. Products, free groups, quotients, tensor products, limits and the parameter spaces ("moduli spaces") of algebraic geometry are all defined this way. This lesson builds on natural transformations, since "is the same as" will mean "is naturally isomorphic to", and it prepares for the Yoneda lemma.

IntuitionH

Probing with a test object

Think of an object $A$ as a measuring device. For any object $X$ , the set $\Hom(A, X)$ records all the ways $A$ can be "placed inside" $X$ — its $A$ -shaped elements. A map $g : X \to Y$ moves $A$ -shaped elements of $X$ to $A$ -shaped elements of $Y$ by composition. So every object $A$ gives a functor $\Hom(A, -) : \mathcal{C} \to \cat{Set}$ .

Now start from the other end: you have a functor $F : \mathcal{C} \to \cat{Set}$ , some construction of "things in $X$ ". Is there a single test object $A$ whose $A$ -shaped elements are exactly the $F$ -things, compatibly with all maps? If so, there must be one special $F$ -thing living on $A$ itself: the one corresponding to $\id_A$ . Call it $u \in F(A)$ . Every other $F$ -thing $y \in F(X)$ is then obtained by pushing $u$ along exactly one arrow $A \to X$ . That special element is a universal element, and the main theorem of this lesson says that representations and universal elements are the same thing.

In the group example, $A = \Z$ and $u = 1$ : every element $g$ of every group is the image of $1$ under exactly one homomorphism $\Z \to G$ . In the subset example (where arrows go into the test object), $A = \{0, 1\}$ and $u = \{1\}$ : every subset of every set is the preimage of $\{1\}$ under exactly one function.

DefinitionsH

Definitions

Throughout, $\mathcal{C}$ is locally small: each $\Hom(A, B)$ is a set. Composition is written $g \circ f$ (" $g$ after $f$ ").

Definition— hom functors

For an object $A$ of $\mathcal{C}$ :

the covariant hom functor $\Hom(A, -) : \mathcal{C} \to \cat{Set}$ sends $X$ to $\Hom(A, X)$ and $g : X \to Y$ to post-composition $g \circ - : \Hom(A, X) \to \Hom(A, Y)$ ;
the contravariant hom functor $\Hom(-, A) : \mathcal{C}^{\mathrm{op}} \to \cat{Set}$ sends $X$ to $\Hom(X, A)$ and $g : X \to Y$ to pre-composition $- \circ g : \Hom(Y, A) \to \Hom(X, A)$ .

Definition— representable functor

A functor $F : \mathcal{C} \to \cat{Set}$ is representable if there is an object $A$ and a natural isomorphism $\theta : \Hom(A, -) \cong F$ . A functor $G : \mathcal{C}^{\mathrm{op}} \to \cat{Set}$ is representable if there is an object $A$ and a natural isomorphism $\theta : \Hom(-, A) \cong G$ . The pair $(A, \theta)$ is a representation and $A$ a representing object.

Some authors (and Mathlib) call the covariant case corepresentable and keep representable for the contravariant one; always check which variance is meant.

Definition— universal element

A universal element of $F : \mathcal{C} \to \cat{Set}$ is a pair $(A, u)$ with $u \in F(A)$ such that for every object $X$ and every $y \in F(X)$ there is a unique arrow $f : A \to X$ with $F(f)(u) = y$ .

For contravariant $G : \mathcal{C}^{\mathrm{op}} \to \cat{Set}$ , a universal element is $(A, u)$ with $u \in G(A)$ such that for every $X$ and $y \in G(X)$ there is a unique $f : X \to A$ with $G(f)(u) = y$ .

A universal element: every element

y

of every

F(X)

is the image of

u

along exactly one arrow

f : A \to X

Worked examplesH

Examples and non-examples

Example— Elements of sets

The identity functor $\cat{Set} \to \cat{Set}$ is represented by a one-point set $\{\ast\}$ with universal element $\ast$ : an element $x \in X$ is the image of $\ast$ under exactly one function, $\ast \mapsto x$ . The functor $X \mapsto X \times X$ is represented by a two-element set $\{1, 2\}$ (a pair is a function from $\{1, 2\}$ ), and $X \mapsto X^n$ by an $n$ -element set.

Example— Underlying sets of algebraic structures

$U : \cat{Grp} \to \cat{Set}$ is represented by $\Z$ with universal element $1$ (proved in the next section).
$U : \cat{Ab} \to \cat{Set}$ : also $(\Z, 1)$ . $U : \cat{Mon} \to \cat{Set}$ : the monoid $(\N, +)$ with $1$ .
$U : \cat{Ring} \to \cat{Set}$ (rings with $1$ ): the polynomial ring $\Z[x]$ with universal element $x$ — for each $r \in R$ there is exactly one ring homomorphism $\Z[x] \to R$ with $x \mapsto r$ , evaluation at $r$ .
$U : \cat{Vect}_k \to \cat{Set}$ : the one-dimensional space $k$ with universal element $1$ . $U : \cat{Top} \to \cat{Set}$ : the one-point space.
$G \mapsto U(G) \times U(G)$ on groups: the free group $F_2 = \langle a, b \rangle$ with universal element $(a, b)$ .

Example— Subsets and the two-element set

The contravariant power-set functor $\mathcal{P} : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ sends $X$ to its set of subsets and $f : X \to Y$ to the preimage map $\mathcal{P}(f) = f^{-1} : \mathcal{P}(Y) \to \mathcal{P}(X)$ . It is represented by $2 = \{0, 1\}$ with universal element $\{1\} \in \mathcal{P}(2)$ : for each $S \subseteq X$ there is exactly one function $\chi : X \to 2$ with $\chi^{-1}(\{1\}) = S$ , the characteristic function $\chi_S$ . Naturality is the identity $\chi_{f^{-1}(S)} = \chi_S \circ f$ .

Example— Open sets and the Sierpiński space

Let $\mathbb{S} = \{0, 1\}$ with open sets $\varnothing$ , $\{1\}$ , $\{0, 1\}$ . The functor $\mathcal{O} : \cat{Top}^{\mathrm{op}} \to \cat{Set}$ , sending a space to its set of open subsets and a continuous map to preimage, is represented by $(\mathbb{S}, \{1\})$ : the function $\chi_U : X \to \mathbb{S}$ is continuous exactly when $\chi_U^{-1}(\{1\}) = U$ is open. The same object with the universal element $\{0\}$ (a closed set of $\mathbb{S}$ ) represents the functor of closed subsets. One object can represent different functors; the universal element is part of the data.

Example— Solutions of equations

On commutative rings, the functor $C(R) = \{(x, y) \in R^2 \mid x^2 + y^2 = 1\}$ is represented by $A = \Z[x, y]/(x^2 + y^2 - 1)$ with universal element the pair of cosets $(\bar x, \bar y)$ : a homomorphism $A \to R$ is determined by the images of $\bar x, \bar y$ , which can be any solution in $R$ . Likewise $R \mapsto R^\times$ (units) is represented by $\Z[x, x^{-1}]$ , and on groups $G \mapsto \{g \mid g^n = 1\}$ is represented by $\Z/n$ .

Example— Non-examples

The covariant power-set functor $\mathcal{P}_\ast : \cat{Set} \to \cat{Set}$ , with $\mathcal{P}_\ast(f)(S) = f(S)$ (direct image), is not representable (Proposition 5 below), although its contravariant cousin is.
The constant functor $\cat{Set} \to \cat{Set}$ with value a two-element set is not representable, for the same reason.
$G : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ , sending $X$ to the set of equivalence relations on $X$ (pulled back along maps), is not representable: if $G \cong \Hom(-, A)$ then $|G(n)| = |A|^n$ , but $|G(1)| = 1$ forces $|A| = 1$ , while $|G(2)| = 2$ .

ProofH

The main theorems

Theorem— Theorem 1 (representations are universal elements)

Let $F : \mathcal{C} \to \cat{Set}$ and let $A$ be an object.

If $\theta : \Hom(A, -) \Rightarrow F$ is a natural isomorphism, then $u = \theta_A(\id_A)$ is a universal element, and $\theta_X(f) = F(f)(u)$ for every $f : A \to X$ .
If $(A, u)$ is a universal element, then $\theta_X(f) = F(f)(u)$ defines a natural isomorphism $\theta : \Hom(A, -) \cong F$ .
These two constructions are mutually inverse: representations of $F$ by $A$ correspond bijectively to universal elements $u \in F(A)$ .

Proof

(1) Let $f : A \to X$ . Naturality of $\theta$ along $f$ says $\theta_X \circ \Hom(A, f) = F(f) \circ \theta_A$ . Apply both sides to $\id_A$ : since $\Hom(A, f)(\id_A) = f \circ \id_A = f$ , we get $\theta_X(f) = F(f)(\theta_A(\id_A)) = F(f)(u)$ . Each $\theta_X$ is a bijection, so for every $y \in F(X)$ there is exactly one $f$ with $\theta_X(f) = y$ , that is, with $F(f)(u) = y$ . So $(A, u)$ is universal.

(2) Each $\theta_X : \Hom(A, X) \to F(X)$ , $f \mapsto F(f)(u)$ , is a bijection: that is precisely the "exists unique" in the definition of a universal element. Naturality: for $g : X \to Y$ and $f : A \to X$ , functoriality of $F$ gives $\theta_Y(g \circ f) = F(g \circ f)(u) = F(g)\big(F(f)(u)\big) = F(g)(\theta_X(f))$ .

(3) Starting from $\theta$ , part (1) shows that the isomorphism built in (2) from $u = \theta_A(\id_A)$ is $f \mapsto F(f)(u) = \theta_X(f)$ , i.e. $\theta$ itself. Starting from $u$ , the isomorphism of (2) sends $\id_A$ to $F(\id_A)(u) = u$ .

∎

The dual statement, for contravariant functors and universal elements with arrows into $A$ , follows by applying Theorem 1 to $\mathcal{C}^{\mathrm{op}}$ . The argument in (1) — "a natural transformation out of $\Hom(A, -)$ is determined by where it sends $\id_A$ " — is the heart of the Yoneda lemma, which removes the word "isomorphism".

Theorem— Theorem 2 (uniqueness up to unique isomorphism)

If $(A, u)$ and $(A', u')$ are universal elements of $F : \mathcal{C} \to \cat{Set}$ , then there is exactly one arrow $\varphi : A \to A'$ with $F(\varphi)(u) = u'$ , and it is an isomorphism. In particular any two representing objects of $F$ are isomorphic.

Proof

Universality of $(A, u)$ gives a unique $\varphi : A \to A'$ with $F(\varphi)(u) = u'$ ; universality of $(A', u')$ gives a unique $\psi : A' \to A$ with $F(\psi)(u') = u$ . Then

F(\psi \circ \varphi)(u) = F(\psi)\big(F(\varphi)(u)\big) = F(\psi)(u') = u = F(\id_A)(u).

Both $\psi \circ \varphi$ and $\id_A$ send $u$ to $u$ , so by the uniqueness clause for $(A, u)$ (with $X = A$ , $y = u$ ) they are equal. Symmetrically $\varphi \circ \psi = \id_{A'}$ . So $\varphi$ is an isomorphism, and it is the only arrow sending $u$ to $u'$ .

∎

The isomorphism is unique once the universal elements are fixed. An object can carry several universal elements: $(\Z, 1)$ and $(\Z, -1)$ both represent $U : \cat{Grp} \to \cat{Set}$ , and the unique isomorphism between them is $n \mapsto -n$ .

Theorem— Theorem 3 (groups and subsets)

$(\Z, 1)$ is a universal element of $U : \cat{Grp} \to \cat{Set}$ , so $\Hom(\Z, G) \cong U(G)$ naturally in $G$ , by $\varphi \mapsto \varphi(1)$ .
$(2, \{1\})$ is a universal element of $\mathcal{P} : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ , so $\mathcal{P}(X) \cong \Hom(X, 2)$ naturally in $X$ .

Proof

(1) Let $G$ be a group and $g \in G$ . The map $\varphi(n) = g^n$ is a homomorphism $\Z \to G$ , because $g^{m + n} = g^m g^n$ for all integers $m, n$ , and $\varphi(1) = g$ . If $\psi : \Z \to G$ is any homomorphism with $\psi(1) = g$ , then $\psi(0) = e$ , $\psi(n + 1) = \psi(n)\,g$ and $\psi(n - 1) = \psi(n)\,g^{-1}$ , so by induction upwards and downwards from $0$ , $\psi(n) = g^n$ for every $n \in \Z$ . Hence $\varphi$ is the unique homomorphism with $\varphi(1) = g$ . By Theorem 1 the bijections $\varphi \mapsto \varphi(1) = U(\varphi)(1)$ are natural: for $h : G \to H$ , $(h \circ \varphi)(1) = h(\varphi(1))$ .

(2) Given $S \subseteq X$ , a function $\chi : X \to 2$ satisfies $\mathcal{P}(\chi)(\{1\}) = \chi^{-1}(\{1\}) = S$ exactly when $\chi(x) = 1$ for $x \in S$ and $\chi(x) = 0$ otherwise. So $\chi_S$ exists and is unique; apply (the dual of) Theorem 1.

∎

Theorem— Theorem 4 (universal properties are representability)

Products. Objects $A, B$ have a product $(P, p_1, p_2)$ if and only if $(P, (p_1, p_2))$ is a universal element of $X \mapsto \Hom(X, A) \times \Hom(X, B)$ (contravariant). Dually, coproducts represent $X \mapsto \Hom(A, X) \times \Hom(B, X)$ .
Free groups. For a set $S$ , the free group $(F(S), \iota)$ is a universal element of $G \mapsto \Hom_{\cat{Set}}(S, U(G))$ : every map $S \to U(G)$ extends uniquely to a homomorphism $F(S) \to G$ . Presentations generalise this: $\langle S \mid R \rangle$ represents $G \mapsto \{\text{maps } S \to G \text{ satisfying the relations } R\}$ .
Quotients. For $N \trianglelefteq G$ , $(G/N, \pi)$ is a universal element of $H \mapsto \{\varphi : G \to H \mid N \subseteq \ker \varphi\}$ . For an equivalence relation $\sim$ on a set $X$ , $(X/{\sim}, \pi)$ represents $Y \mapsto \{f : X \to Y \mid a \sim b \Rightarrow f(a) = f(b)\}$ .
Limits. A diagram $D : J \to \mathcal{C}$ has a limit if and only if the functor $X \mapsto \{\text{cones over } D \text{ with apex } X\}$ is representable; a limit is a universal element (a universal cone).

Proof

In each case, write out the definition of a universal element and compare it with the defining universal property — they are word for word the same. For (1): a universal element is $(P, (p_1, p_2))$ such that for every $X$ and every pair $(f, g) \in \Hom(X, A) \times \Hom(X, B)$ there is a unique $h : X \to P$ with $(p_1 \circ h, p_2 \circ h) = (f, g)$ , because the functor acts on $h$ by precomposition in both coordinates. That is the definition of a product. For (3) with groups: $\pi : G \to G/N$ kills $N$ , and the factorisation theorem says every $\varphi$ with $N \subseteq \ker \varphi$ factors as $\varphi = \bar\varphi \circ \pi$ for exactly one $\bar\varphi$ ; since the functor acts by post-composition, this is universality of $(G/N, \pi)$ . Items (2) and (4) are the same unwinding. Theorem 2 then gives, for free, that products, free groups, quotients and limits are unique up to a unique isomorphism compatible with the structure maps.

∎

Theorem— Proposition 5 (a necessary condition)

If $F : \cat{Set} \to \cat{Set}$ is representable, then $F(\{\ast\})$ has exactly one element. If $G : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ is representable by $A$ , then $G(\varnothing)$ has exactly one element and $|G(X)| = |A|^{|X|}$ for finite $X$ . Consequently the covariant power-set functor is not representable.

Proof

From any set $A$ there is exactly one function $A \to \{\ast\}$ , so $F(\{\ast\}) \cong \Hom(A, \{\ast\})$ is a one-element set. Into any $A$ there is exactly one function from $\varnothing$ , and there are $|A|^n$ functions from an $n$ -element set. For the covariant power set, $\mathcal{P}_\ast(\{\ast\}) = \{\varnothing, \{\ast\}\}$ has two elements.

∎

A more conceptual necessary condition: a covariant representable functor $\Hom(A, -)$ preserves all limits (maps into a limit are compatible families of maps into the diagram), and dually a contravariant one turns colimits into limits. Freyd's representability criterion, a corollary of his adjoint functor theorem, gives a converse: if $\mathcal{C}$ is complete and locally small, a functor $\mathcal{C} \to \cat{Set}$ is representable if and only if it preserves small limits and satisfies a "solution set" condition (Mac Lane, Categories for the Working Mathematician, Chapter V). We do not prove it here.

Formal mathematicsF

Representable functors in Lean

In Mathlib, F.RepresentableBy Y (for F : Cᵒᵖ ⥤ Type) is a natural bijection (X ⟶ Y) ≃ F(X), and F.CorepresentableBy X (for covariant F : C ⥤ Type) is a natural bijection (X ⟶ Y) ≃ F(Y). Morphisms in the category of types are functions wrapped as ↾f.

The power-set functor and Bool. The functor is defined with preimages, and the representation sends a characteristic function χ : X → Bool to {x | χ x = true}. Naturality holds by rfl: the preimage of $\{x \mid \chi\, x = \mathrm{true}\}$ under $f$ is $\{y \mid \chi(f\, y) = \mathrm{true}\}$ . The inverse needs to decide x ∈ S, which uses classical logic — a hint of the logician's viewpoint below.

powersetLean 4Formally verified

/-- The **contravariant power-set functor** `𝒫 : Setᵒᵖ ⥤ Set`. It sends a set `X` to the set
of its subsets, and a function `f : Y → X` to the preimage map `S ↦ f⁻¹(S)`, which goes from
subsets of `X` to subsets of `Y` — backwards, hence `Typeᵒᵖ`. -/
def powerset : Typeᵒᵖ ⥤ Type where
  obj X := Set X.unop
  map f := ↾fun S => (f.unop : _ → _) ⁻¹' S

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

powerset_representableLean 4Proved here from basic factsFormally verified

/-- **The power-set functor is represented by the two-element set `Bool`.** Subsets `S ⊆ X`
correspond to characteristic functions `χ : X → Bool` (`S = {x | χ x = true}`), and the
correspondence is natural: the characteristic function of `f⁻¹(S)` is `χ_S ∘ f`.
Building `χ_S` from `S` needs to decide `x ∈ S`, which uses classical logic. -/
theorem powerset_representable : Nonempty (powerset.RepresentableBy Bool) :=
  ⟨{ homEquiv := fun {X} =>
    { toFun := fun χ => {x | χ x = true}
      invFun := fun (S : Set X) => ↾fun x => @decide (x ∈ S) (Classical.propDecidable _)
      left_inv := fun χ => by
        ext x
        simp
      right_inv := fun (S : Set X) => by
        apply Set.ext
        intro x
        simp }
     homEquiv_comp := fun _ _ => rfl }⟩

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

Groups and $\Z$ . First the induction from Theorem 3, then the bijection $\Hom(\Z, G) \cong G$ and its naturality. (Mathlib writes the integers as a multiplicative group Multiplicative ℤ.) Finally Mathlib's own statement for its category GrpCat, built on Joël Riou's natural isomorphism GrpCat.coyonedaObjIsoForget.

int_hom_eq_zpowLean 4Proved here from basic factsFormally verified

/-- A group homomorphism `φ : ℤ → G` is determined by `g = φ(1)`: it must send `n` to `gⁿ`.
(In Mathlib the integers *as a multiplicative group* are `Multiplicative ℤ`, and `ofAdd n` is
`n` seen there.) Proof by induction over the integers: `φ(n + 1) = φ(n) φ(1)` and
`φ(n − 1) = φ(n) φ(1)⁻¹`. -/
theorem int_hom_eq_zpow (φ : Multiplicative ℤ →* G) (n : ℤ) :
    φ (Multiplicative.ofAdd n) = φ (Multiplicative.ofAdd 1) ^ n := by
  induction n using Int.induction_on with
  | zero => simp
  | succ k ih =>
    calc φ (Multiplicative.ofAdd ((k : ℤ) + 1))
        = φ (Multiplicative.ofAdd (k : ℤ) * Multiplicative.ofAdd 1) := rfl
      _ = φ (Multiplicative.ofAdd (k : ℤ)) * φ (Multiplicative.ofAdd 1) := φ.map_mul _ _
      _ = φ (Multiplicative.ofAdd 1) ^ (k : ℤ) * φ (Multiplicative.ofAdd 1) := by rw [ih]
      _ = φ (Multiplicative.ofAdd 1) ^ ((k : ℤ) + 1) := (zpow_add_one _ _).symm
  | pred k ih =>
    calc φ (Multiplicative.ofAdd (-(k : ℤ) - 1))
        = φ (Multiplicative.ofAdd (-(k : ℤ)) * (Multiplicative.ofAdd 1)⁻¹) := rfl
      _ = φ (Multiplicative.ofAdd (-(k : ℤ))) * (φ (Multiplicative.ofAdd 1))⁻¹ := by
          rw [φ.map_mul, φ.map_inv]
      _ = φ (Multiplicative.ofAdd 1) ^ (-(k : ℤ)) * (φ (Multiplicative.ofAdd 1))⁻¹ := by rw [ih]
      _ = φ (Multiplicative.ofAdd 1) ^ (-(k : ℤ) - 1) := (zpow_sub_one _ _).symm

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

intHomEquivLean 4Formally verified

/-- **`Hom(ℤ, G) ≃ G`**: evaluating at `1` is a bijection from group homomorphisms `ℤ → G` to
elements of `G`; the inverse sends `g` to `n ↦ gⁿ` (Mathlib's `zpowersHom`). Injectivity is
`int_hom_eq_zpow`. The pair `(ℤ, 1)` is a universal element of the forgetful functor. -/
def intHomEquiv : (Multiplicative ℤ →* G) ≃ G where
  toFun φ := φ (Multiplicative.ofAdd 1)
  invFun g := zpowersHom G g
  left_inv φ := by
    refine MonoidHom.ext fun n => ?_
    have h := int_hom_eq_zpow φ (Multiplicative.toAdd n)
    rw [ofAdd_toAdd] at h
    simp [h]
  right_inv g := by simp

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

int_hom_equiv_naturalLean 4Proved here from basic factsFormally verified

/-- The bijection `Hom(ℤ, G) ≃ G` is **natural in `G`**: composing with a homomorphism
`f : G → H` on the left corresponds to applying `f` to the element. This is what makes it a
natural isomorphism `Hom(ℤ, −) ≅ U` with the forgetful functor `U`, not just a family of
bijections. -/
theorem int_hom_equiv_natural (f : G →* H) (φ : Multiplicative ℤ →* G) :
    intHomEquiv (f.comp φ) = f (intHomEquiv φ) :=
  rfl

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

forget_grp_corepresentableLean 4Applies a library theoremFormally verified

/-- **The forgetful functor `Grp ⥤ Set` is corepresentable**, in Mathlib's category `GrpCat`
of groups. This applies Mathlib's instance `GrpCat.forget_isCorepresentable`, built from the
natural isomorphism `GrpCat.coyonedaObjIsoForget : Hom(ℤ, −) ≅ forget` (with `ℤ` lifted to
the right universe). -/
theorem forget_grp_corepresentable : (forget GrpCat.{u}).IsCorepresentable :=
  inferInstance

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

Universal elements: Theorems 1 and 2 in full generality. The definition, both directions of Theorem 1, the bijection between them, and the uniqueness theorem. The proof of universal_unique follows the human proof line by line: build $\varphi$ and $\psi$ , then compare $\psi \circ \varphi$ with the identity using the uniqueness clause.

IsUniversalLean 4Formally verified

/-- An element `x ∈ F(A)` of a functor `F : C ⥤ Set` is **universal** if every element of
every `F(B)` is obtained from `x` along exactly one arrow: for all `B` and `y ∈ F(B)` there is
a unique `f : A ⟶ B` with `F(f)(x) = y`. Example: `1 ∈ U(ℤ)` for the forgetful functor on
groups. -/
def IsUniversal {A : C} (x : F.obj A) : Prop :=
  ∀ (B : C) (y : F.obj B), ∃! f : A ⟶ B, F.map f x = y

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

universal_of_corepresentableLean 4Proved here from basic factsFormally verified

/-- **A representation gives a universal element**: if `e : Hom(A, −) ≅ F`, then
`x = e(id_A)` is universal. Given `y ∈ F(B)`, the arrow is `e⁻¹(y)`; it works because
`F(f)(e(id_A)) = e(id_A ≫ f) = e(f)` by naturality, and it is unique because `e` is
injective. -/
theorem universal_of_corepresentable {A : C} (e : F.CorepresentableBy A) :
    IsUniversal F (e.homEquiv (𝟙 A)) := by
  intro B y
  refine ⟨e.homEquiv.symm y, ?_, ?_⟩
  · show F.map (e.homEquiv.symm y) (e.homEquiv (𝟙 A)) = y
    rw [← e.homEquiv_comp, Category.id_comp, Equiv.apply_symm_apply]
  · intro f hf
    rw [← hf, ← e.homEquiv_comp, Category.id_comp, Equiv.symm_apply_apply]

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

corepresentableOfUniversalLean 4Formally verified

/-- **A universal element gives a representation**: if `x ∈ F(A)` is universal, then
`f ↦ F(f)(x)` is a natural bijection `Hom(A, B) ≃ F(B)`. Bijectivity is exactly the
"exists unique" in the definition; naturality is functoriality of `F`. -/
noncomputable def corepresentableOfUniversal {A : C} {x : F.obj A} (h : IsUniversal F x) :
    F.CorepresentableBy A where
  homEquiv {B} := Equiv.ofBijective (fun f : A ⟶ B => F.map f x)
    ⟨fun _ g hfg => (h B (F.map g x)).unique hfg rfl,
     fun y => (h B y).exists⟩
  homEquiv_comp g f := Functor.map_comp_apply F f g x

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

corepresentable_equiv_universalLean 4Proved here from basic factsFormally verified

/-- **Representations of `F` by `A` correspond exactly to universal elements of `F(A)`.**
The two constructions above are mutually inverse: a representation is determined by where it
sends `id_A` (Mathlib's `CorepresentableBy.ext`), and `F(id_A)(x) = x`. -/
theorem corepresentable_equiv_universal {A : C} :
    Nonempty (F.CorepresentableBy A ≃ {x : F.obj A // IsUniversal F x}) :=
  ⟨{ toFun := fun e => ⟨e.homEquiv (𝟙 A), universal_of_corepresentable e⟩
     invFun := fun x => corepresentableOfUniversal x.2
     left_inv := fun e => by
       apply Functor.CorepresentableBy.ext
       exact Functor.map_id_apply F A _
     right_inv := fun x => by
       apply Subtype.ext
       exact Functor.map_id_apply F A _ }⟩

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

universal_uniqueLean 4Proved here from basic factsFormally verified

/-- **Universal elements are unique up to unique isomorphism.** If `(A, x)` and `(A', x')`
are both universal for `F`, there is an isomorphism `e : A ≅ A'` with `F(e)(x) = x'`, and it is
the *only* arrow `A ⟶ A'` sending `x` to `x'`.
Proof: universality gives `f : A ⟶ A'` with `F(f)(x) = x'` and `g : A' ⟶ A` with
`F(g)(x') = x`. Then `g ∘ f` and `id_A` both send `x` to `x`, so they are equal by the
uniqueness clause for `(A, x)`; likewise `f ∘ g = id_{A'}`. -/
theorem universal_unique {A A' : C} {x : F.obj A} {x' : F.obj A'}
    (h : IsUniversal F x) (h' : IsUniversal F x') :
    ∃ e : A ≅ A', F.map e.hom x = x' ∧ ∀ f : A ⟶ A', F.map f x = x' → f = e.hom := by
  obtain ⟨f, hf, hf_uniq⟩ := h A' x'
  obtain ⟨g, hg, -⟩ := h' A x
  have hgf : f ≫ g = 𝟙 A := by
    apply (h A x).unique
    · rw [Functor.map_comp_apply, hf, hg]
    · rw [Functor.map_id_apply]
  have hfg : g ≫ f = 𝟙 A' := by
    apply (h' A' x').unique
    · rw [Functor.map_comp_apply, hg, hf]
    · rw [Functor.map_id_apply]
  exact ⟨⟨f, g, hgf, hfg⟩, hf, fun f' hf' => hf_uniq f' hf'⟩

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

Not every functor is representable (Proposition 5). A corepresentable functor on types has at most one element over the one-point type, and so the covariant power-set functor has no corepresentation at all — IsEmpty of the type of corepresentations.

subsingleton_of_corepresentableLean 4Proved here from basic factsFormally verified

/-- **A necessary condition.** If a functor `F : Set ⥤ Set` is corepresentable, then `F` of a
one-point set has at most one element — because there is exactly one map from any set to a
point. So a functor whose value at the point has two distinct elements cannot be
corepresentable: not every functor to `Set` is representable. -/
theorem subsingleton_of_corepresentable {F : Type ⥤ Type} {A : Type}
    (e : F.CorepresentableBy A) : Subsingleton (F.obj PUnit) := by
  constructor
  intro y y'
  rw [← e.homEquiv.apply_symm_apply y, ← e.homEquiv.apply_symm_apply y']
  congr 1
  ext a

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

imagePowersetLean 4Formally verified

/-- The **covariant power-set functor**: a set goes to its set of subsets, and `f : X → Y` to
the direct-image map `S ↦ f(S)`. Same objects as `powerset`, arrows the other way. -/
def imagePowerset : Type ⥤ Type where
  obj X := Set X
  map f := ↾fun S => (f : _ → _) '' S
  map_id X := by
    ext S
    simp
  map_comp f g := by
    ext S
    simp [Set.image_image]

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

image_powerset_not_corepresentableLean 4Proved here from basic factsFormally verified

/-- **The covariant power-set functor is not corepresentable** (while the contravariant one is
represented by `Bool`). Its value at a point, `Set PUnit = {∅, {⋆}}`, has two elements, which
`subsingleton_of_corepresentable` forbids. -/
theorem image_powerset_not_corepresentable (A : Type) :
    IsEmpty (imagePowerset.CorepresentableBy A) := by
  constructor
  intro e
  have hsub := subsingleton_of_corepresentable e
  have h : (∅ : Set PUnit) = Set.univ := hsub.elim _ _
  have hmem : PUnit.unit ∈ (∅ : Set PUnit) := by
    rw [h]
    exact Set.mem_univ _
  exact hmem

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

Universal properties as representations (Theorem 4). Products and quotients of types are proved here; free monoids and limits apply Mathlib (FreeMonoid.lift, IsLimit.ofRepresentableBy).

pairsOfMapsLean 4Formally verified

/-- The functor `X ↦ Hom(X, A) × Hom(X, B)` (pairs of maps out of `X`), contravariant in `X`:
a map `f : Y → X` turns a pair `(p, q)` into `(p ∘ f, q ∘ f)`. -/
def pairsOfMaps (A B : Type) : Typeᵒᵖ ⥤ Type where
  obj X := (X.unop → A) × (X.unop → B)
  map f := ↾fun pq => (pq.1 ∘ f.unop, pq.2 ∘ f.unop)

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

product_representsLean 4Proved here from basic factsFormally verified

/-- **The product represents pairs of maps**: `Hom(X, A × B) ≃ Hom(X, A) × Hom(X, B)`,
naturally in `X`, by `h ↦ (π₁ ∘ h, π₂ ∘ h)` with inverse `(p, q) ↦ ⟨p, q⟩`. This is exactly the
universal property of the product, read as a representation. -/
theorem product_represents (A B : Type) : Nonempty ((pairsOfMaps A B).RepresentableBy (A × B)) :=
  ⟨{ homEquiv :=
      { toFun := fun h => (Prod.fst ∘ h, Prod.snd ∘ h)
        invFun := fun pq => ↾fun x => (pq.1 x, pq.2 x)
        left_inv := fun _ => rfl
        right_inv := fun _ => rfl }
     homEquiv_comp := fun _ _ => rfl }⟩

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

respectingMapsLean 4Formally verified

/-- For an equivalence relation `s` on `X`, the covariant functor sending `Y` to the maps
`X → Y` that are constant on equivalence classes (`a ≈ b → f a = f b`). -/
def respectingMaps {X : Type} (s : Setoid X) : Type ⥤ Type where
  obj Y := {f : X → Y // ∀ a b, a ≈ b → f a = f b}
  map g := ↾fun f => ⟨(g : _ → _) ∘ f.1, fun a b hab => by simp [f.2 a b hab]⟩

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

quotient_corepresentsLean 4Proved here from basic factsFormally verified

/-- **The quotient corepresents maps that respect the relation**:
`Hom(X ⧸ ~, Y) ≃ {f : X → Y | a ~ b → f a = f b}`, naturally in `Y`, by composing with the
quotient map. Surjectivity is `Quotient.lift` ("a respecting map factors through the
quotient") and injectivity holds because every element of `X ⧸ ~` is a class `[a]`. -/
theorem quotient_corepresents {X : Type} (s : Setoid X) :
    Nonempty ((respectingMaps s).CorepresentableBy (Quotient s)) :=
  ⟨{ homEquiv :=
      { toFun := fun h => ⟨(h : _ → _) ∘ Quotient.mk s, fun a b hab => by
          simp [Quotient.sound hab]⟩
        invFun := fun f => ↾Quotient.lift f.1 f.2
        left_inv := fun h => by
          ext q
          induction q using Quotient.ind
          rfl
        right_inv := fun _ => rfl }
     homEquiv_comp := fun _ _ => rfl }⟩

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

free_monoid_universalLean 4Applies a library theoremFormally verified

/-- **The free monoid represents "maps of the generators"**: every function `f : α → M` into a
monoid extends to exactly one monoid homomorphism `FreeMonoid α → M` (words are sent to
products). This applies Mathlib's `FreeMonoid.lift` and `FreeMonoid.hom_eq`; it says that
`(FreeMonoid α, of)` is a universal element of `M ↦ (α → M)`. -/
theorem free_monoid_universal {α M : Type*} [Monoid M] (f : α → M) :
    ∃! φ : FreeMonoid α →* M, ∀ a, φ (FreeMonoid.of a) = f a :=
  ⟨FreeMonoid.lift f, fun a => FreeMonoid.lift_eval_of f a,
    fun ψ hψ => FreeMonoid.hom_eq fun a => by rw [hψ a, FreeMonoid.lift_eval_of]⟩

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

limit_of_representableLean 4Applies a library theoremFormally verified

/-- **Limits are representing objects.** For a diagram `K : J ⥤ C`, a representation of the
functor `X ↦ {cones over K with apex X}` by an object `L` makes the cone corresponding to `id_L`
a limit cone. This applies Mathlib's `IsLimit.ofRepresentableBy`. -/
theorem limit_of_representable {J C : Type*} [Category J] [Category C] {K : J ⥤ C} {L : C}
    (h : K.cones.RepresentableBy L) :
    Nonempty (Limits.IsLimit (Limits.IsLimit.OfNatIso.limitCone h)) :=
  ⟨Limits.IsLimit.ofRepresentableBy h⟩

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

What is and is not formalised. Theorems 1 and 2 are proved independently for every locally small category and every functor to types. Theorem 3 is proved independently (with Mathlib's category-level statement cited alongside), Theorem 4 is proved for products and quotients in Type and cited from Mathlib for free monoids and limits, and Proposition 5 is proved for functors on Type. The open-set, ring and free-group examples and Freyd's criterion are not formalised in this module.

ComputationC

Counting arrows

Representability makes counting predictions: if $G \mapsto \{g \mid g^n = 1\}$ is represented by $\Z/n$ , then the number of homomorphisms $\Z/n \to G$ must equal the number of elements of $G$ with $g^n = 1$ . The experiment checks this by brute force — trying every function $\Z/n \to S_3$ — and also checks naturality of subsets versus characteristic functions for all maps between small sets, and applies the counting test of Proposition 5 to some functors on finite sets.

Representable functors on finite sets and groups, by brute forcePythonExhaustive finite checkExact computationComputationally tested

"""Representable functors in finite examples: checking and counting.

Three exact, exhaustive checks on small finite sets and groups.
(1) Subsets are characteristic functions: for all sets X, Y with at most 3
elements and all maps f : Y -> X, the characteristic function of f^-1(S) is
chi_S composed with f (naturality of P(X) = Hom(X, 2)).
(2) Homomorphisms out of a presented group are solutions of its relations: we
count all homomorphisms Z/n -> S3 and V4 -> S3 by brute force over every
function and compare with the number of elements g with g^n = 1, and of
commuting pairs of involutions.
(3) A counting test: a representable functor on finite sets has |F(n)| = n^a
(covariant) or a^n (contravariant). Sequences that fit no such formula
belong to functors that cannot be representable.
"""

import itertools

def maps(dom, cod):
    """All functions dom -> cod, as tuples indexed by dom = range(len)."""
    return list(itertools.product(range(cod), repeat=dom))

def subsets(n):
    """All subsets of range(n), as frozensets."""
    return [frozenset(c) for k in range(n + 1)
            for c in itertools.combinations(range(n), k)]

def chi(s, n):
    """The characteristic function of s ⊆ range(n), as a tuple of 0/1."""
    return tuple(1 if x in s else 0 for x in range(n))

def preimage(f, s):
    """f^-1(s) for f given as a tuple."""
    return frozenset(y for y, fy in enumerate(f) if fy in s)

def powerset_naturality(max_size=3):
    """Check chi(f^-1(S)) = chi(S) ∘ f for all f : Y -> X, S ⊆ X; return the
    number of checks and the number of failures."""
    checks = failures = 0
    for n in range(max_size + 1):
        for m in range(max_size + 1):
            for f in maps(m, n):
                for s in subsets(n):
                    checks += 1
                    lhs = chi(preimage(f, s), m)
                    rhs = tuple(chi(s, n)[f[y]] for y in range(m))
                    failures += lhs != rhs
    return checks, failures

# Groups as (elements, multiplication function, identity).

def symmetric_group_3():
    """S3 as permutations of (0, 1, 2); (p*q)(i) = p(q(i))."""
    elems = list(itertools.permutations(range(3)))
    return elems, (lambda p, q: tuple(p[q[i]] for i in range(3))), (0, 1, 2)

def cyclic_group(n):
    """Z/n under addition."""
    return list(range(n)), (lambda a, b: (a + b) % n), 0

def klein_four():
    """V4 = Z/2 x Z/2."""
    elems = [(a, b) for a in range(2) for b in range(2)]
    return elems, (lambda x, y: ((x[0] + y[0]) % 2, (x[1] + y[1]) % 2)), (0, 0)

def count_homs(source, target):
    """Brute force: how many of the functions source -> target respect
    multiplication? (Such functions automatically preserve 1 and inverses.)"""
    s_el, s_mul, _ = source
    t_el, t_mul, _ = target
    count = 0
    for images in itertools.product(t_el, repeat=len(s_el)):
        h = dict(zip(s_el, images))
        if all(h[s_mul(a, b)] == t_mul(h[a], h[b]) for a in s_el for b in s_el):
            count += 1
    return count

def power(g, n, mul, one):
    """g^n in a group."""
    result = one
    for _ in range(n):
        result = mul(result, g)
    return result

def nth_roots_of_one(n, group):
    """Number of g with g^n = 1: the size of Hom(Z/n, G) by representability."""
    elems, mul, one = group
    return sum(power(g, n, mul, one) == one for g in elems)

def commuting_involution_pairs(group):
    """Pairs (x, y) with x^2 = y^2 = 1 and xy = yx: Hom(V4, G)."""
    elems, mul, one = group
    return sum(mul(x, x) == one and mul(y, y) == one and mul(x, y) == mul(y, x)
               for x in elems for y in elems)

def fits_covariant(seq):
    """Return a with seq[n] == n**a for all n (0**0 = 1), or None."""
    for a in range(len(seq) + 3):
        if all(s == n ** a for n, s in enumerate(seq)):
            return a
    return None

def fits_contravariant(seq):
    """Return a with seq[n] == a**n for all n, or None."""
    if len(seq) < 2:
        return None
    a = seq[1]
    return a if all(s == a ** n for n, s in enumerate(seq)) else None

def bell(n):
    """Number of equivalence relations on an n-element set."""
    row, total = [1], 1
    for _ in range(n):
        new = [row[-1]]
        for x in row:
            new.append(new[-1] + x)
        row, total = new, new[0]
    return total if n else 1

def main():
    checks, failures = powerset_naturality(3)
    print("1. Subsets versus maps to {0, 1}: chi(f^-1 S) = chi(S) ∘ f")
    print(f"   all f : Y -> X, S ⊆ X with |X|, |Y| <= 3: {checks} checks,"
          f" {failures} failures")
    print()
    s3 = symmetric_group_3()
    print("2. Homomorphisms into S3: brute force versus the relations")
    for n in range(1, 5):
        print(f"   |Hom(Z/{n}, S3)| = {count_homs(cyclic_group(n), s3):<3}"
              f"  #{{g in S3 : g^{n} = 1}} = {nth_roots_of_one(n, s3)}")
    print(f"   |Hom(V4, S3)|  = {count_homs(klein_four(), s3):<3}"
          f"  #{{(x, y) : x^2 = y^2 = 1, xy = yx}} = "
          f"{commuting_involution_pairs(s3)}")
    print()
    print("3. Counting test on sets of size n = 0..5 (representable => fits)")
    rows = [
        ("contravariant  X -> P(X), preimage", [2 ** n for n in range(6)], "contra"),
        ("contravariant  X -> equivalence relations",
         [bell(n) for n in range(6)], "contra"),
        ("covariant      X -> X × X", [n * n for n in range(6)], "co"),
        ("covariant      X -> P(X), direct image", [2 ** n for n in range(6)], "co"),
        ("covariant      X -> X ⊔ X", [2 * n for n in range(6)], "co"),
    ]
    for label, seq, kind in rows:
        a = fits_contravariant(seq) if kind == "contra" else fits_covariant(seq)
        verdict = f"fits with |A| = {a}" if a is not None else "fits no |A|"
        print(f"   {label:<42} {verdict}")
        print(f"      sizes {seq}")
    print()
    print("Epistemic status: exhaustive, exact checks in these finite cases. "
          "Part 2\nconfirms Hom(Z/n, G) = {g : g^n = 1} for G = S3 only. In "
          "part 3 a\nsequence that fits proves nothing by itself (naturality "
          "is also needed),\nbut one that fits no formula proves that the "
          "functor is not representable.")

if __name__ == "__main__":
    main()

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

What to notice: $|\Hom(\Z/n, S_3)|$ is $1, 4, 3, 4$ for $n = 1, 2, 3, 4$ , exactly the number of solutions of $g^n = 1$ in $S_3$ (the identity, three transpositions, two 3-cycles). The Klein four-group $V_4 = \langle a, b \mid a^2, b^2, ab = ba \rangle$ gives $10$ homomorphisms, one for each commuting pair of elements of order dividing $2$ . In part 3, a functor whose sizes fit no formula $n^a$ or $a^n$ cannot be representable; a sequence that does fit (like $2^n$ for subsets) is consistent with representability but does not prove it — naturality matters too. This is exhaustive evidence for finitely many cases, not a proof.

Explore

Explore: the product as a representing object

The product $A \times B$ represents the functor "pairs of maps into $A$ and $B$ ". In the widget, choose maps $f : Z \to A$ and $g : Z \to B$ ; then try to build a map $h : Z \to A \times B$ with $\pi_1 \circ h = f$ and $\pi_2 \circ h = g$ . Notice that you have no freedom at all: each $h(z)$ is forced to be $(f(z), g(z))$ . That forced, unique choice is what "the pair $(\pi_1, \pi_2)$ is a universal element" means.

The product, by its maps

Choose maps f : Z → A and g : Z → B. Then try to build a map h : Z → A × B that projects back to f and g.

f : Z → A

f(p) =f(q) =f(r) =

g : Z → B

g(p) =g(q) =g(r) =

⟨f, g⟩ : Z → A × B

p ↦ (red, 2) q ↦ (blue, 2) r ↦ (red, 3)

Your turn: choose h(p), h(q), h(r) by clicking cells.

A × B	1	2	3
red
blue

\Hom(Z, A \times B) \cong \Hom(Z, A) \times \Hom(Z, B)

, naturally in

Z

: the universal element is the pair of projections.

Exercises

1. Representable functors

Warm-upHuman

Which pair $(A, u)$ is a universal element of the forgetful functor $U : \cat{Ab} \to \cat{Set}$ from abelian groups to sets?

Choose one

(\Z, 1)

(\Z/2, 1)

(\{0\}, 0)

(\Q, 1)

2. Representable functors

CoreHuman

The group $\Z^2 = \langle a, b \mid ab = ba \rangle$ represents the functor sending a group $G$ to the set of commuting pairs $\{(x, y) \in G^2 \mid xy = yx\}$ . How many group homomorphisms $\Z^2 \to S_3$ are there?

3. Representable functors

CoreHuman

How many different natural isomorphisms $\Hom(\Z, -) \Rightarrow U$ are there, where $U : \cat{Grp} \to \cat{Set}$ is the forgetful functor?

4. Representable functors

CoreHuman

Which pairs $(A, u)$ with $u \subseteq A$ are universal elements of the contravariant power-set functor $\mathcal{P} : \cat{Set}^{\mathrm{op}} \to \cat{Set}$ (acting by preimage)? Choose all that apply.

Choose all that apply

(\{0, 1\}, \{1\})

(\{0, 1\}, \{0\})

(\{0, 1\}, \varnothing)

(\{0, 1, 2\}, \{1\})

5. Representable functors

CoreHuman

In the proof of Theorem 2 we have $\varphi : A \to A'$ with $F(\varphi)(u) = u'$ and $\psi : A' \to A$ with $F(\psi)(u') = u$ . Why is $\psi \circ \varphi = \id_A$ ?

Choose one

Both

\psi \circ \varphi

and

\id_A

send

u

u

, and by universality of

(A, u)

only one arrow

A \to A

does.Because

F

is faithful.Because

\varphi

and

\psi

are isomorphisms.Because

F(\psi \circ \varphi) = F(\id_A)

as functions on all of

F(A)

6. Representable functors

CoreHuman

Which of these functors $\cat{Set} \to \cat{Set}$ is not representable?

Choose one

X \mapsto X \times X \times X

X \mapsto \{\ast\}

(constant one-point set)

X \mapsto \mathcal{P}(X)

, with

f

acting by direct image

S \mapsto f(S)

X \mapsto X

(the identity functor)

7. Representable functors

StretchHuman

Let $\mathcal{F} : \cat{Top}^{\mathrm{op}} \to \cat{Set}$ send a space to its set of closed subsets (a continuous map acts by preimage). Which pair represents $\mathcal{F}$ ? Here $\mathbb{S} = \{0, 1\}$ is the Sierpiński space with open sets $\varnothing, \{1\}, \{0, 1\}$ .

Choose one

(\mathbb{S}, \{0\})

(\{0, 1\} \text{ discrete}, \{0\})

(\{0, 1\} \text{ indiscrete}, \{0\})

(\mathbb{S}, \{1\})

8. Representable functors

CoreFormal

In the lesson's Lean file, imagePowerset : Type ⥤ Type is the covariant power-set functor (direct images). Which Lean statement says that it is not representable, i.e. that no type $A$ represents it?

Choose one

∀ A : Type, IsEmpty (imagePowerset.CorepresentableBy A)Nonempty (powerset.RepresentableBy Bool)∀ A : Type, Nonempty (imagePowerset.CorepresentableBy A)Subsingleton (imagePowerset.obj PUnit)

9. Representable functors

CoreComputational

Since $\Z/n = \langle a \mid a^n \rangle$ represents $G \mapsto \{g \in G \mid g^n = 1\}$ , the number of homomorphisms $\Z/n \to \Z/m$ equals the number of $k \in \Z/m$ with $nk \equiv 0 \pmod m$ . Write hom_count(n, m) computing this number (for $n, m \ge 1$ ). Then compare your answers with $\gcd(n, m)$ .

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

Common misconceptionsH

Common misconceptions

Misconception

"Every functor to $\cat{Set}$ is representable." Far from it. The covariant power-set functor, the constant two-element functor and the equivalence-relation functor are not, by simple counting (Proposition 5). Representability is a strong condition: a covariant representable functor preserves every limit that exists.

Misconception

Confusing covariant and contravariant representability. $\Hom(A, -)$ is covariant (arrows out of $A$ ); $\Hom(-, A)$ is contravariant (arrows into $A$ ). Subsets are represented contravariantly by $\{0, 1\}$ — a subset of $X$ is a map $X \to \{0, 1\}$ , and maps act by preimage. The same objects with direct images form a covariant functor that is not representable at all. Before asking "what represents $F$ ?", check which way $F$ acts on arrows.

Misconception

"The representing object is unique, so the representation is unique." The object is unique up to isomorphism, but a representation also includes the natural isomorphism, equivalently the universal element. $\Z$ represents $U : \cat{Grp} \to \cat{Set}$ in exactly two ways, with universal elements $1$ and $-1$ (Exercise). What is unique is the isomorphism between two representations once their universal elements are fixed (Theorem 2).

Misconception

"Representable means equal to a hom functor." It means naturally isomorphic to one. $\mathcal{P}(X)$ is a set of subsets, not literally a set of functions; the content of the statement is the natural bijection $S \mapsto \chi_S$ . (In Lean, where Set X is defined as X → Prop, the power set happens to be represented by Prop on the nose.)

Misconception

"A generator is a universal element." Universality is relative to the functor. The element $1 \in \Z/6$ is a universal element of the functor $G \mapsto \{g \in G \mid g^6 = 1\}$ , but not of the forgetful functor $U : \cat{Grp} \to \cat{Set}$ : there is no homomorphism $\Z/6 \to \Z$ sending $1$ to $1$ , so the "exists" half fails. And a set $A$ with $|A| \ge 2$ fails to represent the identity functor through any of its elements because the "unique" half fails: many functions $A \to X$ send a given point to $x$ .

ViewpointsH

Viewpoints

Algebra— Presentations, free objects and tensor products

To the algebraist, representability is the reason presentations work. The group $\langle S \mid R \rangle$ is defined to represent the functor " $S$ -tuples of elements satisfying $R$ ". So $\Z/n = \langle a \mid a^n \rangle$ represents $n$ -th roots of $1$ , and $\Z^2 = \langle a, b \mid ab = ba \rangle$ represents commuting pairs. Counting gives real theorems: the number of commuting pairs in a finite group is $|\Hom(\Z^2, G)| = |G| \cdot k(G)$ , where $k(G)$ is the number of conjugacy classes (for $S_3$ : $6 \cdot 3 = 18$ ). For modules over a commutative ring $R$ , the tensor product $M \otimes_R N$ is the representing object of $P \mapsto \{R\text{-bilinear maps } M \times N \to P\}$ — its universal element is $(m, n) \mapsto m \otimes n$ — and this, not a choice of construction, is what one uses in practice. See groups.

Geometry— The functor of points and moduli spaces

Grothendieck's algebraic geometry turns the motivation upside down. A geometric object $X$ is studied through its functor of points $R \mapsto X(R)$ , the solutions of its equations with coordinates in each commutative ring $R$ : the circle $x^2 + y^2 = 1$ has the rational points $\left(\tfrac{a^2 - b^2}{a^2 + b^2}, \tfrac{2ab}{a^2 + b^2}\right)$ (Pythagorean triples), points over $\Z/p$ , over $\C$ , and so on, all at once. An affine scheme is precisely a representable functor on commutative rings, represented by its coordinate ring. A moduli problem asks for a space whose points classify some objects: the Grassmannian scheme $\mathrm{Gr}(k, n)$ represents the functor whose value on $\operatorname{Spec} R$ is the set of rank- $k$ direct summands of $R^n$ (over a field $F$ : the $k$ -dimensional subspaces of $F^n$ ). Some natural moduli functors are not representable — the functor of elliptic curves up to isomorphism fails because elliptic curves have automorphisms such as $P \mapsto -P$ — which leads to coarse moduli spaces (the $j$ -line) and to stacks. See algebraic geometry.

Topology— Classifying spaces and Brown representability

In topology, representing objects are classifying spaces. The Sierpiński space represents open sets, as above. Much deeper: on the homotopy category of pointed connected CW complexes, E. H. Brown's representability theorem (1962) says that every contravariant functor to sets that turns wedge sums into products and satisfies a Mayer–Vietoris condition is representable. Applied to singular cohomology it gives Eilenberg–MacLane spaces $K(G, n)$ with

H^n(X; G) \cong [X, K(G, n)]

(homotopy classes of maps) for CW complexes $X$ ; for instance $K(\Z, 1)$ is the circle and $K(\Z/2, 1)$ is $\mathbb{RP}^\infty$ . Similarly, isomorphism classes of real vector bundles of rank $n$ over a paracompact space $X$ correspond to $[X, \mathrm{Gr}_n(\R^\infty)]$ , so characteristic classes are cohomology classes of the classifying space. See algebraic topology.

Computation— Representable containers and memoisation

A functional programmer meets representable functors as containers. A container type F a is representable if F a ≅ (K → a) naturally in a for some index type K: pairs (a, a) with K = Bool, vectors of length $n$ with K = Fin n, infinite streams with K = ℕ. Lists are not: at the empty type there is one list (the empty one), which forces K to be empty, yet there are infinitely many lists of booleans — Proposition 5 in disguise. The isomorphism is the basis of memoisation: a function ℕ → a can be stored as the lazy stream of its values and looked up instead of recomputed.

Logic— Truth values as a representing object

The object representing "subsets" is an object of truth values: $\{0, 1\}$ for sets, the Sierpiński space for open sets. In Lean, Set X is defined to be X → Prop, so the power-set functor is represented by Prop definitionally, and representing it by Bool instead needs classical logic, because turning a proposition into a boolean requires deciding it. In an elementary topos the representing object of subobjects is the subobject classifier $\Omega$ , and its internal logic is in general intuitionistic, not two-valued; see elementary topoi. Informally, the Sierpiński space fits this picture too: its "truth values" behave like observable properties, confirmed as soon as evidence is seen but never certified false by any finite observation.

Wonder Trails

Wonder Trail

The universal property of the product, explored from first principles with finite sets: exactly the statement that $(\pi_1, \pi_2)$ is a universal element.

Wonder Trail · Optional · never gradedThe product, by its mapsCan you describe the set of pairs

A \times B

without ever looking inside it — only by how functions go into it?Follow the trail

History & global context

History and global context

Universal mapping problems were formulated by Pierre Samuel in "On universal mappings and free topological groups" (Bulletin of the AMS, 1948), and systematised by Bourbaki in the chapter on structures of Théorie des ensembles (1957).
Daniel Kan introduced adjoint functors in 1958; universal elements and adjunctions are two faces of the same idea.
Alexander Grothendieck made representable functors the backbone of algebraic geometry in his Séminaire Bourbaki lectures of 1959–62 (collected as Fondements de la géométrie algébrique), constructing Hilbert and Picard schemes as representing objects and asking of each moduli problem whether its functor is representable.
In topology, Samuel Eilenberg and Saunders Mac Lane constructed the spaces $K(G, n)$ in the 1940s and 50s, and Edgar H. Brown Jr. proved his representability theorem in "Cohomology theories" (Annals of Mathematics, 1962).
The Sierpiński space is named after the Polish mathematician Wacław Sierpiński. Nobuo Yoneda's lemma (1954), the subject of the next lesson, is the general principle behind Theorem 1.

Elements as arrows

Probing with a test object

Definitions

Examples and non-examples

The main theorems

Representable functors in Lean

Counting arrows

Explore: the product as a representing object

Exercises

Common misconceptions

Viewpoints

Wonder Trail

History and global context

Further reading