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.
Equivariant Ext of a point is degreewise finite and not total finite
Example
Assume the Axiom of Choice (The Axiom of Choice) and let act trivially on the point , in the setting of Equivariant constructible derived category of complex varieties (Invertible matrices and the general linear group , Algebraic group actions, orbit maps, orbit subschemes and scheme-theoretic stabilizers). Let be a field of characteristic zero and let also denote the constant equivariant object. Then Hence the Ext groups are degreewise finite-dimensional but their total direct sum is infinite-dimensional. The forgetful restriction to the ordinary point is not derived fully faithful.
Facts & Assumptions
Given: The Axiom of Choice; the coefficient field of characteristic zero; the group acting trivially on the point; the finite Stiefel approximations of General linear Stiefel approximations stabilize bounded constructible Hom with , , and .
For the trivial action on the point, is the full-rank frame space and is the associated quotient; the map is the -bundle of the construction, and is the constant sheaf (General linear Stiefel approximations stabilize bounded constructible Hom, Equivariant constructible derived category of complex varieties).
The bounded Hom comparison gives whenever (General linear Stiefel approximations stabilize bounded constructible Hom).
The graph charts identify with (Stiefel spaces, Grassmannians, and tautological bundles, Complex projective space and its holomorphic charts). The cell construction needed by CW complex with closure finiteness and weak topology is given explicitly in step 1.2; it is not supplied by either definition.
Cellular cochains with local coefficients compute singular cohomology (Cellular cochains compute cohomology with local coefficients); on a CW complex with cells only in even dimensions the cellular cochain differential is zero, so for even with and vanishes otherwise.
The equivariant Ext theorem gives degreewise finiteness and vanishing in sufficiently negative degrees for bounded constructible objects, and its range bookkeeping is the same finite-resolution comparison (Equivariant constructible Ext is degreewise finite and compatible with characteristic zero scalars).
On the ordinary point, for and vanishes otherwise: a bounded complex of finite-dimensional vector spaces concentrated in degree zero has Hom complex concentrated in degree zero.
For a metric space with contractible-open neighbourhood basis, constant -sheaf cohomology agrees with singular cohomology (Locally contractible metric spaces have singular constant sheaf cohomology). Also : a sheaf map is determined by the image of , and that section gives a map by locally constant scalar multiplication. Applying a -linear injective replacement therefore gives (Analytic field sheaves have injective derived models).
AC is present only because the consumed suppliers [F1], [F2], [F4], [F5] and [F7] assume it; the projective-space cell computation is finite and choice-free (The Axiom of Choice).
Proof technique: direct.
Verification
The group acts trivially on , and the frame space is ; the quotient is the space of complex lines in , i.e. . Under the resolution triple, the constant equivariant object corresponds to the pair because the pullback of along is the constant sheaf , which descends along the -bundle to . So .
The finite cells. Use the filtration by coordinate subspaces. For , the map from the closed unit ball in to given by sends its boundary to by , and is a homeomorphism on the interior to the affine chart complementary to ; its inverse chart coordinate is . The adjunction space formed by attaching this ball to maps continuously and bijectively to . It is compact and the target is Hausdorff by [F3], so this map is a homeomorphism. Induction gives a finite CW structure with one cell in each degree and no odd cells. Its cellular cochain differentials vanish; [F4] consequently gives singular cohomology in those even degrees and zero otherwise. Projective space is metrizable (embed a line as its orthogonal projection matrix) and its smooth ball charts give contractible-open bases; [F7] identifies this computation with constant-sheaf cohomology and hence with .
Fix . Choose with , so that the comparison range of [F2] applies; then by [F7] and step 1.2, which is for even and for odd . For choose any with ; the same comparison applies and because a CW complex has no negative cohomology. Hence for even and vanishes otherwise, which is the displayed computation.
The computation of step 2.1 is degreewise finite: each group is either or . Infinitely many even degrees are nonzero, namely all with , so the total direct sum contains a copy of in infinitely many degrees and is infinite-dimensional.
On the ordinary point, [F6] gives , while the equivariant group is by step 2.1. The restriction functor to the ordinary point would have to induce the comparison map on these Hom groups, and this map cannot be injective because its target is zero and its source is nonzero; hence restriction is not derived fully faithful. This proves all three assertions. AC is present only as recorded in [A1].
Remarks
-
The example exhibits exactly the two phenomena the equivariant Ext theorem separates: degreewise finiteness holds, while total finiteness fails already for the trivial action of on a point, where for every .
-
Restriction to the ordinary point is conservative but not derived fully faithful; the class in is invisible after forgetting the group action.
Depends on
- Analytic field sheaves have injective derived models
- Locally contractible metric spaces have singular constant sheaf cohomology
- The Axiom of Choice
- CW complex with closure finiteness and weak topology
- Invertible matrices and the general linear group $\operatorname{GL}_n(F)$
- Stiefel spaces, Grassmannians, and tautological bundles
- Equivariant constructible derived category of complex varieties
- General linear Stiefel approximations stabilize bounded constructible Hom
- Cellular cochains compute cohomology with local coefficients
- Equivariant constructible Ext is degreewise finite and compatible with characteristic zero scalars
- Algebraic group actions, orbit maps, orbit subschemes and scheme-theoretic stabilizers
- Complex projective space and its holomorphic charts
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
106 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
- Joseph Bernstein and Valery Lunts, Equivariant Sheaves and Functors, Lecture Notes in Mathematics 1578, Part I (Derived category and functors) (standard reference, not scraped)
- A. Hatcher, Algebraic Topology (Cambridge University Press, 2002); author-hosted complete PDF, cited sections read in the extracted text (standard reference, not scraped)