Skip to content

Reorg(lean,#19522): Lean-15c annexes groupees par theme, hierarchie 3 niveaux #19573

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 7, 2026
Merged

Reorg(lean,#19522): Lean-15c annexes groupees par theme, hierarchie 3 niveaux #19573

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
168 changes: 91 additions & 77 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2659,6 +2659,67 @@
"example : True := trivial"
]
},
{
"cell_type": "markdown",
"id": "6f06ac85",
"metadata": {
"papermill": {
"duration": 0.010796,
"end_time": "2026-10-04T09:02:26.972716+00:00",
"exception": false,
"start_time": "2026-10-04T09:02:26.961920+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"## 12. Conclusion\n",
"\n",
"Le lake `grothendieck_lean` couvre tout le spectre — de Yoneda à la cohomologie de Čech, en passant par\n",
"la forme flèche des recouvrements et le site de Zariski. Ce notebook rend **visibles par leurs énoncés**\n",
"une large part de ces modules : chaque `#check` est un lemme qui compile dans Mathlib 4.\n",
"\n",
"**Ce que l'on a appris en chemin.** Que le formalisme catégorique n'est pas du verbalisme : chaque\n",
"théorème du §2 transporte des données calculables (univers, adjonctions, extensions de Kan), et la\n",
"machinerie des sites (§4-5) est ce qui rend « recouvrir » une *opération* plutôt qu'une métaphore.\n",
"Que les faisceaux (§6) sont la réponse à une question précise — quand les sections locales se\n",
"recollent-elles ? — et que la cohomologie (§7) mesure quand elles ne se recollent pas : H⁰ est\n",
"l'espace des sections globales, le H¹ est l'obstruction. Que la géométrie (§8) est atteinte par\n",
"une chaîne d'identifications, chacune prouvée : Zariski *est* une topologie de Grothendieck,\n",
"les fibres *sont* des colimites. Et que la calibration (§9) n'est pas l'annexe du lake : c'est\n",
"ce qui garantit que ses définitions ne sont pas vides.\n",
"\n",
"**Ce que le `#print axioms` garantit.** Les théorèmes sondés ne dépendent que des trois\n",
"axiomes standards (`propext`, `Classical.choice`, `Quot.sound`) — ceux de la logique sous-jacente\n",
"de Lean, aucun autre. Aucun `sorry` : rien n'est promis sans preuve. C'est la différence entre un\n",
"lake qui *raconte* Grothendieck et un lake qui le *prouve*.\n",
"\n",
"La mesure fraîche de visibilité liée à [#11703](https://github.com/jsboige/CoursIA/issues/11703)\n",
"laisse encore des modules invisibles. Ce notebook démontre ainsi que la suite est un travail\n",
"d'enrichissement, plus de déblocage."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Annexes -- approfondissements optionnels\n",
"\n",
"Six annexes issues du chantier de visibilite des modules noirs\n",
"du lake (#11703). Regroupees par theme mathematique plutot\n",
"qu'empilees en queue : la thematique des faisceaux (A) avant\n",
"celle de la cohomologie et des sites (B). Chaque annexe preserve\n",
"son contenu de depart (definitions, cellules code, lectures) ;\n",
"seule la structure narrative change.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Annexe A -- Faisceaux en profondeur\n"
]
},
{
"cell_type": "markdown",
"id": "eb84c944",
Expand All @@ -2673,7 +2734,7 @@
"tags": []
},
"source": [
"## Annexe — SheafCondition : le coeur egaliseur rendu visible (#11703)\n",
"#### A.1 -- Le coeur egaliseur rendu visible (SheafCondition)\n",
"\n",
"Le scan de visibilite du lake (`scan_lake_notebook_visibility.py`) comptait\n",
"`SheafCondition.lean` parmi les modules invisibles : ses trois enonces n'etaient\n",
Expand Down Expand Up @@ -2902,9 +2963,7 @@
"tags": []
},
"source": [
"### Lecture de la sortie\n",
"\n",
"Les `#check` affichent les signatures. Les deux premiers ponts sont des\n",
"**Lecture de la sortie** -- Les `#check` affichent les signatures. Les deux premiers ponts sont des\n",
"équivalences vers `Nonempty (IsLimit ...)` : être un faisceau, ce n'est pas\n",
"seulement que le fork de restriction commute, c'est qu'il soit un\n",
"**égaliseur** — une limite. Le troisième pont remplace « pour tous les cribles\n",
Expand All @@ -2917,7 +2976,7 @@
"`sorryAx`. Le module `SheafCondition.lean` est désormais visible depuis ce\n",
"compagnon. Après l'enrichissement de ces deux annexes, la mesure fraîche laisse\n",
"encore des modules invisibles : le lake a gagné\n",
"des modules depuis, et l'annexe finale en retire plusieurs (dont `Spaces.lean`)."
"des modules depuis, et l'annexe finale en retire plusieurs (dont `Spaces.lean`).\n"
]
},
{
Expand All @@ -2934,7 +2993,7 @@
"tags": []
},
"source": [
"## Annexe — Du crible fermé à la faisceautisation Plus\n",
"#### A.2 -- Du crible ferme a la faisceautisation Plus\n",
"\n",
"Des modules voisins rendent explicite une même chaîne de construction. Dans\n",
"`LawvereTierney.lean`, un opérateur de Lawvere–Tierney ferme les cribles de\n",
Expand All @@ -2950,7 +3009,7 @@
"La cellule suivante interroge les modules à travers l'import racine déjà\n",
"chargé. Les paramètres implicites affichés par `#check @...` rendent visibles\n",
"les hypothèses catégoriques ; les `#print axioms` contrôlent l'intégrité\n",
"d'un théorème pivot par module."
"d'un théorème pivot par module.\n"
]
},
{
Expand Down Expand Up @@ -3284,9 +3343,7 @@
"tags": []
},
"source": [
"### Lecture de la sortie\n",
"\n",
"Le premier groupe expose l'opérateur de clôture sur les cribles. La signature\n",
"**Lecture de la sortie** -- Le premier groupe expose l'opérateur de clôture sur les cribles. La signature\n",
"de `j_monotone` dit que l'inclusion `S ≤ T` est préservée par la clôture, tandis\n",
"que `closure_isClosed` matérialise l'idempotence : fermer un crible produit\n",
"déjà un point fixe.\n",
Expand All @@ -3306,7 +3363,7 @@
"Les trois sorties `#print axioms` ne mentionnent que les axiomes standards\n",
"`propext`, `Classical.choice` et `Quot.sound`. En particulier, aucune ne contient\n",
"`sorryAx` : les trois maillons observés sont bien des déclarations compilées,\n",
"pas des énoncés admis dans le notebook."
"pas des énoncés admis dans le notebook.\n"
]
},
{
Expand All @@ -3323,7 +3380,7 @@
"tags": []
},
"source": [
"## Annexe — Les tiges (stalks) : du germe au recollement (#11703)\n",
"#### A.3 -- Les tiges (stalks) : du germe au recollement\n",
"\n",
"Des modules voisins déclarent la théorie ponctuelle du lake — les **tiges**\n",
"(`stalk`) et leurs germes — et n'étaient cités nulle part dans ce compagnon :\n",
Expand Down Expand Up @@ -4056,9 +4113,7 @@
"tags": []
},
"source": [
"### Lecture de la sortie\n",
"\n",
"Le premier groupe expose la paire intérieure / extérieure sur la tige du\n",
"**Lecture de la sortie** -- Le premier groupe expose la paire intérieure / extérieure sur la tige du\n",
"représentable. `unique_stalk_yoneda` rend un `Unique (stalk (yoneda.obj U) x)`\n",
"sous l'hypothèse `x ∈ U` : la tige n'a qu'un seul élément, le germe de\n",
"l'identité de `U`. `isEmpty_stalk_yoneda` porte l'hypothèse opposée `x ∉ U` et\n",
Expand Down Expand Up @@ -4114,11 +4169,11 @@
"tags": []
},
"source": [
"## Annexe — Des ouverts au préfaisceau gratte-ciel (#11703)\n",
"#### A.4 -- Des ouverts au prefaisceau gratte-ciel\n",
"\n",
"Cette annexe relie quatre modules qui forment une même chaîne topologique. `SpacesMathlib` identifie le site des ouverts construit dans le lake à celui de Mathlib. `SpacesSubcanonical` montre ensuite que les représentables y sont des faisceaux. `StalkCharacterization` reformule la condition de faisceau par séparation et recollement des germes. Enfin, `Skyscraper` applique ce vocabulaire à un préfaisceau concentré autour d’un point.\n",
"\n",
"Les signatures ci-dessous sont vérifiées par Lean dans le lake réel. Elles rendent visibles les propriétés structurantes plutôt que les détails de leurs preuves."
"Les signatures ci-dessous sont vérifiées par Lean dans le lake réel. Elles rendent visibles les propriétés structurantes plutôt que les détails de leurs preuves.\n"
]
},
{
Expand Down Expand Up @@ -4583,11 +4638,9 @@
"tags": []
},
"source": [
"### Lecture du résultat\n",
"\n",
"Le premier groupe de signatures établit un pont sans couche de traduction : la topologie des ouverts du lake est celle de Mathlib, puis sa sous-canonicité autorise Yoneda à produire des faisceaux. La caractérisation par les germes sépare ensuite les deux obligations d’un faisceau : l’unicité locale (`GermSeparated`) et l’existence d’un recollement (`GermGluing`).\n",
"**Lecture de la sortie** -- Le premier groupe de signatures établit un pont sans couche de traduction : la topologie des ouverts du lake est celle de Mathlib, puis sa sous-canonicité autorise Yoneda à produire des faisceaux. La caractérisation par les germes sépare ensuite les deux obligations d’un faisceau : l’unicité locale (`GermSeparated`) et l’existence d’un recollement (`GermGluing`).\n",
"\n",
"Le gratte-ciel rend cette abstraction géométrique. Sa tige est isomorphe à la valeur choisie dans l’adhérence du point et terminale hors de cette adhérence. Sous l’hypothèse que la valeur n’est pas terminale, `support_skyscraper` identifie donc exactement le support à cette adhérence. Les commandes `#print axioms` permettent enfin de contrôler les dépendances logiques des trois résultats pivots."
"Le gratte-ciel rend cette abstraction géométrique. Sa tige est isomorphe à la valeur choisie dans l’adhérence du point et terminale hors de cette adhérence. Sous l’hypothèse que la valeur n’est pas terminale, `support_skyscraper` identifie donc exactement le support à cette adhérence. Les commandes `#print axioms` permettent enfin de contrôler les dépendances logiques des trois résultats pivots.\n"
]
},
{
Expand All @@ -4604,13 +4657,11 @@
"tags": []
},
"source": [
"### Exercice — retrouver la concentration au point fermé\n",
"\n",
"**Objectif.** Identifier le corollaire qui réduit le support du préfaisceau gratte-ciel au singleton du point lorsque celui-ci est fermé.\n",
"**Exercice** -- **Objectif.** Identifier le corollaire qui réduit le support du préfaisceau gratte-ciel au singleton du point lorsque celui-ci est fermé.\n",
"\n",
"1. Repérez la déclaration dont le nom prolonge `support_skyscraper`.\n",
"2. Comparez son hypothèse de fermeture avec celle du théorème général.\n",
"3. Décommentez le `#check`, puis ajoutez sous le message exécutable une micro-preuve qui applique ce corollaire dans un contexte de votre choix."
"3. Décommentez le `#check`, puis ajoutez sous le message exécutable une micro-preuve qui applique ce corollaire dans un contexte de votre choix.\n"
]
},
{
Expand Down Expand Up @@ -4711,6 +4762,13 @@
"#eval \"Exercice a completer : instancier le corollaire pour un point ferme\""
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Annexe B -- Cohomologie et sites\n"
]
},
{
"cell_type": "markdown",
"id": "flasque-godement-annexe",
Expand All @@ -4725,7 +4783,7 @@
"tags": []
},
"source": [
"## Annexe — Faisceaux flasques et résolution de Godement (#11703)\n",
"#### B.1 -- Faisceaux flasques et resolution de Godement\n",
"\n",
"Huit modules du lake déclarent la théorie **flasque** du corpus — les cinq\n",
"modules `Flasque*` (définition, exactitude, quotients, rétracts, stabilité) et\n",
Expand All @@ -4746,7 +4804,7 @@
"faisceau se plonge dans un faisceau flasque construit section par section\n",
"(`godementSection` : germes à gauche), le plongement est fonctoriel et\n",
"additif, et le foncteur préserve les monomorphismes — d'où la résolution\n",
"flasque universelle qui définit la cohomologie des faisceaux."
"flasque universelle qui définit la cohomologie des faisceaux.\n"
]
},
{
Expand Down Expand Up @@ -5610,9 +5668,7 @@
"tags": []
},
"source": [
"### Lecture de la sortie\n",
"\n",
"Le premier groupe fixe la définition : `IsFlasqueSieves` est une **classe de\n",
"**Lecture de la sortie** -- Le premier groupe fixe la définition : `IsFlasqueSieves` est une **classe de\n",
"propositions** sur un préfaisceau de cribles — toute section sur un crible\n",
"s'amalgame sur le crible maximal — et `isFlasqueSieves_iff` en donne la\n",
"caractérisation. Les deux « ponts » relient cette définition générale aux\n",
Expand Down Expand Up @@ -5646,7 +5702,7 @@
"`godementMapHom_id`/`comp`, naturel via `toGodement_naturality`), et\n",
"`godementFunctor_preservesMonomorphisms` garantit que la résolution s'itère\n",
"sans perdre l'injectivité. La cohomologie des faisceaux — section 7 du\n",
"compagnon — a ici sa résolution canonique."
"compagnon — a ici sa résolution canonique.\n"
]
},
{
Expand All @@ -5663,7 +5719,7 @@
"tags": []
},
"source": [
"## Annexe — Sites, topologies et comparaisons (#11703)\n",
"#### B.2 -- Sites, topologies et comparaisons\n",
"\n",
"Les huit derniers modules noirs du scan de visibilité forment un bloc\n",
"cohérent : la **hiérarchie des topologies** sur les schémas (Zariski,\n",
Expand All @@ -5686,7 +5742,7 @@
"referme le chapitre topos. Et entre deux sites, l'image directe continue\n",
"devient un foncteur qui respecte composition et identités, adjoint au\n",
"changement de base : c'est la machinerie qui permet de comparer les\n",
"faisceaux d'un site à l'autre."
"faisceaux d'un site à l'autre.\n"
]
},
{
Expand Down Expand Up @@ -6625,9 +6681,7 @@
"tags": []
},
"source": [
"### Lecture de la sortie\n",
"\n",
"Le groupe **Classifier** décrit Ω vu comme classifieur : `truth_picks_top`\n",
"**Lecture de la sortie** -- Le groupe **Classifier** décrit Ω vu comme classifieur : `truth_picks_top`\n",
"dit que la flèche « vrai » choisit le crible maximal, et les trois\n",
"`chi_app_*` gouvernent la fonction caractéristique d'un monomorphisme —\n",
"appartenance, descendance, et le cas où la valeur est le maximum : c'est\n",
Expand Down Expand Up @@ -6660,47 +6714,7 @@
"composition `comp`), compatible avec l'oubli vers les préfaisceaux\n",
"(`comp_sheafToPresheaf`), et `adjunction_sheafPushforwardContinuous` en\n",
"est l'adjonction — l'outil qui identifie les faisceaux d'un site à ceux\n",
"d'un site raffiné, la pierre angulaire de toute comparaison de sites."
]
},
{
"cell_type": "markdown",
"id": "6f06ac85",
"metadata": {
"papermill": {
"duration": 0.010796,
"end_time": "2026-10-04T09:02:26.972716+00:00",
"exception": false,
"start_time": "2026-10-04T09:02:26.961920+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"## 12. Conclusion\n",
"\n",
"Le lake `grothendieck_lean` couvre tout le spectre — de Yoneda à la cohomologie de Čech, en passant par\n",
"la forme flèche des recouvrements et le site de Zariski. Ce notebook rend **visibles par leurs énoncés**\n",
"une large part de ces modules : chaque `#check` est un lemme qui compile dans Mathlib 4.\n",
"\n",
"**Ce que l'on a appris en chemin.** Que le formalisme catégorique n'est pas du verbalisme : chaque\n",
"théorème du §2 transporte des données calculables (univers, adjonctions, extensions de Kan), et la\n",
"machinerie des sites (§4-5) est ce qui rend « recouvrir » une *opération* plutôt qu'une métaphore.\n",
"Que les faisceaux (§6) sont la réponse à une question précise — quand les sections locales se\n",
"recollent-elles ? — et que la cohomologie (§7) mesure quand elles ne se recollent pas : H⁰ est\n",
"l'espace des sections globales, le H¹ est l'obstruction. Que la géométrie (§8) est atteinte par\n",
"une chaîne d'identifications, chacune prouvée : Zariski *est* une topologie de Grothendieck,\n",
"les fibres *sont* des colimites. Et que la calibration (§9) n'est pas l'annexe du lake : c'est\n",
"ce qui garantit que ses définitions ne sont pas vides.\n",
"\n",
"**Ce que le `#print axioms` garantit.** Les théorèmes sondés ne dépendent que des trois\n",
"axiomes standards (`propext`, `Classical.choice`, `Quot.sound`) — ceux de la logique sous-jacente\n",
"de Lean, aucun autre. Aucun `sorry` : rien n'est promis sans preuve. C'est la différence entre un\n",
"lake qui *raconte* Grothendieck et un lake qui le *prouve*.\n",
"\n",
"La mesure fraîche de visibilité liée à [#11703](https://github.com/jsboige/CoursIA/issues/11703)\n",
"laisse encore des modules invisibles. Ce notebook démontre ainsi que la suite est un travail\n",
"d'enrichissement, plus de déblocage."
"d'un site raffiné, la pierre angulaire de toute comparaison de sites.\n"
]
}
],
Expand Down
Loading