Proper hypercovers compute constructible derived cohomology

Height zero and the induction setup. Let $U\to X$ be a bounded proper hypercover of height zero, that is $U={\mathrm{cosk}}_0{U}_0$. By the convention of the Given, $U$ is the Cech nerve of the proper surjection $U_0\to X$, so [F1] proves both the sheaf and the global augmentation statements for $U$. Suppose inductively that they are proved for all bounded proper hypercovers of height at most $n$, and let $U={\mathrm{cosk}}_{n+1}U$ have height $n+1$. Put $V:={\mathrm{cosk}}_{n}U$. Its matching maps through degree $n$ are those of $U$, and in degrees $j>n$ its matching map is an isomorphism because $V={\mathrm{cosk}}_{n}V$; hence $V$ is a proper hypercover of height at most $n$ and the induction hypothesis applies to $V$.

Levelwise proper surjectivity of $U\to V$. For every $j$ the map $U_j\to V_j$ is proper surjective. For $j\le n$ it is the identity. For $j>n$ it reads $\mathrm{Hom}({\mathrm{sk}}_{n+1}\mathrm{\Delta }[j],U)\to \mathrm{Hom}({\mathrm{sk}}_n\mathrm{\Delta }[j],U)$: the domain is obtained from the codomain by adjoining the finitely many nondegenerate $(n+1)$-faces of $\mathrm{\Delta }[j]$, whose boundaries already lie in the $n$-skeleton, so this map is a Cartesian pullback of the finite product of the matching map $U_{n+1}\to ({\mathrm{cosk}}_{n}U{)}_{n+1}=V_{n+1}$; a finite product over $X$ of proper surjections, and any base change of it, is proper surjective. No local sections are required, and all limits are the finite matching limits of the Given.

The bisimplicial Cech model and the double total. Form the bisimplicial object $W_{r,j}=U_j{\times }_{V_j}\cdots {\times }_{V_j}{U}_j$ with $r+1$ factors, horizontally the Cech nerve of $U_j\to V_j$, and pull coefficients from $X$ throughout. By [F1] and step 1.2, for each fixed $j$ the horizontally augmented derived row computes the coefficient complex on $V_j$, before and after pushing forward to $X$: with $B_j:=(V_j\to X{)}^{\ast }F$ and $a_{r,j}:W_{r,j}\to X$ one has $R{b}_{j\ast }{B}_j\simeq {\mathrm{Tot}}_{r}R{a}_{r,j\ast }{a}_{r,j}^{\ast }F$, where $b_j:V_j\to X$, the identifications being compatible with composition and finite sums by [F3] and [F4]. The induction hypothesis for $V$ gives $F\simeq {\mathrm{Tot}}_{j}R{b}_{j\ast }{B}_j$; substituting the row identifications and using that every total diagonal is finite (the internal degrees are bounded below by the same $a$, by [F3]) identifies the iterated total with the full total, so $F\simeq {\mathrm{Tot}}_{r,j}R{a}_{r,j\ast }{a}_{r,j}^{\ast }F$ and the analogous global statement hold. By [F2] this double total is naturally chain-homotopy equivalent to the total on the diagonal $D_j:=W_{j,j}$.

The retract over $X$. The bounded hypercover $U$ is a retract over $X$ of $D$. The map $i:U\to D$ repeats the same $U_j$-point in all $j+1$ horizontal factors, the horizontal degeneracy; through degree $n$ the map $U_j\to V_j$ is the identity, so $D_j=U_j$ there, and in degree $n+1$ let $r_{n+1}:D_{n+1}\to U_{n+1}$ be the projection to the first horizontal factor. Its faces and degeneracies agree with the degree-$\le n$ identity identifications, because every horizontal factor of $W$ has the same image in $V$ and the lower-degree maps are identities; this defines a map of $(n+1)$-truncated simplicial objects over $X$, and the universal property $U={\mathrm{cosk}}_{n+1}U$ extends it uniquely to $r:D\to U$. The composite $ri$ is the identity through degree $n+1$: in lower degrees because $i$ is the diagonal and $r$ the factor projection on $D_j=U_j$, and in degree $n+1$ because repeating a point and projecting a factor returns it; hence $ri=\mathrm{i}\mathrm{d}$ in every degree by the same universal property. Coefficient pullback reverses these maps, and since $r\circ i=\mathrm{i}\mathrm{d}$ the augmented total of $U$ is a retract of the augmented total of $D$; by step 2.1 the cone of the augmentation of $D$ is acyclic, and a retract of an acyclic cone is acyclic, so the augmentation of $U$ is a quasi-isomorphism. This completes the bounded-height induction.

Arbitrary height by truncation. For an arbitrary proper hypercover $U$, put $U^{(N)}:={\mathrm{cosk}}_N{\mathrm{sk}}_{N}U$; it is a bounded proper hypercover, so step 3.1 applies to it, and the canonical map $U\to U^{(N)}$ is the identity through simplicial degree $N$. In the strict derived total model every internal degree is at least $a$; hence total degrees $m-1$, $m$ and $m+1$ involve only simplicial levels $p\le m-a+1$, because a term of total degree $m+1$ has $p+q=m+1$ with $q\ge a$. Choose $N\ge \max (0,m-a+1)$; then the totals for $U$ and $U^{(N)}$ have the same objects and the same differentials in these three degrees, so the same degree-$m$ cohomology and the same augmentation maps. Since $m$ was arbitrary, the augmentation for $U$ is a quasi-isomorphism, and degree $m$ with its differential is determined by levels through $p=m-a+1$. This is a finite-degree truncation argument, not an interchange of stalks or cohomology with an unjustified infinite product.

The spectral sequence and convergence. Filter the global total of step 4.1 by simplicial degree. Its first page is $E_1^{p,q}=H^q(X_p,a_p^{\ast }F)$, with first differential the alternating sum of face pullbacks by the naturality of [F3]; in degree $m$ the filtration has only the finitely many pieces $0\le p\le m-a$. By [F5] the stationary page is identified, naturally, with the finite associated graded of $H^m(X,F)$; this proves strong convergence and requires no finite-dimensionality of the individual groups $H^q(X_p,a_p^{\ast }F)$.

Refinements and constant coefficients. For two proper hypercovers $U,V$ of $X$, the levelwise product $R_j:=U_j{\times }_X{V}_j$ is a proper hypercover: finite matching limits commute with products, so each matching map of $R$ is the product over $X$ of the matching maps of $U$ and $V$, hence proper surjective, and the levelwise projections give maps of simplicial objects $R\to U$ and $R\to V$ over $X$. By step 4.1 the augmentations of $U$, $V$ and $R$ all identify their totals with the same coefficient complex on $X$, and the refinement maps are compatible with those identifications by naturality of the augmentation, so all proper-hypercover refinements induce the same comparison via the base object. A smooth-projective refinement requires a separate supplied construction: a fiber product of smooth varieties over $X$ need not be a smooth variety, so no smoothness is asserted here. For $F=k_X$ the lower bound is $a=0$ and the page of step 5.1 is exactly the stated first-quadrant spectral sequence. The Axiom of Choice is inherited precisely through [A1].