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.
The factor-set model agrees with the inhomogeneous cochain model in degree two
Statement
Let be the inhomogeneous cochain groups with differentials
and
Then the normalized factor-set quotient from Second cohomology by factor sets agrees with the degree-two cohomology of this inhomogeneous cochain complex:
Facts & Assumptions
Given: A group and an abelian -module .
Normalized two-cocycles are exactly the functions satisfying the displayed cocycle equation, and normalized two-coboundaries are exactly the functions of the form (Normalized two-cocycle and two-coboundary).
The factor-set model defines as (Second cohomology by factor sets).
Proof
Let satisfy , and put . Substituting into the cocycle equation gives for all , so for every . Substituting gives for all , and then taking yields .
By [F1], a normalized two-cocycle is exactly a normalized function satisfying the displayed cocycle equation, so every normalized two-cocycle lies in .
For an arbitrary one-cochain , one has Hence is normalized if and only if , that is, if and only if is a normalized one-cochain. So the normalized elements of are exactly from [F1].
Let be the constant one-cochain . Then So the cohomologous two-cochain satisfies for every . A direct cancellation shows , hence . Therefore every class in has a normalized representative.
Steps 2.1, 1.2, and 1.3 show that every class in has a normalized representative, and two normalized cocycles represent the same class there exactly when they differ by a normalized two-coboundary. Thus the quotient is naturally the same as .
Combining step 3.1 with [F2] gives
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
3 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)