AGLib: extract smooth morphism geometric reducedness and integrality

[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. Once that bootstrap is accepted, the repository-owned roadmap calls for Foundations APIs shared by at least two source or flagship modules. The pinned Mathlib already defines the predicates GeometricallyReduced, GeometricallyIrreducible, and GeometricallyIntegral, together with Smooth and SmoothOfRelativeDimension, but it does not provide the smooth-to-geometrically-reduced producer described below.

At reference commit 9223d85c786394721963a9d642b08d066b72a594, both flagship Algebraic-Jacobian routes carry a Mathlib-only, proof-placeholder-free implementation:

• MainProjects/AlgebraicJacobian/MilneKollar/AlgebraicJacobian/Curve/GeometricallyReduced.lean:55-162
• MainProjects/AlgebraicJacobian/PicardAlbanese/AlgebraicJacobian/Curve/GeometricallyReduced.lean:55-162

The shared API has two layers. The algebra layer proves that a flat, essentially finite-type, formally unramified algebra over a domain is reduced, then derives the etale and standard-smooth cases. The scheme layer proves Smooth.isReduced_of_field, installs Smooth.geometricallyReduced, bridges SmoothOfRelativeDimension, and derives geometric integrality when geometric irreducibility is present. The two route roots import this file, and downstream consumers include CurveProjectivity, Pic0EtRelativeDimension, Jacobian, BaseChangeInstances, and the Riemann--Roch/Albanese layers.

The pinned Mathlib has the field-specialized Algebra.FormallyUnramified.isReduced_of_field and the geometric-integrality constructors, but a search of the pinned tree found no equivalent of Smooth.geometricallyReduced or the domain/standard-smooth reducedness lemmas. No open issue or pull request covers this boundary. This issue is independent of the nilpotent-module issue discovered alongside it and should be queued after bootstrap issue #1.

🎯 Goal

Extract the route-independent smoothness/reducedness API into a narrow AGLib module (or a small acyclic pair of modules) that imports Mathlib only. Do not import or edit FormalizedSources/ or MainProjects/; those paths are provenance and consumer evidence, not dependencies. Keep declarations in the established Mathlib namespaces rather than placing mathematics under a blanket AGLib namespace.

✅ Acceptance criteria

• Re-search the exact pinned Mathlib and current AGLib before adding each declaration. Reuse a more general existing theorem when one exists; do not publish a synonym for the existing field-specialized result.
• Provide the audited algebra results represented by the source candidate: a flat, formally unramified, essentially finite-type algebra over a domain is reduced; etale algebras over a domain are reduced; and the corresponding ring-homomorphism and algebra forms for standard smooth algebras. Preserve the genuinely necessary flatness/domain/finite-type hypotheses.
• Provide the scheme-facing result that a scheme smooth over Spec K for a field K is reduced, the Smooth.geometricallyReduced instance, and the relative-dimension form. Derive the geometric-integrality forms through Mathlib's existing GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible; retain a dimension-one inference instance only if an audit shows it is canonical and does not create typeclass loops.
• Use universe-polymorphic, canonical statements and sensible instance priorities. Remove route names, challenge-specific examples, compatibility scaffolding, and broad import Mathlib; keep imports fine-grained and expose the topic through AGLib/AGLib.lean only when the public API is stable.
• Include a small compiling AGLib consumer/smoke test exercising both direct smoothness-to-reducedness and the geometric-integrality instance, without importing either flagship route.
• Add a module docstring and faithful declaration docstrings with provenance to both candidate files. Cite the precise Stacks results used by the structure theorem and smooth-over-a-field reducedness argument (at least tags 00T7 and 033B, or a justified more precise replacement) through AGLib/docs/references.bib, reusing an existing bibliography key when appropriate.
• The PR must contain no sorry, admit, hidden axiom, or proof-by-bypass assumption. Record any theorem-name or hypothesis change from the source audit in the PR description.

🧪 Validation

Run focused contributor-LSP diagnostics on every changed Lean file and check the import graph/namespace surface. Inspect the declarations for accidental axioms and proof-debt tokens. Leave the full package check to the protected CI workflow; the PR must pass the repository's lake-build status on AGLib without changing the CI 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 11:37:33 UTC. Branch: palimpsest/contributor/issue-8.