Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Singular UCT extension from cycle projections

Statement

Assume AC. Let C be a nonnegative complex of free modules over a commutative PID R, and let G be an R-module. Write Zj=ker⁡dj, Bj=im⁡dj+1 and Hj=Zj/Bj, with negative terms zero. Compute Ext⁡R1(Hn−1,G) from the length-one free resolution Bn−1↪Zn−1↠Hn−1. For every n≥0 the map ι:Ext⁡R1(Hn−1,G)⟶Hn(Hom⁡R(C,G)),[ψ]⟼[ψdn] is well-defined and injective. Its image is the kernel of evaluation β:[φ]↦([z]↦φ(z)), and β is surjective. These maps are natural in chain maps and coefficient homomorphisms. Identification of this Ext group with that computed from any other length-one projective resolution is independent of comparison lifts; no identification with an injective-resolution definition is assumed.

Facts & Assumptions

[F1]

A free PID complex decomposes into two-term cycle-boundary pieces proves, under AC, that Zj,Bj are free and supplies Cj=Zj⊕sj(Bj−1). Put πj(c)=c−sjdjc.

[F2]

Ext via a projective resolution of the first variable defines Ext from the cohomology of Hom of a supplied projective resolution, with positive differential.

[F3]

Singular cochain complex with coefficients uses the positive cochain convention δφ=φd, which we use for this general complex as well.

[F4]

The Axiom of Choice is assumed. The free lifting construction in Free modules are projective, with the exact choice boundary chooses preimages of basis values through surjections. Projective modules have that lifting property by definition.

Proof

Given: R,C,G,n as stated. A cochain of degree j is an R-linear map Cj→G, and its differential is precomposition with dj+1.

1.1F1F2F3given

The differential of these cochains squares to zero because dj+1dj+2=0. A cocycle φ kills Bn, so its restriction to Zn factors uniquely through Hn. A coboundary hdn vanishes on Zn. Thus β is well-defined and linear, including on both kinds of representatives. By [F1], 0→Bn−1→Zn−1→Hn−1→0 is a free resolution. By [F2], its Ext group is Hom⁡(Bn−1,G) modulo the restrictions of maps Zn−1→G.

2.1F1F3step 1.1

For ψ:Bn−1→G, the cochain ψdn is closed. If ψ changes by g∣Bn−1, with g:Zn−1→G, its cochain changes by gπn−1dn=δ(gπn−1), since dn lands in Zn−1 and πn−1 is the identity there. Thus ι descends to a linear map on Ext. If ψdn=hdn for h:Cn−1→G, surjectivity of dn:Cn→Bn−1 gives ψ=h∣Bn−1. The map h∣Zn−1 then represents the required restriction, so [ψ]=0. This proves injectivity.

2.2F1step 1.1

For u:Hn→G, write q:Zn→Hn for the quotient and set φ=uqπn. This kills Bn, since πn is the identity on Zn and q kills Bn. It is a cocycle with evaluation u, so β is onto. The construction is linear in u for a fixed projection. It does not assert that the chosen projection is natural.

3.1step 1.1step 2.1

Every ψdn vanishes on Zn, hence has zero evaluation. Conversely, if a cocycle φ has zero evaluation, then φ(z)=0 for every z∈Zn: the zero map on Hn is zero on every class. Define ψ(dnc)=φ(c). If dnc=dnc′, then c−c′∈Zn, so the definition is independent of the preimage, is linear, and gives φ=ψdn. This proves both containments of im⁡ι=ker⁡β.

3.2step 1.1step 2.1

Let f:C→D be a chain map. It restricts to maps ZjC→ZjD and BjC→BjD commuting with inclusion and quotient, hence induces the contravariant map on the displayed Ext cokernels by precomposition on Bn−1. A restricted map from Zn−1D pulls back to a restricted map from Zn−1C, so this is well-defined. The equality (ψdnD)fn=(ψfn−1∣Bn−1C)dnC proves naturality of ι. On cycles, (φfn)(z)=φ(fnz) proves naturality of β. A coefficient map commutes with every formula by postcomposition. Identity and composition laws follow directly from composition of maps.

4.1F2F4step 1.1step 3.2

For completeness let 0→P1→aP0→qM→0 and 0→Q1→bQ0→rN→0 be length-one projective resolutions, and v:M→N. Projectivity lifts vq to f0:P0→Q0 through r. Since rf0a=0, there is a unique f1:P1→Q1 with bf1=f0a. Any second lift g0 has f0−g0=bh for a unique h:P0→Q1, and injectivity of b gives f1−g1=ha. For ψ:Q1→G, the difference ψf1−ψg1=(ψh)a is zero in the cokernel defining Ext. Thus the induced map is independent of the lift. Composites of lifts lift composites; identity lifts induce identities. Taking M=N and v=1 in both directions yields inverse canonical isomorphisms between the two cokernels. This also proves compatibility with the restricted-resolution maps of step 3.2 and with coefficient maps. For free resolutions the requisite projectivity follows from [F4]; for supplied projective resolutions it is their defining property.

5.1F1F2F4step 2.1step 3.1step 2.2step 3.2step 4.1∎

Steps 2.1, 3.1 and 2.2 give the asserted short exact sequence, and steps 3.2 and 4.1 give its natural interpretation. At n=0, B−1=Z−1=H−1=0, so Ext is zero and evaluation is an isomorphism. For the zero complex or G=0 every displayed map is the unique zero map. For a single nonzero free term in degree n, evaluation is literally the identity on Hom⁡(Cn,G); no boundary term survives. AC is used in [F1] for arbitrary-rank freeness and sections, and in [F4] for free comparison lifts; the quotient and exactness chases introduce no further choices. No injective-derived or balanced Ext theorem has been used.

Depends on

Dependency tree · 2 levels

Sources