ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-07

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.

ex-a-roof-representing-an-ext-one-class.md

Example

Assume Dependent Choice and supplied projective resolution data on $A b$ , with $U$ below supplied for $Z / 2$ , and set-sized Yoneda extension classes as in [F2]. The nonsplit extension $0 \to Z \overset{2}{\to} Z \to Z / 2 \to 0$ is represented in $D (A b)$ by the roof $Z / 2 [0] \overset{s}{\leftarrow} U \overset{f}{\to} Z [1]$ , where $U = (Z \overset{2}{\to} Z)$ in degrees $- 1, 0$ , $s^{0}$ is reduction modulo two, and $f^{- 1} = 1$ . Its class generates ${Ext}^{1} (Z / 2, Z) ≅ Z / 2$ .

Facts & Assumptions

Given: Assume Dependent Choice and supplied projective resolution data on $A b$ , with $U$ below supplied for $Z / 2$ , and set-sized Yoneda extension classes as in [F2]. The nonsplit extension $0 \to Z \overset{2}{\to} Z \to Z / 2 \to 0$ is represented in $D (A b)$ by the roof $Z / 2 [0] \overset{s}{\leftarrow} U \overset{f}{\to} Z [1]$ , where $U = (Z \overset{2}{\to} Z)$ in degrees $- 1, 0$ , $s^{0}$ is reduction modulo two, and $f^{- 1} = 1$ . Its class generates ${Ext}^{1} (Z / 2, Z) ≅ Z / 2$ .

[F1]

In the projective construction of Ext is hom in the derived category, a degree-one Hom cocycle $f : P \to N [1]$ on a projective resolution $s : P \to M [0]$ represents the derived morphism $Q (f) Q (s)^{- 1}$ after the stated classical-to-cochain sign conversion; in degree one this multiplies the cocycle by $- 1$ .

[F2]

The projective Yoneda-to-Ext comparison sends a short exact extension to the cocycle obtained by lifting its endpoint through a projective resolution (Higher Yoneda Ext agrees with derived Ext).

Verification

1.1

The complex $U$ has $H^{- 1} = 0$ and $H^{0} = Z / 2$ , and $s$ induces the identity on this quotient. The map $f$ is a chain map because the target has only degree $- 1$ . Thus $s$ is a projective resolution of $Z / 2 [0]$ , and [F1] sends the cocycle $f$ to exactly the displayed roof.

F1algebra

2.1

The free resolution $U$ computes Ext: the degree-one Hom quotient is $Z / 2 Z$ , and $f$ is the cocycle $1$ . The lift used in [F2] for the displayed short exact sequence is the identity on the middle copy of $Z$ , so its terminal cocycle is this same $f$ . The degree-one sign conversion in [F1] gives $- f$ , but $f$ and $- f$ differ by the boundary $2 f$ in this Hom quotient. Thus the displayed roof represents the extension class and is its nonzero generator. The extension cannot split because every homomorphism $Z / 2 \to Z$ is zero.

F1F2step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

10.4.7 and 10.7.5, pp. 388, 400 (standard reference, not scraped)