TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-09

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.

Degree-one inflation–restriction is exact

Statement

For every extension $1 \to N \to G \to Q \to 1$ and left G-module A, the bar-cohomology sequence $0 ⟶ H^{1} (Q, A^{N}) \overset{\inf}{\to} H^{1} (G, A) \overset{res}{\to} H^{1} (N, A)^{Q}$ is exact. This crossed-map proof is choice-free; the derived interpretation retains its inherited comparison convention. No surjectivity of restriction is asserted.

Facts & Assumptions

Given: The extension, A, and the well-defined degree-one maps.

[F1]

The displayed maps are homomorphisms with the stated domains and codomains (Degree-one maps and the quotient action are well-defined).

Proof

1.1

If an inflated c is principal, say $c (π g) = g a - a$ , restriction to N gives $n a = a$ for every n, because c(1)=0. Thus $a \in A^{N}$ and c itself is principal on Q. Inflation is injective. An inflated cocycle restricts to zero on N, so its class belongs to the kernel of restriction.

F1givenalgebra

2.1

Conversely let D restrict to a principal map $n \mapsto n a - a$ . Replace D by $D_{0} = D - δ a$ , so $D_{0} ∣_{N} = 0$ . For n in N, $D_{0} (g n) = D_{0} (g)$ , and $D_{0} (n g) = n D_{0} (g)$ . But $n g = g (g^{- 1} n g)$ , so these equations also give $n D_{0} (g) = D_{0} (g)$ . Thus $D_{0}$ is constant on quotient fibers and takes values in $A^{N}$ . Define c(q) as this unique common value; no representatives need be chosen. For any g,h above q,r the crossed identity yields $c (q r) = c (q) + q c (r)$ . Hence $D_{0} = \inf c$ and [D] lies in its image.

F1step 1.1algebra∎

Depends on

Degree-one maps and the quotient action are well-defined

Used by

Dependency tree · two levels

2 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

Weibel, An Introduction to Homological Algebra, Chapter 6, Sections 6.4–6.8 (standard reference, not scraped)
Dekimpe–Hartl–Wauters, A seven-term exact sequence for the cohomology of a group extension, Sections 2–5 pp.2–11 and Section 10.2 p.21 (standard reference, not scraped)