feat(AGLib): extract nilpotent invertible-module freeness

[AxelDlv00]

Contributor : contributor 🧑‍💻 📣

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

🔍 Scope

Closes #9.

Adds the Mathlib-only AGLib.RingTheory.Nilpotent.InvertibleModule API for
lifting a cyclic generator across a nilpotent ideal:

• 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
• Module.Invertible.free_of_nilpotent_of_exists_sub_smul_mem
• Ideal.isNilpotent_of_mul_self_eq_bot

The proofs use no finite-generation, Jacobson, locality, domain, or field
hypotheses. Ring and module universes remain independent where Mathlib allows
it; subtraction is required only by the pointwise form.

📚 Provenance and design

The module extracts the Mathlib-only cyclic-invertible route from the
MilneKollar NilpotentThickeningFree.lean candidate. The
PicardAlbanese candidate's same-universe cyclic lemma is documented as
provenance, but no flagship or route-local file is imported. The module
documentation records the nilpotency warning and cites the nilpotent generator
case of Stacks Project Tag 00DV; the corresponding entry is in
AGLib/docs/references.bib.

AGLib.lean publicly imports only the reviewed topic module. A separate
internal consumer is imported privately and checks the pointwise theorem on
the genuinely nonzero square-zero ideal (2) of ZMod 4, including the
square-zero helper.

🧪 Validation

• Completed contributor-LSP diagnostics for the topic module, smoke consumer,
  and umbrella: no errors or warnings.
• Verified all five public declarations: only standard Lean axioms
  (propext, Classical.choice, Quot.sound) and no source warnings.
• Checked the integrated diff for whitespace errors, proof-debt tokens,
  forbidden source-project imports, and unintended files.
• Full Lean CI / lake-build remains the repository's protected CI check.

[AxelDlv00]

Reviewer : mathematical-correctness 📐 ✅

Profile: mathematical-correctness (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: bb1666a

🔍 Coverage

I reviewed exact head bb1666ae03a6436344c1a625b113c0b6e47995ef against issue #9, the PR description, changes.diff, both cited source candidates, and pinned Mathlib commit fabf563a7c95a166b8d7b6efca11c8b4dc9d911f.

The mathematical surface is exactly the issue-scoped family: the four required declarations at AGLib/AGLib/RingTheory/Nilpotent/InvertibleModule.lean:69, :88, :119, and :141; the permitted square-zero helper at :164; and the supporting ZMod 4 smoke example. There is no omitted acceptance-criterion theorem or unrelated mathematical addition. The intended boundary is also preserved: no dual-number wrapper and no source-project theorem or import enters the public API.

✅ Verified

• Module.Invertible.free_of_span_singleton_eq_top: span R {m} = ⊤ makes LinearMap.toSpanSingleton R M m surjective via its exact range identity. The source R and target M are both invertible, so pinned Mathlib's Module.Invertible.bijective_of_surjective makes this map bijective; the resulting R ≃ₗ[R] M transports freeness from R. This remains valid for a commutative semiring and an additive commutative monoid, including the trivial-semiring case; no domain, nontriviality, or subtraction assumption is being used implicitly.

• Submodule.top_le_span_sup_pow_smul_top: the n = 0 case is N ⊔ ⊤ = ⊤. In the successor step, scalar multiplication distributes over N ⊔ I • ⊤, associativity identifies (I ^ n) • (I • ⊤) with I ^ (n + 1) • ⊤, and Submodule.smul_le_right gives (I ^ n) • N ≤ N. Thus the induction proves the stated inclusion for every n, without finite generation or a Jacobson-radical hypothesis. I also checked I = ⊥ and the degenerate exponent-zero witness possible over a trivial semiring; both collapse to the asserted conclusion.

• Module.Invertible.free_of_nilpotent_of_span_sup_smul_eq_top: IsNilpotent I supplies an exponent j with I ^ j = ⊥. Substituting this into the preceding inclusion gives ⊤ ≤ span R {m}, hence the exact cyclicity hypothesis needed by the first theorem. The proof establishes the stated freeness conclusion rather than a weaker localized result.

• Module.Invertible.free_of_nilpotent_of_exists_sub_smul_mem: for each x, the supplied equation x = r • m + (x - r • m) places the two summands in span R {m} and I • ⊤, respectively. This proves the required supremum is top and invokes the preceding theorem. AddCommGroup M is used precisely for this subtraction step; no stronger ring hypothesis is hidden.

• Ideal.isNilpotent_of_mul_self_eq_bot and the smoke consumer: I * I = ⊥ is exactly the exponent-two witness after pow_two. For I = (2) ⊂ ZMod 4, the test correctly proves 2 ^ 2 = 0 and 2 ≠ 0, so the ideal is genuinely nonzero and square-zero. Choosing m = 1 and r = x satisfies the pointwise hypothesis.

The module's mathematical warning is also sound. Stacks Tag 00DV, Lemma 10.20.1(10–12), states the nilpotent, no-finiteness generation forms used here. For the counterexample, Stacks Tag 0B8I identifies invertible modules with finite locally free rank-one modules; consequently a nonprincipal invertible ideal has one-dimensional fibers L / mL, while an R-module isomorphism R ≅ L would make L principal.

🧪 Validation

• review.json, the immutable source snapshot, the changed-file snapshots, and the forge record all agree on the expected head SHA.
• A static scan of both changed Lean modules found no sorry, admit, or axiom declaration.
• I did not start LSP or Lake: this job has PALIMPSEST_ALLOW_LSP=0 and PALIMPSEST_LAKE_POLICY=deny, as required by $PALIMPSEST_DOCUMENTATION/pr-review.md. The mathematical decision is based on the exact source and pinned-library definitions, not inferred from CI alone.

📚 References consulted

• Stacks Project, Tag 00DV, Lemma 10.20.1(10–12) gives the nilpotent Nakayama iteration and generator forms without finiteness.
• Stacks Project, Tag 0B8I, Lemma 15.119.2 gives the finite-locally-free rank-one characterization of invertible modules.
• Pinned Mathlib PicardGroup.lean supplies invertibility of R and Module.Invertible.bijective_of_surjective.
• A focused mathlib PR search found no close precedent for the exact nilpotent invertible-module API. The closest relevant discussion, mathlib4 PR #33361, concerns the finite/Jacobson branch of Tag 00DV(8), so it is materially different from this PR's nilpotent branch; current source and Tag 00DV are the controlling evidence here.

💬 Decision

Approve. I found no mathematical-correctness issue in this exact head.

[AxelDlv00]

Reviewer : maths-lean-correspondence 🌉 ✅

Profile: maths-lean-correspondence (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: bb1666a

🔍 Coverage

I reviewed exact head bb1666ae03a6436344c1a625b113c0b6e47995ef against issue #9, the PR description, changes.diff, all four changed files, both source candidates at reference commit 9223d85c786394721963a9d642b08d066b72a594, and pinned Mathlib commit fabf563a7c95a166b8d7b6efca11c8b4dc9d911f.

The changed public surface is exactly the four required declarations at AGLib/AGLib/RingTheory/Nilpotent/InvertibleModule.lean:69, :88, :119, and :141, plus the issue-permitted generic square-zero helper at :164. I also checked the private helpers and anonymous consumer in InvertibleModuleTest.lean. The intended boundary is preserved: there is no dual-number wrapper, route-local declaration, flagship import, or omitted acceptance-criterion theorem.

✅ Verified

• Definition identity and cyclic freeness. Pinned Mathlib's Module.Invertible R M is the class asserting bijectivity of the canonical contraction Mᵛ ⊗[R] M → R, not another invertibility predicate. It provides the instance for R, while Module.Invertible.bijective_of_surjective requires the source and target modules to be invertible. Here the source is exactly R and the target is exactly M. LinearMap.toSpanSingleton R M m is the map r ↦ r • m, and LinearMap.range_toSpanSingleton identifies its range with Submodule.span R {m}. Therefore free_of_span_singleton_eq_top turns the stated cyclicity hypothesis into an equivalence R ≃ₗ[R] M and then into precisely Module.Free R M.

• Ideal action, powers, and nilpotency. Mathlib's I • N is the submodule generated by products i • n; it is the intended IN, and Submodule.smul_le_right gives IN ≤ N. Its global IsNilpotent I is literally ∃ n, I ^ n = 0, with 0 for ideals equal to ⊥. Thus top_le_span_sup_pow_smul_top expresses M = N + IM ⇒ M = N + IⁿM (as the equivalent top inclusion) for every n. The zero exponent is deliberately tautological, and the successor proof uses the correct product order. Substituting the nilpotency exponent in free_of_nilpotent_of_span_sup_smul_eq_top yields ⊤ ≤ span R {m}, in the required direction, before invoking the cyclic theorem.

• Implicit hypotheses and universes. The iteration itself assumes only CommSemiring R, AddCommMonoid M, and Module R M; no finiteness, Jacobson, locality, domain, or field premise is present. The freeness theorems add exactly the advertised invertibility premise. Pinned Mathlib does derive Module.Finite R M from invertibility, so I read the documentation's “no finite-generation hypothesis” correctly as “no separate finite-generation premise or Nakayama proof dependency”; this does not narrow the stated class beyond invertibility. The ring and module remain in independent universes u and v throughout.

• Pointwise form. At InvertibleModule.lean:141, the additional AddCommGroup M is exactly what makes x - r • m available. Membership in I • ⊤ says the remainder lies in IM, and the proof reconstructs x = r • m + (x - r • m). Hence every element lies in span R {m} ⊔ I • ⊤, which is exactly the asserted generation modulo I • M; neither the implication nor the quotient interpretation is reversed or weakened.

• Square-zero helper and non-vacuity. Ideal.isNilpotent_of_mul_self_eq_bot supplies exponent 2, since I ^ 2 = I * I. The smoke consumer proves (2) ⊂ ZMod 4 is square-zero and also proves (2) ≠ ⊥; choosing m = 1 and r = x then satisfies the pointwise premise. This witnesses a genuine nonzero nilpotent ideal and confirms that the theorem family is not being exercised only in an inconsistent or zero-ideal context.

• Documentation and source correspondence. The two cited source files contain the same induction and pointwise theorem; the MilneKollar copy has separate ring/module universes and proves the cyclic step directly, while the PicardAlbanese copy has one universe and imports a route-local cyclic lemma, exactly as the module documentation says. Stacks Tag 00DV, Lemma 10.20.1(12), states that a set generating M/IM generates M when I is nilpotent, with no finiteness hypothesis. The new bibliography key stacks-project-00DV identifies that exact result. The public declaration docstrings accurately describe their Lean statements.

🧪 Validation

• review.json, the immutable source snapshot, and the live forge record agree on the expected head SHA.
• Static inspection found no alternate existing declaration in pinned Mathlib or AGLib and no proof-debt token in the changed Lean files.
• I did not start LSP or Lake: this job has reviewer LSP disabled and Lake denied, as required by $PALIMPSEST_DOCUMENTATION/pr-review.md. The correspondence decision uses the exact source, mounted reference material, and pinned library definitions rather than inferring intent from elaboration alone.

📚 References consulted

• Stacks Project, Tag 00DV, Lemma 10.20.1(12) gives the exact nilpotent generator statement; clauses (9)-(12) explicitly omit finite generation.
• Pinned Mathlib PicardGroup.lean fixes the identity of Module.Invertible; the same file provides invertibility of R, bijective_of_surjective, and the derived finite/projective instances.
• Pinned Mathlib Span/Basic.lean fixes the map and range identities used by the cyclic theorem, and pinned GroupWithZero/Basic.lean fixes the meaning of IsNilpotent.
• A focused mathlib PR search for the exact theorem names and for nilpotent Module.Invertible/Nakayama analogues found no close version of this API. The nearest relevant history is mathlib4 PR #33361, which refines Tag 00DV(8) and retains the explicit hypotheses (hN : N.FG) (hIjac : I ≤ jacobson ⊥); that is the finite/Jacobson branch, materially different from this PR's nilpotent iteration and clause (12).

💬 Decision

Approve. Every changed declaration, implicit assumption, and docstring in this review dimension corresponds to the intended mathematical claim, with no unintended vacuity or direction error.

[AxelDlv00]

Reviewer : lean-quality 🧪 ✅

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: bb1666a

🔍 Coverage

Reviewed the exact head bb1666ae03a6436344c1a625b113c0b6e47995ef against issue #9,
the pull-request description and diff, the changed-file snapshots, AGLib/ROADMAP.md,
the pinned Mathlib source, and the forge record. Within the Lean-quality
dimension I checked all five public declarations (InvertibleModule.lean:69,
:88, :119, :141, and :164), the private consumer, the umbrella import,
and the bibliography addition. The issue boundary is preserved: the change
adds the requested Mathlib-only module without importing either source route or
changing AGLib.Basic.

✅ Verified

• Module.Invertible.free_of_span_singleton_eq_top has the expected namespace
  and a maintainable proof chain through LinearMap.range_toSpanSingleton,
  Module.Invertible.bijective_of_surjective, and Module.Free.of_equiv.
  The public result does not carry gratuitous finiteness or same-universe
  restrictions.
• Submodule.top_le_span_sup_pow_smul_top states the reusable iteration in the
  natural Submodule namespace. Its induction makes the smul_sup, ideal
  multiplication, and containment steps explicit rather than relying on a
  fragile global simplification.
• The two nilpotent theorems compose through that helper with clear hypotheses
  and docstrings. The pointwise form uses AddCommGroup only for the stated
  subtraction/abel argument; no hidden instance, locality, or finite-
  generation requirement appears in the API.
• Ideal.isNilpotent_of_mul_self_eq_bot is a small, generic square-zero helper
  and is exercised by the consumer. There are no sorry, admit, axiom,
  unsafe, debug, or scratch declarations in the changed code.
• The new module and every public theorem have faithful documentation. The
  source-candidate provenance, the precise Stacks result (Tag 00DV, Lemma
  10.20.1 (12)), and bibliography key stacks-project-00DV are all present.
• File placement, namespaces, theorem spelling, import grouping, indentation,
  and line width follow the local/mathlib guides. The pinned import graph makes
  PicardGroup the source of the invertible-module API; there is no broad
  Mathlib or route-local dependency, and no new global instance or API
  attribute is introduced.
• The anonymous private ZMod 4 consumer checks a genuinely nonzero square-zero
  ideal and is imported privately by the umbrella, so it exercises the public
  theorem without expanding the exported API. This matches the compiling-
  consumer gate in the repository roadmap.

🟡 Non-blocking import observation

At InvertibleModule.lean:8, Mathlib.LinearAlgebra.FreeModule.Basic is already
publicly reachable at this pinned Mathlib head through PicardGroup's import
closure (Contraction → Dual.Lemmas → FreeModule.Finite.Basic). The direct
import (and the analogous test import) is therefore transitive cleanup rather
than a correctness or performance defect; retaining it is also a reasonable
explicit dependency if that upstream import closure changes.

🧪 Validation

• The live forge metadata and review.json agree on the base and head SHAs.
• Static scans of the exact diff found no proof-debt tokens, forbidden source
  imports, whitespace/width violations, or unintended files.
• The unchanged CI workflow contains the protected lake build AGLib check, and
  the Lake/toolchain pins are consistent. No timing/profiling artifact is
  exposed in this review context, so the efficiency assessment above is static.
• I did not run Lake, a full build, or LSP; the reviewer policy forbids those in
  this immutable context.

📚 References consulted

• Local policy: /tmp/palimpsest-documentation/pr-review.md, style.md,
  naming.md, doc-strings.md, and mathlib-reviewing.md.
• Pinned Mathlib definitions: PicardGroup.lean
  and FreeModule/Basic.lean.
• A focused search for Module.Invertible/nilpotent cyclic-freeness found no
  close Mathlib API precedent; PR 33361
  is the materially different finite/Jacobson route.

💬 Decision

✅ Approve. I found no blocking Lean-quality issue on the exact reviewed
head.

[AxelDlv00]

Reviewer : architecture 🏗️ ✅

Profile: architecture (architecture)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: bb1666a

🔍 Coverage

I reviewed pull #10 at exact head bb1666ae03a6436344c1a625b113c0b6e47995ef against issue #9, changes.diff, the four changed files, the accepted AGLib/ROADMAP.md, the pinned Mathlib tree, both cited source candidates, and their direct consumers. The issue asks for one reusable foundations-layer extraction, not a route port. The diff delivers exactly that boundary: four requested public theorems, the explicitly permitted square-zero helper, a private concrete consumer, root exposure, and the matching bibliography entry. There are no omitted requested declarations, unrelated AGLib modules, source-project edits, or route imports.

✅ Verified

• Foundations placement and trajectory. The production module AGLib/AGLib/RingTheory/Nilpotent/InvertibleModule.lean is pure commutative module theory. It imports only Mathlib, extends the established Module.Invertible, Submodule, and Ideal namespaces, and does not introduce a blanket AGLib mathematics namespace. It therefore sits in roadmap layer 1 and has no edge to a later AGLib layer or a flagship route.

• Cyclic-invertible group (:69). Module.Invertible.free_of_span_singleton_eq_top follows the canonical Mathlib route: the span equality makes LinearMap.toSpanSingleton surjective, and pinned Module.Invertible.bijective_of_surjective upgrades that map to an equivalence. The result is then expressed as Module.Free, which is the existing downstream abstraction. The source and module universes are independent (u and v), and the theorem does not introduce a route-local definition or compatibility facade.

• Nilpotent iteration group (:88, :119, :141). Submodule.top_le_span_sup_pow_smul_top is the reusable foundation lemma behind the two public nilpotent forms. The induction only uses submodule supremum/smul operations and ideal powers; it does not package a missing result behind finite-generation, locality, or Jacobson assumptions. Substituting the exponent supplied by IsNilpotent produces the exact cyclic hypothesis consumed by free_of_span_singleton_eq_top. The pointwise theorem is kept as the consumer-facing boundary and adds only the AddCommGroup structure needed for subtraction. This is a coherent API family rather than an isolated theorem dump.

• Square-zero bridge and consumer (:164, InvertibleModuleTest.lean). Ideal.isNilpotent_of_mul_self_eq_bot is generic, has no existing equivalent in the pinned Mathlib search, and is explicitly allowed by issue AGLib: extract nilpotent Nakayama freeness for invertible modules #9. The smoke consumer exercises the public pointwise theorem on the genuinely nonzero square-zero ideal (2) of ZMod 4; it is not a dual-number-specific declaration and does not import either source route.

• Source correspondence and reuse. The MilneKollar and PicardAlbanese candidates contain the same iteration and consumer-facing route, and their DualNumberChartTriviality files call these results. The new module extracts the MilneKollar Mathlib-only route, while documenting the PicardAlbanese cyclic lemma as provenance rather than importing it. This gives the roadmap's required shared-by-two-sources foundation and leaves route-specific wrappers where they belong. The untouched source copies are an intentional migration boundary; a later consumer-migration issue can remove those duplicates without making AGLib depend on the source projects.

• Public boundary and dependency order. AGLib/AGLib.lean:8-9 publicly exposes the stable topic alongside the existing bootstrap module, while the test at :11 is an ordinary import and therefore does not re-export Smoke declarations. The production file's direct Mathlib imports are justified by its exported Module.Free and Module.Invertible API. A static search found no exact declaration already present in pinned Mathlib or AGLib and no import-cycle indicator.

🟡 Integration notes

• AGLib/AGLib.lean:11 privately imports InvertibleModuleTest so the package's single AGLib target compiles the required consumer. That is a reasonable issue-scoped validation arrangement and does not enlarge the public API, but it makes ZMod and test-only dependencies part of every umbrella compilation. When the package gains a separate test target, move this consumer there while keeping the public import at :9 and the production module unchanged. This is non-blocking for the current roadmap milestone.

• AGLib/README.md still describes the bootstrap as exposing no declarations of its own. That wording is now stale after the reviewed root exposure, but it does not alter the dependency graph or the usable API; it is suitable for a small documentation follow-up rather than a change request on this extraction.

🧪 Validation

• review.json, the immutable source/ snapshot, and the live forge record all agree on base 3defc91b228ace7c9e0ca3f62f41b58d89bc2278 and head bb1666ae03a6436344c1a625b113c0b6e47995ef.
• The repository-owned .github/workflows/lean-ci.yml checks the root target with lake build AGLib; the immutable forge output did not include a CI result, so I make no independent green-status claim. Per review policy I did not start Lake, LSP, or cache downloads.
• Static scans of the changed Lean files found no sorry, admit, or axiom declarations, no source-project imports, and no unintended changed files.

📚 References consulted

• The accepted AGLib/ROADMAP.md (mission boundary, layer DAG, extraction gates, and replacement triggers) and the local Pull Request Review and Mathlib reviewing guides were the governing architecture criteria.
• The pinned Mathlib PicardGroup.lean defines Module.Invertible and bijective_of_surjective; FreeModule.Basic supplies Module.Free.of_equiv. No narrower pinned file defining the required invertibility class was found.
• A focused search of current Mathlib PR history for this exact API and for nilpotent Module.Invertible/Nakayama placement found no close equivalent. The nearest finite/Jacobson precedent is mathlib4 PR #33361, whose refined API retains the explicit hypotheses (hN : N.FG) (hIjac : I ≤ jacobson ⊥); that is materially different from this PR's terminating nilpotent iteration. Mathlib4 PR #41528 is a later semiring-generalization of the surrounding Module.Invertible API, useful as directional precedent but not authority over the pinned version.

💬 Decision

Approve. I found no blocking architecture or trajectory defect in this exact head: the change advances the accepted foundations route, preserves an acyclic Mathlib-only dependency boundary, and leaves a canonical migration path for the two source consumers.

[AxelDlv00]

Maintainer : maintainer-adviser 🧭 ✅

Profile: maintainer-adviser (maintainer,contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: bb1666a

🚦 Gate status

✅ Accepted exact head bb1666ae03a6436344c1a625b113c0b6e47995ef. The required lake-build status passed, and mathematical-correctness, maths–Lean-correspondence, Lean-quality, and architecture each recorded a current-head approval. No requested change remained unresolved.

🔀 Merge result

✅ Squash-merged pull #10 into palimpsest/aglib as 3b031ca81048858e2a5648f3d3bc712a0c3fd355. The merge adds the issue-scoped, Mathlib-only nilpotent invertible-module freeness API, its private ZMod 4 consumer, umbrella exposure, and the Tag 00DV bibliography entry.

🟡 Linked issue

Issue #9 still reports open after the merge. GitHub does not apply the PR's closing keyword when merging into this non-default integration branch, and this maintainer job's forge adapter does not expose an issue-state mutation.