feat: roadmap for analytic toric geometry

[Paul-Lez]

• Supply the missing finite fan-to-scheme layer in Toric-compatible Mathlib carriers.
• Construct analytic toric charts, finite-fan gluing, proper maps, boundary strata, and algebraic comparison.

Sources: Fulton and Cox–Little–Schenck.

AI assistance: Codex (GPT-5) and Codex 5.6 Sol.

[CBirkbeck]

Part of a deep adversarial review of the reusable-roadmap split — PRs #279–#284, reviewed 25 August 2026. This section covers #281 — Analytic toric geometry.

Head reviewed: c36cf7b4dfa3e8633c15abfb8036c71d270535b5

Verdict

Major changes requested.

The new scope is appropriate and reusable, and the insistence on one toric dialect is exactly right. The current roadmap is nevertheless not closed under its prerequisites. It assumes an algebraic fan/toric-scheme API which is not present in the public Toric project or at the Tau Ceti pin, and several infinite-fan statements are false or undefined without stronger finiteness conditions.

1. The stated algebraic supplier does not currently exist

The roadmap says that Yaël Dillies's Toric project and Mathlib already supply:

• rational cones;
• fans and fan morphisms;
• dual affine semigroups;
• affine toric schemes from cones;
• gluing from fans;
• algebraic toric morphisms.

The current public Toric project does not yet expose this stack. Its root imports group schemes, tori, monoid algebras, toric ideals, a generic ToricVariety class, and a FromMonoid construction. Its ToricVariety definition is a scheme with a dense torus and action; it is not a fan construction.

Therefore Layer 0 is not an import boundary yet. “Coordinate with the Toric maintainers” is good policy but does not supply a prerequisite.

Choose one of the following:

1. make this PR explicitly stacked on a named Toric branch/PR whose declarations are listed and imported;
2. create a separate algebraic toric-geometry roadmap owning cones, fans, semigroups, fan schemes, and morphisms;
3. expand Layer 0 into a full, definite supplier with exact declarations and sources.

Do not merge while the central input is a prospective external API with no exact branch or declarations.

2. Mathlib's PointedCone is not a strongly convex toric cone

Mathlib defines PointedCone R E as a submodule under nonnegative scalars: it is a convex cone containing zero. In standard toric terminology, a fan cone must also be rational polyhedral and strongly convex/salient:

[
\sigma\cap(-\sigma)={0}.
]

The roadmap currently speaks as if PointedCone already expresses this condition.

Add an explicit toric-cone predicate or structure, built on the Mathlib carrier, containing:

• finite generation/polyhedrality;
• rationality with respect to the lattice;
• strong convexity;
• the primitive-ray API.

Regularity then says that the primitive ray generators extend to a lattice basis. Without the strong-convexity condition the dense-torus and orbit-cone statements are not the standard toric theorems.

A useful regression test is the full line in a rank-one lattice: it is a Mathlib PointedCone, but its dual semigroup gives a point, not an affine toric curve with dense one-dimensional torus.

3. “Locally finite fan” is not defined and has a trap at the origin

Every cone contains zero. Hence the family of cones of an infinite fan is never locally finite as a family of subsets of the whole vector space: every neighbourhood of zero meets every cone.

The roadmap must define the intended condition. Possibilities include:

• local finiteness of intersections with the unit sphere;
• finite star of every cone;
• local finiteness of relative interiors away from zero;
• an explicit finite-cone condition.

The topological consequences must be proved from the chosen definition. The bare phrase “countable locally finite fan” is not an unambiguous input.

4. The support criterion needs quasi-compactness for infinite fans

For finite-type toric varieties, the usual support criterion characterizes proper toric morphisms. For an infinite fan, equality of supports does not by itself provide quasi-compactness or finite type, which are part of properness.

Restrict the properness and compactness theorems to finite fans, or add an exact quasi-compactness hypothesis, such as a finite source-cone cover above each target cone. The same issue affects:

• “complete iff compact”;
• properness of subdivisions;
• the countable locally finite version of the map theorem.

Do not transfer the finite-fan criterion verbatim to an infinite non-quasi-compact gluing.

5. The topology in Suggested.lean is defined so that the main homeomorphism is tautological

regularAffinePointTopology e is the topology induced through the chosen equivalence

[
X_\sigma(\mathbb C)\simeq\mathbb C^k\times(\mathbb C^\times)^l.
]

The following regularAffinePointHomeomorph is then true by definition. It does not verify the roadmap's intended topology from a finite monomial embedding, nor independence from generators or from the extending basis.

Define the complex-point topology independently:

• from a finite set of semigroup generators and the resulting closed monomial embedding; or
• from an already supplied analytification topology.

Then prove:

• independence from the generating set;
• the regular-coordinate map is a homeomorphism;
• changing the extending basis preserves the atlas;
• this topology agrees with the algebraic complex-point comparison.

6. The analytic point carrier needs an exact global comparison

For an affine scheme, AlgHom ℂ[S] ℂ is the correct affine functor-of-points carrier. For a global toric scheme, the roadmap must state exactly how:

[
\operatorname{Hom}(\operatorname{Spec}\mathbb C,X_\Sigma)
]

is compared with the topological gluing of affine point sets. This needs a theorem that complex-valued points respect the affine open-cover gluing and that the overlap equivalences are the same maps.

“Complex points of the algebraic toric variety” must not mean the underlying prime-ideal space of the scheme.

7. The monomial calculus is incomplete on regular charts

The suggested file has:

• polynomial monomials on (\mathbb C^n);
• Laurent monomials on ((\mathbb C^\times)^n).

Maps between regular affine charts

[
\mathbb C^k\times(\mathbb C^\times)^{n-k}
]

require mixed exponent matrices, with negative exponents permitted only in invertible coordinates. Add the typed mixed-monomial carrier and its composition/holomorphy conditions.

8. Pin the simple-normal-crossings carrier

The roadmap promises that the toric boundary is an SNC divisor, but no exact public notion is selected. State whether the conclusion is:

• a finite or locally finite family of embedded complex hypersurfaces;
• a union with local coordinate-hyperplane normal form;
• an effective divisor with multiplicities one;
• or all three, with comparison theorems.

This is especially important for countably many rays.

9. The special deformation-retraction material must remain specialized

The README mentions positive-part and spine deformation retractions. Such a contraction is not canonical for an arbitrary regular fan. State the exact combinatorial hypotheses and keep honeycomb or A₂-fan conclusions in the downstream construction project.

10. Suggested.lean is not representative of the roadmap

It currently checks local set-level monomial formulas. It has no target for:

• the fan carrier;
• analytic realization;
• chart gluing;
• Hausdorffness;
• torus actions and orbits;
• boundary divisors;
• fan morphisms;
• the properness criterion;
• algebraic–analytic comparison.

Once the algebraic supplier is fixed, import it and seed these declarations. Until then, a green build does not validate the roadmap's central architecture.

What should remain

• the reusable analytic scope;
• the rule that Tau Ceti must not create a second toric dialect;
• the regular-coordinate local model;
• the chartwise rather than general-GAGA comparison;
• coordinate-free characters and basis-dependent coordinate lemmas;
• explicit countability requirements;
• coordination with the Toric maintainers.

Recommended disposition

Keep the PR in draft. First fix the algebraic supplier contract and the definitions of toric cone, infinite fan, and properness. The remaining analytic layers can then be reviewed against actual imported objects.

---

Cross-roadmap notes (apply across the #279–#284 split)

• PRs #280, #282, #283, and #284 still use the Levent six-sphere PDF as the link in the PR body. These are now general-purpose roadmaps. The construction paper should be described only as a motivating consumer; each PR body should instead foreground the standard sources listed in its README.
• Every downstream roadmap should import or #check the exact representative interfaces of its supplier once those suppliers land. Prose references alone are not enough to prevent incompatible carriers.
• The intended merge order is:
  #279 and corrected #283 first; #280 after both; #281 after #279 and an exact algebraic toric supplier; #282 after #279 and a reconciled compact-Riemann-surface degree API; and #284 after corrected #283 plus its geometric-topology and Morse/transversality suppliers.

[Paul-Lez]

🤖 Addressed in 57df472. The roadmap now supplies a definite finite Toric-compatible cone, fan, and scheme layer; distinguishes Mathlib PointedCone from salient toric cones; restricts support properness and compactness to finite fans; defines affine topology independently through monomial embeddings; types mixed monomial maps; pins global Spec-point gluing and the finite SNC boundary carrier; and expands Suggested.lean across the algebraic and analytic interfaces.

[CBirkbeck]

Part of the second deep review of the reusable-roadmap split — PRs #279–#284, reviewed 26 August 2026 against the updated heads. This section covers #281 — Analytic toric geometry.

Head reviewed: 57df47277145ed68c32b49356c50a504e6270c03

All six updated branches pass their current CI. The comments below concern the mathematics and the proposed public APIs, not elaboration failures.

What has been fixed

The revised roadmap has addressed nearly every point from the first review:

• it restricts the main development to finite fans;
• it openly owns the missing algebraic fan-to-scheme supplier rather than pretending it already exists;
• a toric cone is required to be finite, rational and salient;
• the affine topology is defined independently by a monomial embedding;
• the regular coordinate theorem is no longer tautological;
• mixed affine/torus monomial maps are represented;
• the algebraic comparison uses actual Spec(ℂ)-points;
• the main gluing, orbit, boundary, properness and comparison interfaces are now seeded.

Unfortunately the foundational “integral lattice” predicate is still too weak, and this makes a stated theorem false.

1. IsIntegralLattice does not define a lattice

The current definition asks only that

i : N →+ V

be injective and that its real span be all of V.

Take

$$ N=\mathbf Z^2,\qquad V=\mathbf R,\qquad i(a,b)=a+\sqrt2,b. $$

This map is injective and its image spans R, but its image is dense and not discrete. It is not a lattice.

Now take the positive ray σ = R_{\ge 0}. Both (1,0) and (0,1) are primitive lattice elements whose images lie on the positive ray. Hence the proposed theorem that a rational salient ray has a unique primitive generator is false under the current hypotheses.

The clean correction is to require that the scalar-extension map

$$ \mathbf R\otimes_{\mathbf Z}N\longrightarrow V $$

be a linear equivalence. Equivalent full-lattice data—rank equality plus a discrete embedding and spanning—would also work, but the scalar-extension equivalence is the most useful toric interface.

2. Mixed monomial composition is false on the whole ambient space

mixedMonomialMap_comp is currently stated for every ambient point, rather than on mixedChartDomain.

Let a source torus coordinate be z. Let A produce the two torus coordinates

$$ (z,z^{-1}), $$

and let B multiply them. On the torus locus the composite is 1. At z=0, Lean's integer-power convention gives both problematic terms as zero, so B(A(0))=0, while the multiplied exponent is 0, giving 0^0=1.

Thus the equality is true on the natural locus where torus coordinates are nonzero, but not as an unrestricted ambient identity. State the theorem with hz : z ∈ mixedChartDomain ....

3. The boundary normal form must be holomorphic, not merely topological

The proposed local boundary normal form is represented by a PartialHomeomorph. A topological coordinate does not prove that a component is a complex hypersurface or that the boundary is a simple normal-crossings complex divisor.

The target should be a complex local chart, local biholomorphism or PartialDiffeomorph in the complex structure groupoid, with the coordinate functions proved holomorphic.

4. Minor: IsRegularCone should carry the toric-cone hypothesis

As a standalone predicate, regularity can currently hold vacuously or be discussed for cones which are not rational salient toric cones. Either add IsToricCone i σ to IsRegularCone, or document that it is only meaningful together with the separate toric hypothesis and keep every public theorem carrying both.

Verdict

Major changes requested. The finite-fan architecture is now good, but the integral-lattice definition invalidates the primitive-ray foundation and must be repaired before merge.

---

Cross-roadmap disposition (applies across #279–#284)

• #279: fix one gluing signature; then merge.
• #280: add the complex-linear analytic input and group-valued connecting API; then merge.
• #281: repair the lattice foundation and monomial-domain theorem before further review.
• #282: make cusp data primitive and resolve degree/Riemann–Hurwitz ownership.
• #283: fix the low-degree relative-homotopy carrier; then merge.
• #284: keep the revised README, but substantially rewrite Suggested.lean around genuine manifold orientations, tangent-bundle trivializations, collared boundary data and actual quadratic forms/formations.

[Paul-Lez]

🤖 Addressed in c43a1b0. Integral lattices now require a scalar-extension linear equivalence, regularity includes the toric-cone hypothesis, mixed monomial composition is restricted to the nonzero-coordinate domain, and the boundary normal form is complex-differentiable rather than merely topological.

[CBirkbeck]

Part of the third adversarial review of the reusable-roadmap split (#279–#284) and companion roadmaps (#288, #81, #250), reviewed 26 August 2026 against the current heads. This section covers #281 — Analytic toric geometry.

Head reviewed: c43a1b05280f26994d46f93eb1c4331a026ff60b

CI status at time of posting: the run on this head hit a workflow startup failure and has been re-queued; the routine build should complete before merging.

Result

Approve mathematically.

The foundational lattice error is fixed. IsIntegralLattice now asks for a scalar-extension equivalence

$$ \mathbf R\otimes_{\mathbf Z}N \simeq V, $$

which rules out dense injective maps such as
$(a,b)\mapsto a+\sqrt2 b$.

The other corrections are also present:

• IsRegularCone includes the toric-cone hypothesis;
• mixed monomial composition is stated only on the locus where torus coordinates are nonzero;
• the boundary normal form uses a complex PartialDiffeomorph, not merely a homeomorphism;
• the global complex points are morphisms Spec ℂ ⟶ X;
• the finite-fan restriction and properness support criterion are explicit.

I found no remaining mathematical blocker.

---

Cross-roadmap dependency recommendation — Analytic geometry chain

Acyclic implementation order:

ComplexManifolds
    ├── ComplexTori
    ├── AnalyticToricGeometry
    └── FuchsianOrbifolds core

ModularForms.LevelOne.JInputs
    └── FuchsianOrbifolds.LevelOne

RiemannSurface.Degree  (independent lower module)
    ├── FuchsianOrbifolds applications
    └── ModularForms.DimensionFormula

The generic degree/genus module must not depend on the higher ModularForms Riemann–Roch module.

Recommended disposition (all nine PRs)

1. Merge after routine CI: #279, #280, #281.
2. Small focused repairs: #283, #81.
3. Coordinate and repair together: #282 and #288.
4. Rewrite the representative architecture before merge: #284.
5. Complete the class-field endpoint and state the global-function-field scope: #250.

[mrdouglasny]

Status note, not a review — this is approved and I'm not asking for changes.

This looks merge-ready but is silently stuck on two things:

1. The required build check never ran on this head. Combined status on c43a1b0 is pending
   with zero contexts, and there is no build check run. This is the workflow startup failure
   @CBirkbeck flagged in the third-round review on 26 August — it was re-queued, but it appears
   never to have come back.
2. The branch is 106 commits behind main, and the ruleset enforces
   strict_required_status_checks_policy, so it has to be up to date regardless.

Updating the branch clears both, since the new head triggers a fresh build.

One thing to know before doing that: the ruleset also sets dismiss_stale_reviews_on_push, so the
update will dismiss the existing approval. That doesn't need another deep review — I'm on
roadmap-reviewers and happy to re-approve the updated head once build is green, on the strength
of the round-three verdict. Given the size of the gap the build is a real re-test rather than a
formality, so worth letting it finish first.