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.
Extension-theoretic interpretation of the standard five-term exact sequence
Statement
For an extension and an abelian -module , assume the standard low-degree sequence
is exact. Then the transgression detects extension of degree-one classes: for one has exactly when is the restriction of a class in . Under the factor-set classification, the last inflation map is represented by pulling a -extension back along and then pushing it out along the inclusion .
Facts & Assumptions
Given: An extension and an abelian -module .
Restriction and inflation in degree one are the explicit maps defined on cocycles in Restriction, inflation, and the quotient conjugation action on first cohomology.
The degree-one inflation-restriction sequence is exact (Inflation-restriction exact sequence in degree one).
classifies extensions of by (H^2 classifies extensions with fixed abelian kernel action).
The displayed five-term sequence is the standard exact low-degree five-term sequence attached to .
Proof
The first three terms are exactly the degree-one inflation-restriction sequence, so they are exact by [L1], with maps described concretely by [F1].
Under [L2], a class in is an extension of by . The map to first pulls that extension back along , producing an extension of by , and then pushes out along the inclusion . That is the extension-theoretic meaning of the last inflation map in the displayed sequence.
Exactness of [A1] at says Thus exactly when is the restriction of a degree-one class on , which is precisely the asserted extension criterion for the cohomology class.
Steps 1.2 and 1.3 give the two claimed interpretations, while step 1.1 identifies the preceding degree-one maps.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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
- Clara Loh, Group Cohomology, SS 2019 (standard reference, not scraped)
- Caroline Lassueur, Cohomology of Groups, SS 2021 (standard reference, not scraped)