Skip to content

Ext of infinite modules via Nassau's untwisted tensor resolution - #279

Open
JoeyBF wants to merge 12 commits into
SpectralSequences:masterfrom
JoeyBF:claude/cohomology-field-resolution-cmcu0i
Open

Ext of infinite modules via Nassau's untwisted tensor resolution#279
JoeyBF wants to merge 12 commits into
SpectralSequences:masterfrom
JoeyBF:claude/cohomology-field-resolution-cmcu0i

Conversation

@JoeyBF

@JoeyBF JoeyBF commented Aug 1, 2026

Copy link
Copy Markdown
Collaborator

Compute Ext_A(M, k) — additively, plus products, Massey products, and the Adams d₂ — for
modules the minimal-resolution engine cannot reach, by resolving the base field and tensoring
instead of resolving M directly.

Contains #267. The bottom seven commits (up to ext_algebra: reframe docs so ExtAlgebra reads as classical Ext(k,k)) are #267 unchanged — this work builds directly on the ExtDifferential
trait and cohomology_subquotient introduced there. Review #267 first; this should land after
it, at which point those commits disappear from this diff. The four commits above that line are
this PR's own, and each compiles on its own.

The construction

A minimal resolution engine resolves a finite module directly, and its generators already are
Ext. It cannot resolve an infinite M such as H^*(RP^∞). Nassau's workaround:

  1. Minimally resolve the base field k, giving P• → k — finite, fast, already implemented.

  2. Tensor with M. Since A is a Hopf algebra, P_s ⊗_k M is free, so Q• = P• ⊗ M → M is a
    free — but non-minimal — resolution of M.

  3. Untwist the diagonal A-action through the antipode χ. The coboundary of Hom_A(Q•, k) then
    has the closed form

    δ_{(i,α),(l,γ)} = [m_α]( χ(a_li) · m_γ )
    

    where a_li ∈ A is the component of d_P(z_l) on the generator x_i.

Because δ is closed-form, Q• is never materialised: every computation is cochain-sized,
driven by the small resolution of k and the module action on M.

What's here

  • ext_algebra::tensor_resolution — the engine: TensorResolutionDifferential (serving as both
    the coboundary δ_Q and the cup product), Antipode, the tensor_resolution_ext /
    tensor_resolution_products entry points, and TensorResolutionSecondary for the Adams d₂.
  • A pluggable CochainCup alongside ext_algebra: let the Ext DGA carry a differential and compute cohomology #267's ExtDifferential. Since Q• is non-minimal,
    Ext_A(M, k) is the genuine cohomology of Hom_A(Q•, k) rather than its generators, so products
    are transported between the cochain and cohomology bases.
  • Massey products via the cochain DGA — on a non-minimal resolution the classical
    chain-map/null-homotopy bracket degenerates, so ⟨a, b, c⟩ is computed as [a ∪ v] with
    δ_Q v = b ∪ c. A minimal resolution attaches no cup and keeps the chain-map construction.
  • SecondaryLift::hit_generator() is now a runtime method defaulting to the compile-time
    HIT_GENERATOR, with SecondaryResolution::new_with_hit_generator to set it, plus a guard in
    SecondaryComposite::act for the empty output block an identity (op_degree = 0) action on a
    same-degree generator produces.
  • iter_s_t_inclusiveiter_s_t runs f(s, t) once f(s-1, t') is done for t' < t, which
    is right for a minimal resolution: d lands in Ā·P_{s-1}, so every coefficient has positive
    degree and f(s, t) reads only generators of degree strictly below t. A non-minimal
    differential has an identity component and can reach degree t itself. That is a shift of the
    wavefront by one column, not a reason to serialise filtrations, so both drivers are now wrappers
    over one engine parameterised by that lag.
  • δ_Q disk caching under a new SaveKind::TensorDifferential. Its header records only the
    algebra and bidegree, so two modules would collide by name and a shape check alone cannot
    separate them; each file stores a fingerprint of M and refuses to load for another.
  • examples/tensor_resolution.rs charts Ext_A(RP^∞, F_2), with a benchmark fixture so CI
    exercises the construction end to end.

Backward compatibility

The minimal path is unchanged: hit_generator() defaults to the old constant, lift/project are
identities on a minimal resolution so the cochain/cohomology transport is a no-op, and the lag-1
driver path is textually the existing iter_s_t.

Testing

Pinned against the direct minimal resolution wherever one exists — C2 for the additive Ext, the
products, the Massey products and the d₂; RP^∞ for the additive Ext and the products, against
the direct non-Nassau resolution. Also ∂² = 0 on Q•, a δ_Q save/load round trip plus a test
that a directory populated for one module is refused for another, a check that the construction
collapses to P• when M = k, and ordering tests for the new driver that assert the dependency
from inside f (under concurrent a recorded completion order proves nothing about happens-before).

Two tests are #[ignore]d, with the reason in the attribute:

  • tensor_d2_matches_direct_c2_stem60 — correct but heavy. It passes under --features concurrent; it is skipped by default only for runtime.
  • tensor_d2_matches_direct_rp_inf — blocked by a mathematical obstruction, not by anything here:
    H^*(RP^∞) admits several secondary (B-module) structures and the secondary machinery assumes
    the zero one, which does not lift for RP^∞. The companion test
    secondary_zero_structure_fails_for_rp_inf shows the direct minimal resolution fails
    identically at (10, 3), so this is not a minimality problem.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo


Generated by Claude Code

claude added 11 commits August 1, 2026 05:36
`ExtAlgebra` models Ext as the cochain complex Hom(P•, k) = k^gens. Over a
field with a minimal resolution its coboundary is identically zero, so Ext is
just the generators. But a *deformation* (a motivic τ-Bockstein δ) or a
*secondary* operation (an Adams d₂) makes the coboundary nonzero, and then
the interesting object is its cohomology.

This adds that differential as a pluggable piece:

- `ExtDifferential`: a fixed bidegree `shift` plus, at each bidegree, the
  coboundary `matrix` in the generator bases. For graded coefficients (e.g.
  F₂[τ], graded by motivic weight) it also exposes `graded_dimension` /
  `matrix_capped`, so cohomology can be computed one graded slice at a time;
  the default (ungraded/field) makes those no-ops and recovers the old
  behavior exactly.
- `ExtAlgebra::with_differential` / `differential` to attach and read it.
- `cohomology_dimension` (+ `_capped`): dim H = gens − rank δ_out − rank δ_in.

It's generic — nothing here is motivic. The two consumers are the motivic
lift's δ and the secondary (d₂) machinery; the tests exercise it on the
classical sphere with a mock differential (kernel/image bookkeeping) and
confirm the zero-differential case is just the generators.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
Validate that the differential→cohomology abstraction serves a second consumer:
the Adams d₂. Two additions, no behavior change to existing paths.

- `ExtAlgebra::cohomology_subquotient(b)`: the cohomology at `b` as a
  `Subquotient` of the generators — ker(δ out) mod im(δ into), i.e. actual
  representatives of the surviving classes, not just the dimension. The natural
  companion to `cohomology_dimension`; the motivic side wants it (surviving-class
  reps) as much as the secondary side does.
- `SecondaryCoboundary: ExtDifferential`: the Adams d₂ presented as a coboundary
  on the primary ExtAlgebra, shift (n,s) → (n-1,s+2), matrix read from the
  secondary resolution's homotopies. Its `matrix` sizes each end at its own
  bidegree so an `a×0` (empty target: a d₂-cycle) and a `0×b` (off-axis source,
  in-quadrant target: an ambient-`b` image) stay distinct; off the first quadrant
  Ext is a *known* zero, in-quadrant-but-unresolved is unknown (`None`).

Gate test: attaching `SecondaryCoboundary` and computing the E₃ page via the
shared `cohomology_subquotient` reproduces the spectral-sequence bookkeeping's
`page_data` exactly across the sphere in a range (dimension at every bidegree,
including the axes). This is the groundwork for routing the secondary layer's
page/product machinery onto the shared path.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
…y path

The secondary layer computed its E₃ pages by building a whole Sseq<2, Adams>
per resolution and reading `page_data` off it. Now that the Adams d₂ is an
`ExtDifferential`, `cohomology_subquotient` computes the same E₃ page directly
(ker d₂ / im d₂), so the parallel bookkeeping is redundant.

- `ExtAlgebra::cohomology_subquotient(b)`: the E₃ page (representatives, not
  just the dimension `cohomology_dimension` gives).
- `SecondaryExtAlgebra` holds an Ext-with-d₂ for `M` and for the unit; its
  `page_data`/`unit_page_data` are now `cohomology_subquotient`, and
  `extend_all` no longer builds any Sseq. The `res_sseq`/`unit_sseq` fields,
  their construction, and the `e3_page_data` helper are gone.
- `SecondaryResolutionHomomorphism::hom_k` took a whole `Sseq` only to read one
  page (the λ-part's d₂-image quotient). It now takes the E₃ page as a function
  of bidegree and queries it at its own `lambda_source` — no fragile
  reconstruction of that bidegree by the caller (the first, index-arithmetic
  attempt is what the new product smoke test caught).

Hardening from review:
- assert `ExtDifferential::matrix` shapes in `cohomology_subquotient`
  (gens(b) rows / gens(b) columns), so a nonconformant impl fails loudly;
- debug_assert `rank_out + rank_in ≤ gens` before the cohomology subtraction;
- document that graded impls must override `graded_dimension`/`matrix_capped`
  together;
- the `MockDiff` test fixture now returns correctly-shaped zero matrices (via
  the resolution's generator counts), making it a valid reference for
  `cohomology_subquotient`, not just rank-only `cohomology_dimension`;
- `SecondaryCoboundary` is `pub(crate)` and derives its prime from the
  resolution instead of storing it.

Validated: `secondary-S_2` and `secondary-C2` benchmarks are byte-identical to
golden; new tests cover the E₃-page agreement, the mock subquotient, and that
the secondary product's Ext part is the primary product.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
… + nightly fmt

The `hom_k`/`hom_k_with` signature change (Sseq → E₃-page function) missed a
caller: `examples/secondary_massey.rs`, which only compiles under default
features (my local runs used --no-default-features, and my grep for callers
searched src/ only). Adapt its call to pass the E₃ page as a closure over the
example's existing `get_page_data`.

Also run nightly `cargo fmt` (the repo's rustfmt.toml enables unstable options —
reorder_impl_items, group_imports, format_strings — that stable rustfmt silently
skips), which the `lint` CI job checks.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
…lved range

`secondary_product`/`secondary_massey` query the E3 page one row past the
resolved filtration, where the outgoing d2 lands at an unresolved bidegree.
The old Sseq path (SecondaryResolution::e3_page) treats an uncomputed outgoing
differential as zero — those classes provisionally survive — so page_data was
always defined there. cohomology_subquotient is stricter: a None outgoing
matrix makes it return None, and unit_page_data's .expect() then panicked
(caught by the C2 v_1 benchmark under `just benchmarks`).

Reproduce the e3_page convention locally in SecondaryCoboundary::matrix by
distinguishing the two ends: an in-quadrant-but-unresolved *source* still means
the page is unknown (None), but an in-quadrant-but-unresolved *target* means
the secondary resolution records no d2 there yet, so give a `rows × 0` matrix
(the whole source is a provisional d2-cycle) instead of None. The generic
cohomology_subquotient contract is unchanged. That `rows × 0` matrix is never
consumed as an incoming differential, since the target bidegree's own
subquotient short-circuits to None at its numerator.

Verified byte-identical against the secondary-*, secondary_product-*, and
secondary_massey-* golden benchmarks.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
cohomology_dimension_capped mixed a capped generator count (graded_dimension)
with ranks read off matrix_capped without checking the matrices are the right
shape. An undersized capped matrix would understate a rank and silently
overstate the cohomology. Assert the outgoing matrix has `gens` rows and the
incoming matrix has `gens` columns before row-reducing, matching the shape
checks already in cohomology_subquotient.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
Lead ExtAlgebra and ExtDifferential with the classical story — Ext is the
cohomology of Hom(P•,k); minimal resolution ⇒ generators, non-minimal ⇒ the
canonical dualised differential Hom(d,k) — rather than the deformation story.
The Adams d2 / motivic δ are named only as *also* using the pluggable
coboundary, with the machinery kept in their own modules (the secondary layer);
they no longer headline ExtAlgebra's interface. Generalize graded_dimension's
wording from "motivic weight" to "a deformation base R" (F2[τ] as the example),
since the cap-sweep is the general R-module shape, not motivic-specific.

Docs only — no logic changes. Docs build clean under -D broken_intra_doc_links
-D private_intra_doc_links.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013ePtYD7Bt4iPeCtmqtqvZE
`iter_s_t` runs `f(s, t)` once `f(s - 1, t')` is done for every `t' < t`. That
is the right dependency for a minimal resolution: its differential lands in
`Ā·P_{s-1}`, so every coefficient has positive degree and `f(s, t)` only reads
generators of degree strictly below `t`.

A non-minimal differential has an identity component, so `f(s, t)` can read the
generator of degree exactly `t` one filtration down. That is a shift of the
wavefront by one column, not a reason to serialise filtrations, so
`iter_s_t_inclusive` is `iter_s_t` with the recursion advanced one step less:
having finished `(s, t)` it releases `(s + 1, t')` for `t' < T` instead of
`t' < T + 1`, where `T` is the contiguous computed prefix of filtration `s`.
Filtrations still overlap in time.

Both are wrappers over one engine, parameterised by that lag. The lag also
settles the seeding, which is not a free choice: at lag 1 the dependency of
`f(s, min_t)` is vacuous and every filtration can be seeded at once, which is
what `iter_s_t` does; at lag 0 it is `f(s - 1, min_t)`, so only the bottom
filtration may be seeded. The lag-1 path is textually the existing `iter_s_t`.

The tests assert the contract from inside `f` — that every `(s - 1, t')` with
`t' ≤ t` has completed before `(s, t)` runs — since under `concurrent` the
bidegrees genuinely overlap and a recorded completion order proves nothing
about happens-before.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo
…lution

`HIT_GENERATOR` was a compile-time constant on `SecondaryLift`, so whether
composites may hit same-degree generators was fixed per type. A
`SecondaryResolution` over a non-minimal complex needs it per instance: such a
differential has identity components, so `∂∂` genuinely lands on same-degree
generators. Add a `hit_generator()` method defaulting to the constant, and
`SecondaryResolution::new_with_hit_generator` to set it; `new` keeps the old
value, so every existing lift is unchanged.

`SecondaryComposite::act` also assumed a non-empty output block. With an
identity action (`op_degree == 0`) on a same-degree generator the block is
empty and `generator_offset` indexes out of range, so skip it before taking the
offset. This cannot arise for a minimal resolution, whose differential has no
identity component.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo
A minimal resolution engine resolves a finite module directly, and its
generators already are Ext. It cannot resolve an infinite `M` such as
`H^*(RP^∞)`. Nassau's workaround is to resolve the base field instead:
minimally resolve `k` as `P• → k`, then tensor with `M`. Since `A` is a Hopf
algebra `P_s ⊗_k M` is free, so `Q• = P• ⊗ M → M` is a free — but non-minimal —
resolution of `M`. Untwisting the diagonal action through the antipode `χ`
gives the coboundary of `Hom_A(Q•, k)` in closed form,

    δ_{(i,α),(l,γ)} = [m_α]( χ(a_li) · m_γ ),

where `a_li` is the component of `d_P(z_l)` on the generator `x_i`. Because `δ`
is closed-form, `Q•` is never materialised: every computation is cochain-sized,
driven by the small resolution of `k` and the module action on `M`.

`Q•` being non-minimal, `Ext_A(M, k)` is the genuine cohomology of
`Hom_A(Q•, k)` rather than its generators, so `ExtAlgebra` gains a pluggable
`CochainCup` alongside the `ExtDifferential` it already had, and products are
transported between the cochain and cohomology bases. Massey products go
through the cochain DGA: on a non-minimal resolution the chain-map/null-homotopy
bracket degenerates, so `⟨a,b,c⟩` is `[a ∪ v]` with `δ_Q v = b ∪ c`. A minimal
resolution attaches no cup and keeps the chain-map construction, where
lift/project are identities — so the minimal path is unchanged throughout.

`TensorResolutionSecondary` carries the same construction to the Adams `d₂`,
and `δ_Q` matrices are cached under a new `SaveKind::TensorDifferential`. That
header records only the algebra and bidegree, so two modules would collide by
name and a shape check alone cannot separate them; each file therefore stores a
fingerprint of `M` and refuses to load for another.

Correctness is pinned against the direct minimal resolution wherever one
exists: `C2` for the additive Ext, the products, the Massey products and the
`d₂`, and `RP^∞` for the additive Ext and the products against the direct
non-Nassau resolution. `tensor_d2_matches_direct_rp_inf` is ignored for a
mathematical reason recorded in the attribute — `H^*(RP^∞)` admits several
secondary structures and the machinery assumes the zero one, which the
companion test shows fails identically on the direct minimal resolution.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo
The example computes `Ext_A(RP^∞, F_2)`, a module the minimal-resolution engine
cannot reach. Rows above the highest non-zero one carry no information and are
dropped, so the header reports the range actually printed rather than the range
requested — otherwise every row is mis-indexed by the reader.

The benchmark fixture gives CI an end-to-end check of the construction. It
covers n = 0..20, s = 0..10 in well under a second, and the output is identical
with and without `--features concurrent`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo
@coderabbitai

coderabbitai Bot commented Aug 1, 2026

Copy link
Copy Markdown

Warning

Review limit reached

@JoeyBF, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 22 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: c68f559b-d1ee-47ab-a08d-54395bcc8e96

📥 Commits

Reviewing files that changed from the base of the PR and between 99ddfb6 and 85ad5ca.

📒 Files selected for processing (13)
  • ext/SAVE-FORMAT.md
  • ext/crates/sseq/src/coordinates/mod.rs
  • ext/examples/benchmarks/tensor_resolution-RPinf
  • ext/examples/secondary_massey.rs
  • ext/examples/tensor_resolution.rs
  • ext/src/ext_algebra/massey.rs
  • ext/src/ext_algebra/mod.rs
  • ext/src/ext_algebra/secondary.rs
  • ext/src/ext_algebra/tensor_resolution.rs
  • ext/src/resolution.rs
  • ext/src/resolution_homomorphism.rs
  • ext/src/save.rs
  • ext/src/secondary.rs

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

The `#[ignore]` attribute claimed ~4.5 min. Two measured runs with
`--features concurrent` took 1824s uncontended and 2071s while competing with
other cargo invocations, so ~30 min is the honest figure. Both passed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LdymHggmtPKyEsPEbF7DWo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants