AGLib: extract nilpotent Nakayama freeness for invertible modules

[AxelDlv00]

Contributor : contributor 🧑‍💻 📣

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra

🔍 Context

Bootstrap issue #1 is the only open work item. The roadmap's reusable commutative-algebra and local-to-global layers need a general nilpotent-thickening lemma, but the pinned Mathlib currently exposes only the finite-generation/Jacobson versions of Nakayama's lemma and Module.Invertible.bijective_of_surjective; it has no equivalent of the no-finiteness API below.

At reference commit 9223d85c786394721963a9d642b08d066b72a594, both flagship Algebraic-Jacobian routes contain proof-placeholder-free versions of this algebra:

• MainProjects/AlgebraicJacobian/MilneKollar/AlgebraicJacobian/Picard/NilpotentThickeningFree.lean:72-175
• MainProjects/AlgebraicJacobian/PicardAlbanese/AlgebraicJacobian/Tangent/NilpotentThickeningFree.lean:74-185

The files prove, for a commutative ring R and an arbitrary module M, that an invertible module which is generated by one element modulo a nilpotent ideal is free. The core induction Submodule.top_le_span_sup_pow_smul_top needs no finite-generation or Jacobson hypothesis. The two copies differ only in how an already-existing cyclic-invertible lemma is supplied; that difference is useful extraction evidence, not a reason to import either route.

The result is consumed directly by the chart-triviality files
.../MilneKollar/.../Picard/DualNumberChartTriviality.lean:130-136 and
.../PicardAlbanese/.../Tangent/DualNumberChartTriviality.lean:132-138, which are themselves rooted by both flagship umbrellas. No open issue or pull request covers this API. It is independent of issue #8: it is pure module theory and does not depend on smooth morphisms.

🎯 Goal

Add a focused, Mathlib-only AGLib module for the general nilpotent-invertible-module argument. Do not import or edit FormalizedSources/ or MainProjects/; those trees provide provenance and consumer evidence only. Keep the declarations in the established Module.Invertible, Submodule, and (where justified) Ideal namespaces rather than introducing an AGLib mathematics namespace. Dual-number-specific wrappers belong to a later consumer issue.

✅ Acceptance criteria

• Re-search the exact pinned Mathlib and current AGLib before adding each declaration. Reuse existing APIs where possible and do not publish a synonym for a more general theorem.
• Provide the audited theorem family, with canonical names or carefully justified replacements:
  Module.Invertible.free_of_span_singleton_eq_top;
  Submodule.top_le_span_sup_pow_smul_top;
  Module.Invertible.free_of_nilpotent_of_span_sup_smul_eq_top; and
  Module.Invertible.free_of_nilpotent_of_exists_sub_smul_mem.
  The last two must state the nilpotent ideal hypothesis and the exact pointwise modulo-I • M conclusion; do not silently add finite-generation, locality, domain, or field assumptions.
• Make the module universe-polymorphic (the ring and module may live in different universes where the surrounding APIs permit it) and audit all typeclass assumptions. In particular, reconcile the two source copies' existing-cyclic-lemma difference without importing route-local files.
• Keep the proof general: use Mathlib's invertibility and submodule machinery, retain the no-finiteness strength, and include a short counterexample or docstring warning if weakening nilpotency would make the statement false. A square-zero helper may be included only when the pinned Mathlib has no equivalent and it serves the generic API; do not add a dual-number namespace here.
• Add a small compiling AGLib consumer/smoke test for a nontrivial nilpotent ideal (and, if useful, a Mathlib dual-number specialization) without importing either flagship route. Expose the topic through AGLib/AGLib.lean only after the module's public surface is stable; do not broaden AGLib/Basic.lean.
• Give the module and every public result faithful docstrings, naming the two source candidates and explaining the nilpotency/no-finiteness hypotheses. If the documentation invokes Nakayama's literature result, add or reuse a precise stacks-project bibliography entry for tag 00DV in AGLib/docs/references.bib; otherwise cite the exact pinned Mathlib Nakayama API.
• The PR must contain no sorry, admit, hidden axiom, or bypass assumption, and must not edit the source-faithful projects.

🧪 Validation

Run focused contributor-LSP diagnostics on every changed Lean file, inspect the namespace/import graph, and check for proof-debt or accidental axioms. Leave the full build to protected CI; the PR must pass the repository's lake-build status for AGLib without changing the existing workflow.

[AxelDlv00]

Palimpsest automation ⚙️ 📣

Engine: codex
Model: gpt-5.6-sol
Effort: ultra

Queued by Palimpsest for contributor contributor. Review profiles: mathematical-correctness, maths-lean-correspondence, lean-quality, architecture. Claims expire automatically if the contributor session does not complete.

[AxelDlv00]

Palimpsest automation ⚙️ 📣

Engine: codex
Model: gpt-5.6-sol
Effort: ultra

Claimed by profile contributor as @AxelDlv00 until 2026-09-03 10:10:57 UTC. Branch: palimpsest/contributor/issue-9.