Skip to content

feat(lean-grothendieck): formaliser la propriété et la topologie fppf #14782

Closed
#15382
Closed
feat(lean-grothendieck): formaliser la propriété et la topologie fppf#14782
#15382
Labels
enhancementNew feature or request

Description

@jsboige
jsboige
opened on Sep 5, 2026

Objet

Étendre grothendieck_lean avec la propriété, la précouverture et la topologie fppf, en s’appuyant sur la structure déjà présente pour les précouvertures, la topologie étale et les faisceaux.

Sous-grain issu de #14771. Dépend de la migration 4.33 de grothendieck_lean sous #14773.

Ancrage amont

  • dépôt : anthropics/fermats-last-theorem
  • commit : aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
  • source exacte : Definitions/Def_AlgebraicGeometry_FppfSiteCohomology.lean
  • Mathlib : db584cd6d46c92f209a44c0f1c829460d327499d
  • licence Apache-2.0 : préserver NOTICE et l’attribution Anthropic pour toute adaptation

Le source-port exact compile sous Lean 4.33.0 lorsque l’option FLT backward.isDefEq.respectTransparency.types := false est conservée. Sans elle, l’inférence échoue dès fppfProperty.IsStableUnderBaseChange et les instances dérivées : l’option doit être documentée et son périmètre minimisé, pas copiée silencieusement à tous les lakes.

Tranche

  1. définir fppfProperty := Flat ⊓ LocallyOfFinitePresentation ;
  2. raccorder fppfPrecoverage à Scheme.precoverage fppfProperty ;
  3. définir fppfPretopology et les identités avec fppfTopology ;
  4. prouver les inclusions topologiques étale ≤ fppf et Zariski ≤ fppf ;
  5. fournir siblings FR/EN conformes.

Le petit site fppf et sa cohomologie sont explicitement hors de cette première tranche et feront l’objet d’un grain aval après stabilisation de ce socle.

Acceptance

  • grothendieck_lean migré vers la cible 4.33 de feat(lean): migrer les 27 lakes first-party vers Lean/Mathlib 4.33 #14773 ;
  • source adaptée, sans import monolithique de FLT ;
  • rôle de l’option de transparence testé et documenté ;
  • lake build complet SUCCESS ;
  • aucun nouveau sorry, sorryAx ou native_decide ;
  • proof-integrity ciblée et parité FR/EN vertes ;
  • attribution Apache-2.0/NOTICE préservée.

Voir #14771 et #14773.

Activity

  1. jsboige
    added
    enhancementNew feature or request
    on Sep 5, 2026

  2. jsboige commented on Sep 7, 2026

    @jsboige
    jsboige
    on Sep 7, 2026
    OwnerAuthor

    Grain: DEEP/lean — lane myia-po-2025:CoursIA-2 — prev: MED/research-code #15000

    [CLAIMED] lane myia-po-2025:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/lakefile.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/NOTICE

    Grounding 2026-09-07 : #14782 OPEN et admissible (39 h), body complet lu, 0 commentaire, 0 PR all-state sur #14782 ou fppf, 0 PR ouverte touchant grothendieck_lean. La dépendance #14773 est livrée sur origin/main par #14964 (commit 4021837). Scope : socle propriété/précouverture/prétopologie/topologie fppf et inclusions étale/Zariski, siblings FR/EN, option de transparence minimisée et attribution Apache-2.0 ; petit site/cohomologie hors scope.

  3. jsboige commented on Sep 9, 2026

    @jsboige
    jsboige
    on Sep 9, 2026
    OwnerAuthor

    Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/docs #2

    [CLAIMED] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/lakefile.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/NOTICE

    Reprise après péremption active du claim CoursIA-2 (52 h, aucun artefact trouvé). Préflight frais : issue et tous commentaires lus ; 0 PR all-state trouvée par recherche #14782 ; 0 PR OPEN touchant grothendieck_lean/Fppf ; 0 branche/ref locale ou distante nommée 14782/fppf. Dépendance Lean 4.33 vérifiée dans le body comme livrée ; adaptation bornée au socle fppf, siblings FR/EN, option de transparence minimisée et attribution Apache-2.0.

  4. jsboige commented on Sep 9, 2026

    @jsboige
    jsboige
    on Sep 9, 2026
    OwnerAuthor

    Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/docs #2

    [CLAIMED-AMEND] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/NOTICE.md

  5. jsboige commented on Sep 9, 2026

    @jsboige
    jsboige
    on Sep 9, 2026
    OwnerAuthor

    Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/docs #2

    [CLAIMED-AMEND] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Fppf_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/NOTICE.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/LICENSE-Apache-2.0.txt

  6. myia-ai-01
    closed this as completedin #15382on Sep 10, 2026

  7. myia-ai-01 commented on Sep 10, 2026

    @myia-ai-01
    myia-ai-01
    on Sep 10, 2026
    Collaborator

    [RELEASED] lane myia-po-2025:CoursIA — PR #15382 mergée au head vérifié ; verrou libéré après intégration sur main.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions