Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated↗ rests on later material
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.

Point operations and the open closed constructible line

Example

Assume the Axiom of Choice (The Axiom of Choice) and let k be a field. (1) The constructible category of a point is the bounded derived category of finite-dimensional k-vector spaces, Dcb(pt⁡;k)≃Db(k-Vectfd) (Algebraically constructible complexes of analytic field sheaves). For the identity map of the point, all four pullback/pushforward operations f∗,f∗,f!,f! are the identity functors of that category, the tensor product and internal Hom are the usual finite cochain constructions, and the dualizing object is k concentrated in degree 0 (Derived tensor–Hom and inverse/direct image for field sheaves ↗, Derived operations on analytic field sheaves ↗). (2) On the complex line with the open inclusion j:C∗↪C and the closed inclusion i:{0}↪C, there is a k-linear short exact sequence of sheaves 0→j!kC∗→kC→i∗k→0, and its associated exact triangle is the ordinary localization triangle of the constructible derived category.

Facts & Assumptions

Given: The Axiom of Choice, a field k, the point pt⁡ with its unique stratification, and the complex line with j:C∗↪C and i:{0}↪C. The point-operation clauses use the actual ordinary-operations lemma and the exceptional-candidate Definition named by the two later-page forward references.

[F1]

Dcb(X;k) is the full subcategory of Db(Sh⁡k(X)) of complexes with bounded, algebraically constructible cohomology, constructibility being local constancy of finite rank on the strata of a witnessing finite smooth algebraic frontier stratification (Algebraically constructible complexes of analytic field sheaves).

[F2]

Under AC the k-sheaves carry functorial injective resolutions, and with the dependent choice supplied by AC the bounded-below injective complexes with bounded cohomology model the bounded derived category, so Hom groups are computed by these replacements (Analytic field sheaves have injective derived models).

[F3]

For an open inclusion j:U↪X with closed complement Z and inclusion i:Z↪X, every sheaf of abelian groups F on X fits into a short exact sequence 0→j!(F∣U)→F→i∗(F∣Z)→0 (Extension by zero and the closed complement: a short exact sequence).

[F4]

A sheaf of abelian groups on X whose stalks vanish off a closed subset Z is canonically the pushforward of its restriction to Z (A sheaf with no stalks off a closed subset is a pushforward).

[F5]

Extension by zero is left adjoint to restriction and is exact on sheaves of abelian groups (Extension by zero is left adjoint to restriction and is exact on abelian sheaves).

[F6]

The mapping cone of a chain map f:C∙→D∙ has degree-n term Cone⁡(f)n=Dn⊕Cn−1 with differential dn(y,x)=(dnD(y)+fn−1(x),−dn−1C(x)) (The mapping cone of a chain map).

[F7]

The derived category is triangulated with cone triangles, and every distinguished triangle gives a long exact cohomology sequence; rotating a triangle gives a distinguished triangle (The derived category inherits a triangulated structure).

[A1]

The axiom of choice is used through the injective models of [F2] and in the degreewise splitting of a bounded complex of possibly infinite-dimensional vector spaces in step 1.1; the line computation itself is finite and explicit (The Axiom of Choice).

Verification

technique · direct
1.1F1F2A1algebra

A sheaf on the point is its vector space of sections, and the point's unique stratification makes constructibility exactly finite-dimensional cohomology by [F1]. For a bounded complex V, choose complements Zn(V)=Bn(V)⊕Hn and Vn=Zn(V)⊕Ln using AC. The differential identifies Ln with Bn+1(V), so V is the direct sum of the zero-differential complex (Hn) and a contractible complex of pairs Ln→∼Bn+1(V). If all cohomology is finite-dimensional, (Hn) is a bounded finite-dimensional representative, including the acyclic case where it is zero. Every vector space is injective under AC, because extending a basis splits every vector-space inclusion and extends every linear map from its subspace. Bounded complexes of vector spaces thus compute derived morphisms as homotopy classes by [F2], in both the finite-dimensional and full vector-space categories. For two finite-dimensional complexes these chain maps and homotopies are identical in both categories, proving full faithfulness as well as essential surjectivity. Hence Dcb(pt⁡;k)≃Db(k-Vectfd).

2.1F1F2A1step 1.1

On the point inverse and direct image of the identity are exact identity functors, and every section has compact support, so the proper-support functor is also the exact identity. Their derived functors are therefore identities. In the exceptional candidate of Derived operations on analytic field sheaves ↗, the fibre opens are only the point and the empty set; compact sections are exact, giving dimension bound d=0, and the constant sheaf k is itself c-soft, so take K=k[0]. For a bounded finite-dimensional complex B every term is injective over k, and the candidate has sections Hom⁡k∙(k,B)=B on the point and zero on the empty set. Thus f! is the identity with its ordinary evaluation adjunction, and ωpt⁡=apt⁡!k=k[0]. The ordinary-operations lemma Derived tensor–Hom and inverse/direct image for field sheaves ↗ identifies tensor and internal Hom with the finite signed complexes: (A⊗B)n=⨁p+q=nAp⊗kBq, with d(a⊗b)=dAa⊗b+(−1)pa⊗dBb, and Homn(A,B)=∏pHom⁡k(Ap,Bp+n), with dφ=dBφ−(−1)nφdA. Their terms and amplitudes are finite, so they belong to the category identified in step 1.1. Here f∗ and f! in the Example denote their derived operations, which coincide with their exact underived functors in this case.

2.2F3F4F5step 1.1

Apply [F3] to the constant sheaf F=kC on X=C, with U=C∗ and Z={0}: the restriction kC∣C∗ is the constant sheaf kC∗, the restriction to the closed point is k, and the sequence reads 0→j!kC∗→kC→i∗k→0, the terms being computed by [F5] for the extension by zero. Stalkwise the middle sheaf is exact: at x≠0 the stalk of j!kC∗ is k and the stalk of i∗k is 0, while at 0 the first stalk is 0 and the last is k; the quotient of kC by j!kC∗ has no stalks off {0}, and by [F4] it is canonically the pushforward i∗k of its restriction to the closed point. All maps are k-linear, since they are obtained from the canonical adjunction units of [F5] applied to k-sheaves.

3.1F1F6F7step 2.2construct∎

In cochain grading, the cone C of the map g:kC→i∗k has C−1=kC, C0=i∗k and differential g, by reindexing [F6]. Put A=j!kC∗. The chain map u:A[1]→C given by the kernel inclusion in degree −1 is a quasi-isomorphism: step 2.2 gives H−1(C)=A, H0(C)=0, and u induces the identity on the only possible nonzero cohomology. The cone triangle kC→i∗k→C→kC[1] is distinguished by [F7]. Its signed inverse rotation and the quasi-isomorphism −u:A[1]→C give the distinguished triangle A→kC→i∗k→A[1] with the kernel inclusion as first arrow: the inverse rotation negates the projection C[−1]→kC, cancelling the sign of −u. All three sheaves restrict to constant finite-rank sheaves (including rank zero) on each stratum of {C∗,{0}}, so this localization triangle lies in Dcb(C;k).

Remarks

  • The point computation specializes the actual later-page operation interfaces to d=0 and K=k[0]. The line computation uses the published extension-by-zero sequence, mapping-cone convention and triangulated structure.

  • The example deliberately makes no claim that the four operations of the later formalism exist for arbitrary maps here; it computes only the identity map of the point and the two inclusions of the line, where the triangle is the localization triangle.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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