yoneda_ai is an AI-assisted formal monograph and mathematical study dedicated to category theory, natural transformations, and constructive proofs of the celebrated Yoneda Lemma and its consequences.
The monograph investigates both covariant and contravariant formulations of representable functors, proving that an object in a locally small category is completely determined up to isomorphism by the network of its morphisms with other objects.
| [GitHub] | Source Repository — formal LaTeX sources, diagram definitions, and development notes. |
|---|---|
| [link] | Release v0.1 — official GitHub release tagged artifact. |
| [PDF] | The Monograph (PDF) — complete monograph text, diagrams, and proofs. |
| [Diagrams] | Interactive Commutative Diagrams — SVG category theory commutative diagrams and Yoneda functor visualization. |
| [Home] | Return to Obelisk About Page. |
Let \(\mathcal{C}\) be a locally small category. For any object \(A \in \mathrm{Ob}(\mathcal{C})\), the contravariant hom-functor (presheaf): \[ h_A = \mathrm{Hom}_{\mathcal{C}}(-, A) : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set} \] maps an object \(X\) to the set of morphisms \(\mathrm{Hom}_{\mathcal{C}}(X, A)\), and a morphism \(f : X \to Y\) to pre-composition \(-\circ f : \mathrm{Hom}_{\mathcal{C}}(Y, A) \to \mathrm{Hom}_{\mathcal{C}}(X, A)\).
For every object \(A \in \mathcal{C}\) and every presheaf \(F : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set}\), there exists a natural bijection: \[ \Phi_{A, F} : \mathrm{Nat}\big(\mathrm{Hom}_{\mathcal{C}}(-, A), F\big) \overset{\sim}{\longrightarrow} F(A) \] given by evaluating a natural transformation \(\alpha\) at the identity morphism: \[ \Phi_{A, F}(\alpha) = \alpha_A(\mathrm{id}_A) \in F(A). \] The inverse mapping constructs for every element \(u \in F(A)\) a natural transformation \(\alpha^{(u)}\) whose components \(\alpha^{(u)}_X : \mathrm{Hom}_{\mathcal{C}}(X, A) \to F(X)\) are defined by: \[ \alpha^{(u)}_X(f) = (F(f))(u). \]
As a direct corollary, setting \(F = h_B = \mathrm{Hom}_{\mathcal{C}}(-, B)\) yields: \[ \mathrm{Nat}\big(h_A, h_B\big) \cong \mathrm{Hom}_{\mathcal{C}}(A, B). \] Hence the Yoneda functor: \[ y : \mathcal{C} \to \mathbf{Set}^{\mathcal{C}^{\mathrm{op}}}, \quad A \mapsto h_A \] is fully faithful. In particular, \(h_A \cong h_B\) as presheaves if and only if \(A \cong B\) in \(\mathcal{C}\).
In traditional set theories (ZFC), the collection of all sets or the category of sets \(\mathbf{Set}\) cannot be formed as a set. In the Morse-Kelley (MK) class theory underlying the Obelisk Proof Assistant, a rigorous distinction is maintained: