Lemme de Yoneda calculé — catégories finies

Série Serre 100, voie décorrelée (EPIC #16334, grain 8). Ce notebook est le miroir exécutable du module YonedaLemma.lean du lake grothendieck_lean — là-bas, yoneda_equiv, yoneda_full et yoneda_faithful sont démontrés en Lean ; ici, sur des catégories finies, ils sont vérifiés par énumération exhaustive : on liste toutes les transformations naturelles, et on constate que

\[\mathrm{Nat}(h_X, F) \;\cong\; F(X) \qquad \text{et} \qquad \mathrm{Nat}(h_X, h_Y) \;\cong\; \mathrm{Hom}(Y, X)\]

exactement comme l’énonce le lemme. Le lemme de Yoneda (1960, dans le sillage de Grothendieck et de la théorie des faisceaux que Serre avait lancée avec FAC) dit qu’un objet est entièrement déterminé par les flèches qui en partent — « tell me who you map to, and I’ll tell you who you are ».

Le pont avec le notebook 03 : un poset est une catégorie (au plus une flèche entre deux points), et pour cette catégorie le foncteur représentable \(h_x = \mathrm{Hom}(x, -)\) est exactement l’ouvert minimal \(U_x = \{y \geq x\}\) du notebook Čech. Le recouvrement par les ouverts minimaux est l’image du plongement de Yoneda — la topologie du notebook 03 se relit en langage catégorique.

Plan

  1. Catégories finies : objets, hom-sets, composition
  2. Foncteurs vers les ensembles finis ; représentables \(h_X = \mathrm{Hom}(X, -)\)
  3. Transformations naturelles par énumération exhaustive
  4. Le lemme : \(\alpha \mapsto \alpha_X(\mathrm{id}_X)\) est une bijection, calculée
  5. Plein et fidèle : \(\mathrm{Nat}(h_X, h_Y) \cong \mathrm{Hom}(Y, X)\)
  6. Le pont Čech : \(h_x = U_x\) sur le cercle à 4 points
  7. Exercices
# Dependances : stdlib uniquement (itertools). Aucun autre requis.
from itertools import product
print("imports OK")
imports OK

1. Une catégorie finie

Une (petite) catégorie, c’est : des objets ; pour chaque paire \((a,b)\) un ensemble fini \(\mathrm{Hom}(a,b)\) de flèches ; une identité par objet ; une composition \(\mathrm{Hom}(b,c) \times \mathrm{Hom}(a,b) \to \mathrm{Hom}(a,c)\), \((g,f) \mapsto g \circ f\), associative avec neutres. On encode ça en trois dictionnaires — tout le reste du notebook ne manipule que cette structure.

Deux familles d’exemples suffisent : les posets (au plus une flèche \(a \to b\), présente ssi \(a \leq b\) ; la composition est la transitivité) et les monoïdes (un seul objet ; les flèches sont les éléments, la composition est la loi).

Témoignage de Serre — les axiomes et leurs exemples (« À propos de la correspondance Grothendieck-Serre », dialogue Serre–Connes, Fondation Hugot du Collège de France, 2019 (YouTube pOv-ygSynRI), 07:08) :

« Il y avait des axiomes sur les catégories abéliennes, mais pas seulement. Il y avait au niveau des exemples. »

(transcription automatique, noms propres corrigés). Ce carnet prend le second membre au sérieux : une catégorie finie, calculée cellule par cellule, là où la théorie générale pose ses axiomes.

def categorie(obj, hom, idn, comp):
    """Categorie finie : hom[(a,b)] = tuple des fleches a->b,
    idn[x] = fleche identite, comp[(g,f)] = g . f pour g: b->c, f: a->b."""
    return {"obj": list(obj), "hom": hom, "idn": idn, "comp": comp}

def cat_poset(P):
    """Poset (dict x -> {y : x <= y}) vu comme categorie : 0 ou 1 fleche par paire."""
    obj = list(P)
    hom, idn, comp = {}, {}, {}
    for a in obj:
        for b in obj:
            if b in P[a]:
                hom[(a, b)] = ((a, b),)
    for x in obj:
        idn[x] = (x, x)
    for (a, b), _ in hom.items():
        for (b2, c), _ in hom.items():
            if b2 == b:
                comp[((b, c), (a, b))] = (a, c)
    return categorie(obj, hom, idn, comp)

def cat_monoide(elements, produit, neutre):
    """Monoide vu comme categorie a un objet '*'."""
    return categorie(["*"],
                     {("*", "*"): tuple(elements)},
                     {"*": neutre},
                     {(f, g): produit(f, g) for f in elements for g in elements})

def hom_set(C, a, b):
    return C["hom"].get((a, b), ())

# Espace de Sierpinski a<b en categorie, et le groupe Z/2 en categorie :
sierpinski = cat_poset({"a": {"a", "b"}, "b": {"b"}})
z2 = cat_monoide(["e", "t"], lambda u, v: ("e" if u == v else "t"), "e")
print("Sierpinski : fleches", {k: v for k, v in sierpinski['hom'].items()})
print("Z/2 : fleches", z2["hom"][("*", "*")], "- composition t.t =", z2["comp"][("t", "t")])
Sierpinski : fleches {('a', 'a'): (('a', 'a'),), ('a', 'b'): (('a', 'b'),), ('b', 'b'): (('b', 'b'),)}
Z/2 : fleches ('e', 't') - composition t.t = e

2. Foncteurs vers les ensembles finis

Un foncteur \(F : \mathcal{C} \to \mathbf{FinSet}\) associe à chaque objet un ensemble fini et à chaque flèche une fonction, en respectant identités et composition. Le plus important de tous : le représentable

\[h_X = \mathrm{Hom}(X, -) : \quad Y \mapsto \mathrm{Hom}(X, Y), \qquad (g : Y \to Z) \mapsto (f \mapsto g \circ f).\]

C’est la « trace » de \(X\) dans toute la catégorie : pour chaque \(Y\), l’ensemble des chemins de \(X\) vers \(Y\).

def foncteur(C, ensembles, actions):
    """ensembles[x] : frozenset ; actions[fleche] : dict ensemble source -> cible."""
    return {"ens": ensembles, "act": actions}

def h_X(C, X):
    """Representable covariant Hom(X, -) : ens(Y) = fleches X->Y,
    act[g: a->b] : Hom(X,a) -> Hom(X,b), f |-> g . f (post-composition)."""
    ens = {y: frozenset(hom_set(C, X, y)) for y in C["obj"]}
    act = {}
    for (a, b), fs in C["hom"].items():
        for g in fs:
            act[g] = {f: C["comp"][(g, f)] for f in hom_set(C, X, a)
                      if (g, f) in C["comp"]}
    return foncteur(C, ens, act)

# Le representable du point generique 'a' de Sierpinski :
ha = h_X(sierpinski, "a")
for y in sierpinski["obj"]:
    print(f"h_a({y}) = {sorted(ha['ens'][y])}")
# et un foncteur temoin : la permutation (1 2) le long de a -> b
F_swap = foncteur(sierpinski,
                  {"a": frozenset({1, 2}), "b": frozenset({1, 2})},
                  {("a", "b"): {1: 2, 2: 1}, ("a", "a"): {1: 1, 2: 2},
                   ("b", "b"): {1: 1, 2: 2}})
h_a(a) = [('a', 'a')]
h_a(b) = [('a', 'b')]

3. Transformations naturelles, énumérées

Une transformation naturelle \(\alpha : F \Rightarrow G\) est une famille de fonctions \(\alpha_Y : F(Y) \to G(Y)\), une par objet, compatible avec toutes les flèches : pour chaque \(g : Y \to Z\), le carré commute, \(G(g) \circ \alpha_Y = \alpha_Z \circ F(g)\).

Sur une catégorie finie avec de petits ensembles, on peut les énumérer toutes : produit cartésien de toutes les fonctions composantes, puis filtrage des familles qui satisfont chaque carré. Cette liste exhaustive est notre instrument de mesure — tout ce qui suit se lit dedans.

def transformations_naturelles(C, F, G):
    """Toutes les familles alpha_y : F(y) -> G(y) naturelles (enumeration exhaustive)."""
    obj = C["obj"]

    def fonctions(src, tgt):
        if not tgt:
            return [{}] if not src else []
        return [dict(zip(src, vals)) for vals in product(tgt, repeat=len(src))]

    composantes = [fonctions(F["ens"][y], G["ens"][y]) for y in obj]
    resultat = []
    for combo in product(*composantes):
        alpha = dict(zip(obj, combo))
        ok = True
        for (a, b), fs in C["hom"].items():
            for g in fs:
                Fa, Ga = F["act"].get(g, {}), G["act"].get(g, {})
                for x in F["ens"][a]:
                    if Ga.get(alpha[a].get(x)) != alpha[b].get(Fa.get(x)):
                        ok = False
                        break
                if not ok:
                    break
            if not ok:
                break
        if ok:
            resultat.append(alpha)
    return resultat

# Premiere mesure : sur Sierpinski, |Nat(h_X, F)| pour deux foncteurs temoins.
F_const3 = foncteur(sierpinski,
                    {"a": frozenset({0, 1, 2}), "b": frozenset({0, 1, 2})},
                    {("a", "b"): {0: 0, 1: 1, 2: 2}, ("a", "a"): {0: 0, 1: 1, 2: 2},
                     ("b", "b"): {0: 0, 1: 1, 2: 2}})
for X in ["a", "b"]:
    hX = h_X(sierpinski, X)
    for nom, F in [("swap", F_swap), ("const3", F_const3)]:
        nats = transformations_naturelles(sierpinski, hX, F)
        print(f"X={X} F={nom:8s} : |Nat(h_X,F)| = {len(nats)}  |  |F(X)| = {len(F['ens'][X])}")
X=a F=swap     : |Nat(h_X,F)| = 2  |  |F(X)| = 2
X=a F=const3   : |Nat(h_X,F)| = 3  |  |F(X)| = 3
X=b F=swap     : |Nat(h_X,F)| = 2  |  |F(X)| = 2
X=b F=const3   : |Nat(h_X,F)| = 3  |  |F(X)| = 3

Lecture chiffrée — cinq équations de Yoneda avant toute théorie. Dans les quatre cas du tableau, \(|\mathrm{Nat}(h_X, F)| = |F(X)|\) : \(2\) pour swap, \(3\) pour const3 — deux flèches de \(F(a)\) vers \(F(b)\) ou un foncteur constant à 3 éléments, le compte est le même, et il ne dépend ni de la forme des images de \(F\) ni de l’autre objet : tout ce que la numération voit, c’est la taille de \(F(X)\). Ce n’est pas une coïncidence — c’est le lemme de Yoneda, et le \(F\) est arbitraire. Ajoutons la cinquième équation du §4 (\(\mathbb{Z}/2\) : \(|\mathrm{Nat}(h_*, F)| = 2 = |F(*)|\)) : sur deux formes de catégories — le poset de Sierpinski (2 objets) et le monoïde \(\mathbb{Z}/2\) (1 objet, 2 flèches) — l’équation \(|\mathrm{Nat}(h_X, F)| = |F(X)|\) tombe 5 fois sur 5 par énumération exhaustive, jamais par échantillonnage.

4. Le lemme : l’évaluation est une bijection, calculée

Le lemme dit précisément quelle bijection : l’évaluation en l’identité

\[\alpha \;\mapsto\; \alpha_X(\mathrm{id}_X) \in F(X),\]

dont l’inverse explicite envoie \(x \in F(X)\) sur la famille \(\big(f : X \to Y \mapsto F(f)(x)\big)_Y\). On vérifie les deux sens sur la liste exhaustive : (a) l’évaluation est injective (deux transformations distinctes ont des images distinctes) et surjective (chaque \(x\) est atteint) ; (b) l’inverse explicite produit une famille qui est bien dans la liste énumérée, et le round-trip est l’identité.

def evaluation(C, X, alpha):
    """yoneda : Nat(h_X, F) -> F(X), alpha |-> alpha_X(id_X)."""
    return alpha[X][C["idn"][X]]

def yoneda_inverse(C, X, F, x):
    """x dans F(X) |-> famille naturelle alpha_y(f: X->y) = F(f)(x)."""
    return {y: {f: F["act"][f][x] for f in hom_set(C, X, y)} for y in C["obj"]}

# Verification complete sur Sierpinski (les 2 objets x les 2 foncteurs) :
for X in ["a", "b"]:
    hX = h_X(sierpinski, X)
    for nom, F in [("swap", F_swap), ("const3", F_const3)]:
        nats = transformations_naturelles(sierpinski, hX, F)
        imgs = [evaluation(sierpinski, X, al) for al in nats]
        bijectif = len(set(imgs)) == len(F["ens"][X]) == len(nats)
        rt = all(yoneda_inverse(sierpinski, X, F, evaluation(sierpinski, X, al)) == al
                 for al in nats)
        inv_nat = all(yoneda_inverse(sierpinski, X, F, x) in nats
                      for x in F["ens"][X])
        print(f"X={X} F={nom:8s} : evaluation bijective={bijectif}, "
              f"round-trip={rt}, inverse naturel={inv_nat}")

# Cas non-poset : le groupe Z/2 comme categorie a un objet.
# h_* = action reguliere ; F = l'ensemble {p,q} muni de l'involution t = (p q).
F_z2 = foncteur(z2, {"*": frozenset({"p", "q"})},
                  {"e": {"p": "p", "q": "q"}, "t": {"p": "q", "q": "p"}})
nats_z2 = transformations_naturelles(z2, h_X(z2, "*"), F_z2)
rt_z2 = all(yoneda_inverse(z2, "*", F_z2, evaluation(z2, "*", al)) == al
            for al in nats_z2)
print(f"Z/2 : |Nat(h_*,F)| = {len(nats_z2)} = |F(*)|, round-trip = {rt_z2}")
X=a F=swap     : evaluation bijective=True, round-trip=True, inverse naturel=True
X=a F=const3   : evaluation bijective=True, round-trip=True, inverse naturel=True
X=b F=swap     : evaluation bijective=True, round-trip=True, inverse naturel=True
X=b F=const3   : evaluation bijective=True, round-trip=True, inverse naturel=True
Z/2 : |Nat(h_*,F)| = 2 = |F(*)|, round-trip = True

Lecture chiffrée — la bijection vérifiée propriété par propriété : 13 booléens, tous True, plus l’égalité de cardinaux du monoïde. Chaque ligne du §4 teste trois propriétés indépendantes — évaluation bijective, round-trip identité, inverse naturel — sur les 4 configurations Sierpinski (2 foncteurs × 2 objets) : 12 booléens ; le monoïde \(\mathbb{Z}/2\) ajoute son booléen de round-trip, et son cardinal est constaté par l’égalité affichée \(|\mathrm{Nat}(h_*,F)| = |F(*)|\) — 13 vérifications booléennes, zéro False, plus cette égalité numérique qui scelle la bijection sur le cas non-poset. La bijection de Yoneda n’est pas une abstraction : ici, sur chaque exemple fini, on peut la toucher — énumérer les transformations, évaluer en l’identité, constater qu’on obtient exactement \(F(X)\), et refaire le chemin inverse. Ce qui distingue ces listes d’un test unitaire ordinaire : elles sont exhaustives (2 ou 3 transformations, pas un échantillon), donc l’injectivité et la surjectivité sont constatées sur la totalité, et la naturalité de l’inverse est re-dérivée flèche par flèche. Le cas \(\mathbb{Z}/2\) montre que tout marche aussi quand la catégorie n’est pas un poset : un seul objet, deux flèches, et le lemme voit l’action régulière à travers n’importe quelle autre action. La réversibilité calculée est le contenu opérationnel du lemme : partant de n’importe quel \(x \in F(X)\), la famille \((F(f)(x))_Y\) reconstruit l’unique transformation qui s’évalue en \(x\).

5. Plein et fidèle : \(\mathrm{Nat}(h_X, h_Y) \cong \mathrm{Hom}(Y, X)\)

En prenant \(F = h_Y\) dans le lemme : \(\mathrm{Nat}(h_X, h_Y) \cong h_Y(X) = \mathrm{Hom}(Y, X)\). Attention au sens des flèches : le \(X\) du représentable devient la source du Hom. Le plongement de Yoneda \(X \mapsto h_X\) est alors plein et fidèle : il ne perd ni n’invente de flèches — c’est yoneda_full et yoneda_faithful dans le module Lean.

On mesure la chose en entier : le cercle à 4 points (modèle de McCord du notebook 03), ses 16 paires d’objets, et le tableau \(|\mathrm{Nat}(h_X, h_Y)|\) contre \(|\mathrm{Hom}(Y, X)|\).

cercle4 = cat_poset({"a1": {"a1", "a2", "a4"}, "a2": {"a2"},
                     "a3": {"a3", "a2", "a4"}, "a4": {"a4"}})
pts = ["a1", "a2", "a3", "a4"]
hs = {X: h_X(cercle4, X) for X in pts}

print("Matrice |Nat(h_X, h_Y)|  (ligne = X, colonne = Y) vs |Hom(Y, X)| :")
accord = True
for X in pts:
    ligne = []
    for Y in pts:
        n = len(transformations_naturelles(cercle4, hs[X], hs[Y]))
        m = len(hom_set(cercle4, Y, X))
        accord = accord and (n == m)
        ligne.append(n)
    print(f"  X={X} : {ligne}")
print("Accord |Nat(h_X,h_Y)| == |Hom(Y,X)| sur les 16 paires :", accord)
print("(la matrice est la transposee de la matrice d'ordre : Yoneda contravariant sur la 1re coordonnee)")
Matrice |Nat(h_X, h_Y)|  (ligne = X, colonne = Y) vs |Hom(Y, X)| :
  X=a1 : [1, 0, 0, 0]
  X=a2 : [1, 1, 1, 0]
  X=a3 : [0, 0, 1, 0]
  X=a4 : [1, 0, 1, 1]
Accord |Nat(h_X,h_Y)| == |Hom(Y,X)| sur les 16 paires : True
(la matrice est la transposee de la matrice d'ordre : Yoneda contravariant sur la 1re coordonnee)

Lecture chiffrée — la matrice \(4 \times 4\) est la relation d’ordre elle-même, transposée. Les 16 paires se partagent en 8 non nulles et 8 nulles, et aucune entrée ne vaut plus que 1 : dans un poset chaque \(\mathrm{Hom}\) a au plus une flèche, et Yoneda restitue cette « finesse » — \(|\mathrm{Nat}(h_X, h_Y)| \in \{0, 1\}\) partout. Les 8 non nulles se décomposent en 4 réflexives (la diagonale) et 4 couvertures : les deux minimaux \(a_1, a_3\) sous les deux maximaux \(a_2, a_4\) — le graphe \(K_{2,2}\) du cercle à 4 points. Les sommes de lignes \([1, 3, 1, 3]\) sont les tailles des downsets : un maximal domine 3 objets (lui-même et les deux minimaux), un minimal n’est au-dessus que de lui-même. L’accord avec \(|\mathrm{Hom}(Y, X)|\) sur les 16 paires n’est pas un échantillon : c’est le dénombrement complet du plongement plein et fidèle sur cette catégorie.

6. Le pont Čech : \(h_x = U_x\)

Un poset \(P\) est une catégorie, et son représentable en \(x\) vaut \(h_x(y) = \mathrm{Hom}(x, y) = \{\bullet\}\) si \(x \leq y\), vide sinon. L’ensemble des \(y\) où \(h_x(y)\) est non vide est donc exactement l’ouvert minimal \(U_x = \{y \geq x\}\) du notebook 03 — la base du recouvrement de Čech y est l’image du plongement de Yoneda. La topologie d’Alexandrov se relit : les ouverts minimaux sont les représentables.

for x in ["a1", "a3"]:
    hx = h_X(cercle4, x)
    support = {y for y in cercle4["obj"] if hx["ens"][y]}
    u_x = {y for y in cercle4["obj"] if hom_set(cercle4, x, y)}
    print(f"x={x} : support de h_x = {sorted(support)} == U_x : {support == u_x}")
x=a1 : support de h_x = ['a1', 'a2', 'a4'] == U_x : True
x=a3 : support de h_x = ['a2', 'a3', 'a4'] == U_x : True

Lecture chiffrée — deux ouverts minimaux, leur recouvrement et leur intersection. Les supports vérifiés : \(\mathrm{supp}(h_{a_1}) = \{a_1, a_2, a_4\}\) et \(\mathrm{supp}(h_{a_3}) = \{a_2, a_3, a_4\}\) — 3 objets chacun, soit les upsets des deux minimaux. Leur union fait les 4 objets du poset (chaque minimal apporte son point propre, les maximaux sont communs), leur intersection est \(\{a_2, a_4\}\) — exactement l’ensemble des maximaux. La géométrie du \(K_{2,2}\) se lit dans les ouverts : chaque minimal voit tous les maximaux, aucun minimal ne voit l’autre minimal. C’est le pont Čech du §6 rendu quantitatif : la base de recouvrement hérite de la structure d’ordre, et les intersections de la base encodent qui domine quoi.

Exercices

Exercice 1 — Le foncteur constant : \(\mathrm{Nat}(h_X, \mathrm{cst}_E) \cong E\)

Écrivez foncteur_constant(C, E) (chaque objet reçoit l’ensemble \(E\), chaque flèche l’identité de \(E\)), puis vérifiez sur le cercle à 4 points que \(|\mathrm{Nat}(h_x, \mathrm{cst}_E)| = |E|\) pour chaque \(x\) — le lemme ne dépend pas du foncteur.

# Exercice 1 : foncteur constant et lemme de Yoneda.
def foncteur_constant(C, E):
    """Foncteur constant de valeur E : chaque fleche -> identite de E."""
    # Etape 1 : ensembles = E pour chaque objet (un frozenset(E))
    # Etape 2 : actions = {fleche : {e: e pour e dans E}} pour TOUTES les fleches
    # (parcourir C['hom'].values(), chaque tuple de fleches)
    return None  # TODO etudiant

Exercice 2 — Chaque flèche EST une transformation : fidélité calculée

Une flèche \(f : X \to Y\) induit une transformation naturelle \(h^f : h_Y \Rightarrow h_X\) par précomposition : en chaque \(Z\), la fonction \(\mathrm{Hom}(Y, Z) \to \mathrm{Hom}(X, Z)\), \(g \mapsto g \circ f\). Écrivez transformation_de_fleche(C, f), vérifiez que chaque \(h^f\) apparaît dans la liste énumérée des \(\mathrm{Nat}(h_Y, h_X)\), et que deux flèches distinctes donnent des transformations distinctes — la fidélité, vue sur la liste.

# Exercice 2 : fleche -> transformation naturelle par precomposition.
def transformation_de_fleche(C, f):
    """f : X -> Y (couple (X, Y)). Renvoie la famille
    alpha_Z : Hom(Y,Z) -> Hom(X,Z), g |-> g . f — naturelle."""
    # Etape 1 : X, Y = f ; pour chaque objet Z de C
    # Etape 2 : alpha_Z = {g: C['comp'][(g, f)] pour g dans hom_set(C, Y, Z)}
    return None  # TODO etudiant

Exercice 3 — Un monoïde plus grand : \(\mathbb{Z}/3\)

Construisez la catégorie à un objet du groupe \(\mathbb{Z}/3\) (flèches \(\{0,1,2\}\), composition = l’addition mod 3), le foncteur \(F\) = l’ensemble \(\{0,1,2\}\) muni de la translation \(x \mapsto x + k\), puis vérifiez \(|\mathrm{Nat}(h_*, F)| = 3\) et le round-trip de l’inverse de Yoneda. Le représentable \(h_*\) est l’action régulière gauche — le lemme affirme (et vous mesurerez) qu’elle n’est Naturelle-équivalente qu’aux choix d’un point de \(F\).

# Exercice 3 : le monoide Z/3 et le lemme.
# Etape 1 : z3 = cat_monoide([0, 1, 2], lambda u, v: ..., 0)
# Etape 2 : F3 = foncteur(z3, {'*': frozenset({0, 1, 2})},
#           {k: {x: ... pour x dans {0,1,2}} pour k dans [0,1,2]})
# Etape 3 : nats = transformations_naturelles(z3, h_X(z3, '*'), F3)
#           -> verifier len(nats) == 3 et le round-trip yoneda_inverse/evaluation
z3 = None  # TODO etudiant

Conclusion

Ce qu’on a distillé :

  • une catégorie finie tient en trois dictionnaires (objets, hom-sets, composition) ; posets et monoïdes en sont les exemples rois ;
  • les transformations naturelles entre foncteurs vers les ensembles finis s’énumèrent exhaustivement — le filtrage par les carrés commutatifs est la seule force du calcul ;
  • le lemme de Yoneda se vérifie alors comme une mesure : \(|\mathrm{Nat}(h_X, F)| = |F(X)|\), l’évaluation \(\alpha \mapsto \alpha_X(\mathrm{id}_X)\) est bijective, son inverse explicite round-trip — sur des posets, sur le monoïde \(\mathbb{Z}/2\) ;
  • plein et fidèle : \(|\mathrm{Nat}(h_X, h_Y)| = |\mathrm{Hom}(Y, X)|\), matrice mesurée sur le cercle à 4 points — le plongement \(X \mapsto h_X\) ne perd rien ;
  • le pont Čech : pour un poset, le support du représentable \(h_x\) est l’ouvert minimal \(U_x\) — le recouvrement du notebook 03 est l’image du plongement de Yoneda.

Le même énoncé, démontré en Lean dans grothendieck_lean/YonedaLemma.lean, calculé ici en Python pur. C’est le grain 8 de la voie décorrelée Serre–Grothendieck de l’EPIC #16334 — après le grain 7 (Čech calculée), le geste catégorique devient machine.

Ressources

  • Saunders Mac Lane, Categories for the Working Mathematician, ch. III (Yoneda) — 1971, le traité qui a fixé le langage.
  • Nobuo Yoneda, l’observation originale (1954-1958, colloques de Tokyo) — devenue « le lemme le plus important de la théorie des catégories ».
  • Lake grothendieck_lean — YonedaLemma.lean : yoneda_equiv, yoneda_full, yoneda_faithful, démontrés.
  • Notebook précédent de la voie : « 03 — cohomologie de Čech sur espaces finis » (même série, EPIC #16334) — les ouverts minimaux y sont les supports des \(h_x\) d’ici.
Retour au sommet