Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hypercover total degree uses only a finite matching truncation

Example

Assume the Axiom of Choice as inherited from the proper-hypercover theorem. Let X∙→X be a proper hypercover and let F be a coefficient complex in Dcb(X;k) with cochain lower bound a (Simplicial objects, simplicial commutative rings and homotopy groups). Then the cohomology of the total complex in degree m, and its differential, are determined by the simplicial levels p≤m−a+1 only; every hypercover truncation cosk⁡Nsk⁡NX∙ with N≥m−a+1 computes the same Hm(X,F). In particular for the constant sheaf F=kX, where a=0, degree n uses only levels through n+1. Keeping only the cochain terms through level n and omitting the outgoing differential does not suffice in general: the differential out of the term (p,q)=(n,0) of the Cech complex lands in the level n+1 term (n+1,0).

Facts & Assumptions

Given: the proper hypercover X∙→X, the coefficient F∈Dcb(X;k) with cochain lower bound a, an integer m, and the truncations cosk⁡Nsk⁡NX∙; the Axiom of Choice is inherited from the proper-hypercover theorem and no new choice is made below.

[F1]

Proper hypercovers compute constructible derived cohomology supplies the two augmentation quasi-isomorphisms of a proper hypercover, the finite diagonals, and the statement that degree m and its differential are determined by levels through p=m−a+1.

[F2]

Simplicial objects, simplicial commutative rings and homotopy groups fixes the simplicial face and degeneracy operators and the Moore-complex conventions used for the Cech complex. The truncation and coskeleton conventions are given in [F1].

Verification

technique · direct
1.1F1given

Degree bookkeeping. In the total complex of the hypercover, the term in bidegree (p,q) has p≥0 and q≥a and contributes to total degree p+q. For a fixed total degree m this gives 0≤p≤m−a. The differentials entering and leaving total degree m involve terms of total degree m−1, m and m+1, so the largest simplicial level appearing in the data of Hm and of its differential is p=(m+1)−a=m−a+1.

2.1F1step 1.1construct

The truncation computes the same cohomology. By [F1], the comparison of X∙ with its N-coskeleton truncation cosk⁡Nsk⁡NX∙ is the identity through simplicial degree N, and the total complex in a fixed total degree uses only finitely many levels. Choosing N≥m−a+1 makes the two total complexes agree in degrees m−1, m and m+1; hence they have the same Hm and the same augmentation maps there. Since m was arbitrary, every truncation with N at least the stated bound computes the same cohomology Hm(X,F).

3.1F1F2step 1.1step 2.1algebra∎

Constant coefficients and sharpness for hard truncation. For F=kX the lower bound is a=0, so the actual total-degree computation uses the outgoing map from level n to level n+1. To see that omitting that map can change the answer in every degree, take the proper surjection from two reduced points S={0,1} to a point and its Cech nerve. The map is proper since preimages of compact sets are finite, and its fiber powers are finite discrete spaces. A sheaf on a finite discrete space is a family of vector spaces, so global sections are a finite product and exact. Hence the derived section model has internal degree zero only. The normalized degree-p cochains are k2, indexed by the two alternating nondegenerate strings of length p+1. Interior deletions give degenerate strings and vanish in the normalized differential; the two endpoint deletions give δp(v0,v1)=(v1+(−1)p+1v0,v0+(−1)p+1v1), which has rank one over every field. The full augmented complex is contracted by inserting one point, as in [F1], so its positive cohomology is zero and H0=k. If one retains only cochain levels 0,…,n and discards δn, its top cohomology is k for n>0 and k2 for n=0, giving the wrong answer. Thus level n+1 is necessary in general for this hard truncation of the cochain data. A coskeleton truncation is different: it reconstructs higher levels from matching limits, so no claim that cosk⁡nsk⁡nX∙ itself fails descent is made.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources