feat: roadmap for algebraic vector bundles

[0xSimex]

Adds a roadmap entry, TauCetiRoadmap/AlgebraicVectorBundles/, for the scheme-theoretic theory of algebraic vector bundles.

Scope

• finite locally free sheaves, locally constant rank, pullback, tensor, dual, symmetric/exterior powers, and determinant;
• the relative-spectrum anti-equivalence

  QCAlg(X)ᵒᵖ ≃ AffSch/X;
  

• the Stacks/EGA correspondence

  QCoh(X)ᵒᵖ ≃ GradedVB(X),
  

  and, after restricting and dualizing,

  FinLocFree(X) ≃ GeomVB(X);
  

• the section-valued universal property of the geometric total space and its compatibility with pullback and the standard algebra of bundles.

The conventions distinguish linearSpec(F) = Spec_X Sym(F), which represents linear functionals and is contravariant, from totalSpace(E) = Spec_X Sym(Eᵛ), which represents sections and is covariant.

Existing boundary

The roadmap was audited against the pinned Mathlib 05ae010 and Tau Ceti e8af08d. It consumes the existing IsQuasicoherent, IsFinitePresentation, IsLocallyFree, tildeEquiv, InvertibleSheaf, and FinitelyPresentedSheaf APIs, and specifies the sheaf-monoidal, relative-Spec, and geometric-total-space layers developed by the roadmap.

It also coordinates the intended shapes with mathlib4#27098, mathlib4#39553, mathlib4#39989, and mathlib4#40194, following compatible theorem names and interfaces.

Successors

Projective, Grassmann, and flag bundles, together with their quotient-classifying universal properties, are identified as a separate successor roadmap. Chow groups and characteristic classes then form a further successor, followed by a cohomological-realization roadmap adding cycle classes and Betti/de Rham comparison. Together with the merged Hodge-structures roadmap #49, this gives the interface needed to formulate the Hodge Conjecture.

Suggested.lean records complete target signatures for the three layers, including the relative-Spec and vector-bundle equivalences and the section-valued universal property of the geometric total space.

Roadmap: AlgebraicVectorBundles

(Disclosure: this roadmap and PR description were drafted and revised with OpenAI Codex under my direction and editing.)

[CBirkbeck]

🤖 AI-authored review. This review was written jointly by Claude (Anthropic, via Claude Code) and ChatGPT 5.6 Pro (OpenAI), and is being posted from @CBirkbeck's account on their behalf. Please read it as a Claude + ChatGPT 5.6 Pro review, not a human one.

Review of TauCetiRoadmap PR #297

Assessment: request changes.

I reviewed the current head, a4ef07f…. The roadmap has a good overall direction, particularly the distinction between

$$ \operatorname{linearSpec}(\mathcal F)=\operatorname{Spec}_X\operatorname{Sym}(\mathcal F) $$

and

$$ \operatorname{Tot}(\mathcal E) =\operatorname{Spec}_X\operatorname{Sym}(\mathcal E^\vee), $$

together with the resulting contravariant and covariant functorialities. The relative-Spec anti-equivalence, base-change goals, and section-valued universal property are also the right major pieces. However, the two proposed geometric target categories currently have the wrong morphisms, the determinant functor is not defined on the stated category, and several of the most important constructions are represented only by unrelated opaque sorry definitions. The current head also does not build.

1. GradedVectorBundle and GeometricVectorBundle have the wrong morphisms

This is the main blocking issue.

The roadmap defines

abbrev GradedVectorBundle (X : Scheme) :=
  (linearSpec X).EssImageSubcategory

abbrev GeometricVectorBundle (X : Scheme) :=
  (totalSpace X).EssImageSubcategory

and then proposes

noncomputable def linearSpecEquiv :
    (QuasicoherentSheaf X)ᵒᵖ ≌ GradedVectorBundle X

noncomputable def totalSpaceEquiv :
    FiniteLocallyFreeSheaf X ≌ GeometricVectorBundle X

Mathlib’s EssImageSubcategory is a full subcategory of the target category. Thus these categories contain every morphism of affine schemes over $X$ between objects in the essential image, not merely grading-preserving or fibrewise-linear morphisms.

Already over $X=\operatorname{Spec} k$, the rank-one object has total space $\mathbb A^1_k$. The scheme endomorphism

$$ t\longmapsto t^2 $$

is a morphism over $k$, and hence appears in both proposed full essential-image categories. It does not arise from a linear map $k\to k$. Consequently the induced linearSpec and totalSpace functors are not full, and the stated equivalences do not describe the intended categories.

The README actually gives the correct idea: morphisms in the target must preserve the grading, or equivalently preserve the zero, addition, and scalar-multiplication structure. But that structure never appears in Suggested.lean.

I suggest choosing one of the following two implementations.

Option A: graded quasicoherent algebras

Define a category of nonnegatively graded quasicoherent $\mathcal O_X$-algebras, with graded algebra morphisms, and then define the full subcategory of algebras freely generated in degree one. For example, schematically:

GradedQuasicoherentAlgebra X
gradedSymmetricAlgebra :
  QuasicoherentSheaf X ⥤ GradedQuasicoherentAlgebra X

FreeGradedQuasicoherentAlgebra X :=
  (gradedSymmetricAlgebra X).EssImageSubcategory

Using an essential image is appropriate here, because the ambient morphisms are already required to preserve the grading. Mathlib has generic graded-object infrastructure that should be used rather than representing a grading by an unrelated family of modules.

The target condition should preferably be an isomorphism of graded algebras

$$ \operatorname{Sym}^{\mathrm{gr}}(\mathcal A_1)\cong\mathcal A, $$

not merely separate module isomorphisms

$$ \operatorname{Sym}^n(\mathcal A_1)\cong\mathcal A_n. $$

The latter do not by themselves record compatibility with multiplication and the unit.

Option B: affine module schemes

A more geometric API would define an affine $\mathcal O_X$-module scheme: an affine $V\to X$ with

zero     : X ⟶ V
add      : V ×ₓ V ⟶ V
smul     : 𝔸¹ₓ ×ₓ V ⟶ V

satisfying the module laws. Morphisms would preserve all three operations. This directly excludes polynomial maps such as $t\mapsto t^2$.

There is already generic category-theoretic infrastructure for module objects in a cartesian monoidal category in CategoryTheory.Monoidal.Cartesian.Mod, so this should be investigated before introducing a one-off category of geometric bundles.

Under either implementation, keep separate functors

linearSpecScheme :
  (QuasicoherentSheaf X)ᵒᵖ ⥤ AffineSchemeOver X

linearSpec :
  (QuasicoherentSheaf X)ᵒᵖ ⥤ LinearSchemeOver X

with a theorem saying that forgetting the module or grading structure recovers linearSpecScheme. Then define the equivalence using the structured functor, not as an arbitrary opaque equivalence.

Also, the name GradedVectorBundle is misleading for an arbitrary quasicoherent sheaf. Unless finite local freeness is imposed, the resulting object is a linear scheme, not a vector bundle. I would use names such as LinearScheme or QuasicoherentLinearScheme, reserving GeometricVectorBundle for the finite locally free case.

2. The proposed determinant functor does not exist on all morphisms

The target

noncomputable def determinant :
    FiniteLocallyFreeSheaf X ⥤ InvertibleSheaf X

is not correct when FiniteLocallyFreeSheaf X contains all finite locally free sheaves and all module morphisms.

For a map $\mathcal E\to\mathcal F$, the usual exterior-power map

$$ \bigwedge^r\mathcal E\longrightarrow\bigwedge^r\mathcal F $$

gives a map between determinant lines only when the ranks agree. The standard determinant construction on a morphism is stated under equality of the source and target ranks.

There is no functorial repair obtained by declaring the determinant map to be zero when the ranks differ. For example, take a split inclusion and projection

$$ \mathcal O_X\longrightarrow \mathcal O_X^2 \longrightarrow \mathcal O_X $$

whose composite is the identity. Sending both unequal-rank maps to zero would send their composite to zero, whereas the determinant of the identity is the identity.

There are several correct APIs:

determinantObj :
  FiniteLocallyFreeSheaf X → InvertibleSheaf X

with functoriality only for isomorphisms;

determinant (r : ℕ) :
  FiniteLocallyFreeSheafOfRank X r ⥤ InvertibleSheaf X

for fixed rank;

or a determinant functor on the core/groupoid of finite locally free sheaves. A Knudsen–Mumford determinant functor on the exact category of vector bundles is another possibility, but that is a substantially larger piece of infrastructure.

For this roadmap, the fixed-rank functor is probably the cleanest first target.

3. The closed monoidal structure does not restrict to arbitrary quasicoherent sheaves as stated

The README asks for a symmetric monoidal closed structure on X.Modules and says that it should be restricted to quasicoherent sheaves.

The tensor product does restrict to quasicoherent sheaves. The ordinary sheaf internal Hom does not preserve quasicoherence for arbitrary quasicoherent source and target. A standard sufficient hypothesis is that the source be of finite presentation; in particular, for finite locally free $\mathcal E$,

$$ \mathcal H!om(\mathcal E,\mathcal F) \cong \mathcal E^\vee\otimes\mathcal F $$

is quasicoherent.

The roadmap should say:

• X.Modules is symmetric monoidal closed;
• QuasicoherentSheaf X is symmetric monoidal;
• internal Hom from a finitely presented, and especially a finite locally free, source lands in quasicoherent sheaves;
• finite locally free sheaves form a rigid symmetric monoidal category.

The closed structure should also be pinned by an adjunction, not merely by an opaque bifunctor:

tensorLeftAdjunction (E : X.Modules) :
  tensoringLeft E ⊣ internalHom.obj (Opposite.op E)

or an equivalent natural Hom equivalence. Otherwise the target does not specify that the proposed internalHom is the internal Hom for the proposed tensor product.

4. The intrinsic geometric categories promised in the README are absent from Suggested.lean

The README says that a graded vector bundle should intrinsically consist of:

• an affine morphism $p:V\to X$;
• a grading on $p_*\mathcal O_V$;
• an identification of degree zero with $\mathcal O_X$;
• isomorphisms from the symmetric powers of degree one;
• grading-preserving morphisms.

None of these structures or recognition theorems appears in Suggested.lean. Instead, the target category is only the full essential image discussed above.

This leaves out one of the main advertised achievements of the roadmap: recognizing vector bundles intrinsically rather than simply naming the image of a functor. At minimum there should be target declarations for:

GradedLinearScheme X
GradedLinearScheme.Hom
gradedLinearSchemeOfSymmetricAlgebra
degreeOne :
  GradedLinearScheme X ⥤ QuasicoherentSheaf X
linearSpecDegreeOneIso
degreeOneLinearSpecIso

and the analogous finite locally free subcategory.

A useful factorization would be:

$$ \mathrm{QCoh}(X)^{\mathrm{op}} \simeq {\text{free graded quasicoherent algebras}}^{\mathrm{op}} \simeq {\text{graded affine linear schemes over }X}. $$

The first equivalence is algebraic and the second is relative Spec. This separates two conceptually different arguments and provides much better intermediate APIs.

5. The current target file does not build

At the current head, dependency resolution succeeds but the Lean build fails with two errors.

The first is in finiteLocallyFreeToFinitelyPresented: the use of the generic full-subcategory inclusion does not provide the required finite-presentation instance for the arbitrary object introduced internally. This can be avoided by defining the object map directly from E.property.2, or by using the appropriate object-property lift with an explicit preservation proof.

The second is in pullbackObjIso: the selected Scheme.Modules.pullback.mapIso is not an isomorphism of the expected objects. This is also evidence that pullback should be defined by lifting the existing module pullback functor through the finite-locally-free object property. Then the forgetful comparison should be supplied by the standard lifted-subcategory API, and will often be definitional rather than requiring a custom mapIso.

I would require a green build before merging the roadmap, since these are not warnings in proof bodies but failures in the proposed declaration shapes.

6. The relative-Spec equivalence needs to be decomposed into named functors and universal properties

The bare target

noncomputable def relativeSpecEquiv :
    (QuasicoherentAlgebra X)ᵒᵖ ≌ AffineSchemeOver X

conceals almost all of the mathematical work. Relative Spec and its affine anti-equivalence are correct goals, including the pushforward-algebra and base-change statements.

The roadmap should expose at least:

relativeSpec :
  (QuasicoherentAlgebra X)ᵒᵖ ⥤ AffineSchemeOver X

affineFunctions :
  AffineSchemeOver X ⥤ (QuasicoherentAlgebra X)ᵒᵖ

relativeSpecHomEquiv :
  (T ⟶ relativeSpec.obj (Opposite.op A)) ≃
    (pullbackAlgebra T.hom).obj A ⟶ 𝒪_T

relativeSpecPushforwardIso :
  affineFunctions.obj (relativeSpec.obj (Opposite.op A)) ≅
    Opposite.op A

relativeSpecCounitIso :
  relativeSpec.obj (affineFunctions.obj V) ≅ V

relativeSpecBaseChangeIso :
  baseChange f (relativeSpec.obj (Opposite.op A)) ≅
    relativeSpec.obj (Opposite.op ((pullbackAlgebra f).obj A))

together with naturality and the triangle identities needed to construct the equivalence.

There is substantial hidden infrastructure here:

• pushforward of the structure sheaf along an affine morphism as a quasicoherent algebra;
• pullback of quasicoherent algebras;
• the strong symmetric monoidal structure on module pullback;
• comparison with ordinary affine Spec when $X$ is affine;
• compatibility with composition and identity base changes.

These should appear as explicit dependency layers rather than being hidden inside relativeSpecEquiv.

7. The universal property of total space needs naturality

The proposed

totalSpaceHomEquiv (E) (T) :
  (T ⟶ totalSpace E) ≃
    (𝒪_T ⟶ pullback T.hom E.obj)

is the right pointwise statement, but a collection of unrelated equivalences is not enough. The universal property should be natural in both $T$ and $E$. In particular, a morphism $\mathcal E\to\mathcal F$ must correspond under the equivalence to postcomposition on sections, and a morphism $T'\to T$ must correspond to pullback of sections.

I suggest either a Yoneda-level natural isomorphism or explicit naturality lemmas:

totalSpaceHomEquiv_natural_left
totalSpaceHomEquiv_natural_right
totalSpaceHomEquiv_id
totalSpaceHomEquiv_comp

The construction should also be visibly obtained from the relative-Spec universal property and finite-locally-free duality:

$$ \operatorname{Hom}_X \bigl(T,\operatorname{Spec}_X\operatorname{Sym}(\mathcal E^\vee)\bigr) \cong \operatorname{Hom}_{\mathcal O_T} \bigl(f^*\mathcal E^\vee,\mathcal O_T\bigr) \cong \operatorname{Hom}_{\mathcal O_T} \bigl(\mathcal O_T,f^*\mathcal E\bigr). $$

Add a characteristic theorem such as

totalSpace_eq_linearSpec_dual

or define totalSpace through linearSpec and dual so that this relation is definitional.

8. Too many opaque definitions lack characteristic equations

The target file currently introduces opaque definitions for:

• finite-locally-free pullback;
• tensor product;
• internal Hom;
• dual;
• symmetric and exterior powers;
• determinant;
• symmetric algebra;
• relative Spec;
• linear Spec;
• total space;
• the two summit equivalences.

Many have no theorem identifying their underlying object with the intended existing construction. With sorry, these declarations could all be satisfied by unrelated choices, so the target file does not currently enforce the architecture described in the README.

For each construction, add a projection or comparison theorem. For example:

@[simp]
theorem pullback_obj_val :
    ((pullback f).obj E).obj =
      (Scheme.Modules.pullback f).obj E.obj

@[simp]
theorem tensor_obj_val :
    (tensorFiniteLocallyFree.obj (E, F)).obj =
      E.obj ⊗ F.obj

theorem dual_obj_iso :
    (dual.obj (Opposite.op E)).obj ≅
      internalHomObj E.obj (𝒪 X)

theorem symmetricPower_obj_iso :
    ((symmetricPower n).obj E).obj ≅
      SymmetricPower n E.obj

theorem exteriorPower_obj_iso :
    ((exteriorPower n).obj E).obj ≅
      ExteriorPower n E.obj

theorem linearSpec_obj_iso :
    affineSchemeOverForget.obj
      ((linearSpec X).obj (Opposite.op F)) ≅
      relativeSpecScheme (symmetricAlgebra.obj F)

theorem totalSpace_obj_iso :
    affineSchemeOverForget.obj ((totalSpace X).obj E) ≅
      relativeSpecScheme
        (symmetricAlgebra.obj ((dual X).obj (Opposite.op E)))

For the proposed equivalences, state that their forward functors are the named functors:

linearSpecEquiv_functor_iso :
  linearSpecEquiv X |>.functor ≅ linearSpecStructured X

totalSpaceEquiv_functor_iso :
  totalSpaceEquiv X |>.functor ≅ totalSpaceStructured X

Without such a statement, an opaque equivalence does not establish that linearSpec or totalSpace is the equivalence.

9. Rank should be a bundled locally constant function

The roadmap currently proposes a function

rank (E : FiniteLocallyFreeSheaf X) (x : X) : ℕ

followed by a theorem that it is locally constant. Since local constancy is fundamental to almost every later operation, it would be cleaner to define

rank :
  FiniteLocallyFreeSheaf X → LocallyConstant X ℕ

and derive pointwise notation from evaluation. Rank is locally constant for finite locally free modules.

Then add:

rankLocus (E) (r : ℕ) : Opens X
rank_pullback
rank_iso
rank_tensor
rank_dual
rank_directSum
rank_symmetricPower
rank_exteriorPower

and define the fixed-rank property and subcategory:

isFiniteLocallyFreeOfRank (X) (r : ℕ) :
  ObjectProperty X.Modules

FiniteLocallyFreeSheafOfRank X r

This resolves the determinant problem and gives the local-triviality theorems a precise statement.

10. The promised rank-one comparison is only one-way

The README promises to identify rank-one finite locally free sheaves with the existing InvertibleSheaf API, but Suggested.lean only defines a functor

invertibleToFiniteLocallyFree

There should be an equivalence

invertibleSheafEquivFiniteLocallyFreeRankOne :
  InvertibleSheaf X ≌ FiniteLocallyFreeSheafOfRank X 1

with a theorem identifying the underlying module-sheaf functors.

This is important because TauCeti already has an InvertibleSheaf and tensor-product API; the new vector-bundle development should extend that API rather than create an adjacent rank-one theory.

11. The fibre entry in the dictionary is imprecise

The README identifies

module fibre E ⊗ k(x)  |  scheme fibre over x

These are not literally the same kind of object. The correct statement is

$$ \operatorname{Tot}(\mathcal E)\times_X\operatorname{Spec}\kappa(x) \cong \operatorname{Spec}_{\kappa(x)} \operatorname{Sym}\bigl((\mathcal E_x\otimes\kappa(x))^\vee\bigr). $$

Its $\kappa(x)$-rational points identify with the vectors of the module fibre. The roadmap should distinguish the affine-space scheme associated to the fibre from its set of rational points.

A useful target is:

totalSpaceFiberIso (E) (x : X) :
  fiber (totalSpace E) x ≅
    affineSpaceOfModule (E.fiber x)

together with the induced equivalence on $\kappa(x)$-points.

12. The monoidal structure should use the generic subcategory machinery

Mathlib already has generic infrastructure for giving a full subcategory a monoidal structure from an object property closed under the tensor product and containing the unit.

Rather than adding unrelated instances

modulesMonoidalCategory X
quasicoherentMonoidalCategory X

I suggest:

1. build the monoidal and closed structure generically for sheaves of modules over a sheaf of rings;
2. prove that quasicoherence is an ObjectProperty.IsMonoidal;
3. prove that finite local freeness is an ObjectProperty.IsMonoidal;
4. obtain the full-subcategory structures from the generic API;
5. prove that finite locally free sheaves form a rigid category.

The existing presheaf-of-modules monoidal infrastructure should be the starting point, with sheafification supplying the sheaf tensor product.

This would make the following statements consequences of coherent categorical structure rather than separate constructions:

tensorFiniteLocallyFree
dual
evaluation
coevaluation
doubleDualIso
internalHomIsoDualTensor

Pullback should similarly be a strong symmetric monoidal functor, since that single API supplies the tensor, dual, symmetric-power, exterior-power, and determinant base-change comparisons.

13. Base change needs one coherent pseudofunctorial API

The roadmap includes pullback and a few identity/composition examples, but the main constructions all require compatible base-change isomorphisms.

I would introduce named functors and comparisons:

pullbackQCoh
pullbackFiniteLocallyFree
pullbackQuasicoherentAlgebra
baseChangeAffineSchemeOver

pullbackIdIso
pullbackCompIso
pullbackTensorIso
pullbackDualIso
pullbackSymmetricPowerIso
pullbackExteriorPowerIso

relativeSpecBaseChangeIso
linearSpecBaseChangeIso
totalSpaceBaseChangeIso

and record the identity and composition coherence conditions. Otherwise each later layer will construct its own slightly different change-of-base isomorphism.

14. Direct sums, flatness, and exact sequences are promised but not targeted

The README includes direct sums, rank formulae, flatness, and locally split short exact sequences, but Suggested.lean has no corresponding declarations.

For direct sums and additive structure, add at least:

finiteLocallyFree_zero
finiteLocallyFree_biproduct
rank_biproduct
totalSpace_biproduct_iso_product

For exact sequences, the useful theorem is that a short exact sequence of vector bundles is locally split when the quotient is locally free. The category of vector bundles is naturally treated as an exact category with these sequences.

The assertion that finite locally free is equivalent to finitely presented and flat also requires a definition of flatness for module sheaves, locality of flatness, compatibility with stalks and affine restriction, and the affine finite-presentation-plus-flat theorem. I did not find an existing sheaf-level flatness API at the pinned Mathlib revision. Either add a genuine flatness sublayer or remove this from the core deliverables rather than leaving it implicit.

15. The affine comparison should be more than an opaque equivalence

The proposed

tildeFiniteProjectiveEquiv :
  FiniteProjectiveModule R ≌
    FiniteLocallyFreeSheaf (Spec R)

is important enough to expose its compatibility with all subsequent operations:

tildeFiniteProjectiveEquiv_obj_iso
globalSections_tilde_iso
tilde_tensor_iso
tilde_dual_iso
tilde_symmetricPower_iso
tilde_exteriorPower_iso
tilde_totalSpace_iso
rank_tilde

I would also avoid inventing a new bundled FiniteProjectiveModule unless necessary. Prefer a full subcategory of the existing ModuleCat R cut out by Mathlib’s finite and projective predicates. This will make the existing module tensor, dual, and symmetric/exterior-power APIs available without adapters.

16. Add concrete normalization tests

The roadmap would benefit from a few literal endpoint examples:

totalSpace_free :
  totalSpace (𝒪_X ^⊕ r) ≅ affineSpace X r

totalSpace_unit :
  totalSpace (𝒪_X) ≅ affineLine X

linearSpec_affine :
  linearSpec (ModuleCatSheaf.associated M) ≅
    Spec (SymmetricAlgebra R M)

totalSpace_affineFiniteProjective :
  totalSpace (tilde P) ≅
    Spec (SymmetricAlgebra R (Module.Dual R P))

These test the dual convention, the variance, and the relative-Spec normalization. They would catch exactly the kind of accidental reversal that is otherwise easy to introduce in this development.

Suggested restructuring

The current layers conceal several independent projects. I would split them approximately as follows:

Layer 0A: sheaves of modules

• tensor product and unit;
• internal Hom and tensor–Hom adjunction;
• symmetric monoidal and closed coherence;
• pullback as a strong symmetric monoidal functor.

Layer 0B: quasicoherent and finite locally free sheaves

• quasicoherence of tensor;
• finite local freeness, rank and rank loci;
• affine finite-projective comparison;
• direct sums and tensor products;
• rigid duality and dualizable-object characterization.

Layer 0C: polynomial operations

• symmetric and exterior powers;
• pullback and affine comparison;
• fixed-rank determinant;
• rank-one comparison with InvertibleSheaf.

Layer 1A: quasicoherent algebras and affine morphisms

• quasicoherent algebra category;
• pushforward algebra of an affine morphism;
• relative Spec functor and universal property.

Layer 1B: relative-Spec anti-equivalence

• unit and counit;
• affine-base comparison;
• base change;
• the actual anti-equivalence.

Layer 2A: structured linear schemes

• graded-algebra or affine-module-scheme structure;
• linear Spec with its zero, addition and scalar maps;
• full faithfulness and recognition via degree one.

Layer 2B: geometric vector bundles

• finite locally free degree-one piece;
• local triviality as affine space;
• covariant total-space functor;
• section universal property;
• total-space equivalence and fibre theorem.

This would make the roadmap much more implementable and would give later connections, Higgs-bundle, and Hodge-theoretic developments stable interfaces rather than one very large summit.

What is already good

Several choices in the roadmap are worth preserving:

• The distinction between linearSpec F and totalSpace E := linearSpec (Eᵛ) is correct and important.
• The variance of the two functors is handled correctly in the prose.
• Relative Spec and the anti-equivalence between quasicoherent algebras and affine schemes over $X$ is the right foundational theorem.
• The section-valued universal property for total spaces is the right geometric endpoint.
• Keeping finite locally free sheaves as a full subcategory of module sheaves is sensible.
• Exact dependency pins and explicit tracking of upstream Mathlib work are good.
• The roadmap correctly emphasizes base change rather than treating it as an afterthought.
• Reusing TauCeti’s existing invertible-sheaf and finitely-presented-sheaf APIs is the right direction.

Changes I would require before merge

1. Replace the full essential-image categories in AffineSchemeOver X by structured categories whose morphisms are grading-preserving or fibrewise linear.
2. Replace the determinant functor on all finite locally free sheaves by a fixed-rank, isomorphism-only, or exact-category version.
3. Correct the claim that the closed structure restricts to arbitrary quasicoherent sheaves.
4. Add the intrinsic graded/module-scheme categories and recognition theorems promised by the README.
5. Decompose relativeSpecEquiv into named functors, universal properties, unit/counit, and base-change theorems.
6. Add naturality to the total-space universal property.
7. Add characteristic equations for every opaque functor and for the forward functors of the summit equivalences.
8. Bundle rank as a locally constant function and add fixed-rank subcategories.
9. Add the rank-one equivalence with InvertibleSheaf.
10. Correct the fibre dictionary.
11. Add coherent strong-monoidal pullback and graded-algebra or affine-module-scheme APIs.
12. Make the target file build on the pinned dependency graph.

With those changes, this could become a strong roadmap. At present, the object-level picture is largely right, but the categorical morphisms and the target signatures do not yet formalize the mathematical theorem the README claims.

---

— Claude (Anthropic) + ChatGPT 5.6 Pro (OpenAI), posted via @CBirkbeck

[0xSimex]

Thanks @CBirkbeck — this was very helpful. I reworked the roadmap so that the geometric side carries the graded/linear structure and therefore has the correct morphisms; I also corrected the fixed-rank determinant and made the relative-Spec and total-space constructions explicit.

🤖 AI disclosure: This revision and comment were prepared with OpenAI Codex under my direction and review.