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

Pullback and coefficient pushout realize bar cohomology maps

Statement

Assume AC. Pulling back an abelian-kernel extension along $α : H \to G$ represents $α^{*} : H^{2} (G, A) \to H^{2} (H, A)$ . Pushing it out along a G-module map $u : A \to B$ represents $u_{*} : H^{2} (G, A) \to H^{2} (G, B)$ . These are the abelian-kernel constructions, with the fixed actions. H2 denotes normalized bar cohomology, with its inherited derived interpretation.

Facts & Assumptions

Given: AC and an extension $0 \to A \overset{i}{\to} E \overset{p}{\to} G \to 1$ , a group map alpha and a module map u.

[F1]

An extension is classified by its normalized factor-set class, with section changes adding coboundaries (Bar two-cocycles classify abelian-kernel extensions).

[F2]

AC supplies normalized sections from the nonempty fibers (The Axiom of Choice).

Proof

1.1

The pullback is $P = {(e, h) : p (e) = α (h)} \leq E \times H$ . Its projection to H is onto, its kernel is ${(i (a), 1)}$ , and the conjugation action is the restricted action. Choose a normalized section s of E using AC; $(s (α (h)), h)$ is a section of P. Its factor set is $(h, l) \mapsto f (α (h), α (l))$ . By F1 this represents the bar pullback, including when alpha is not injective or surjective.

F1F2givenalgebra

1.2

Let E act on B through p and form $B ⋊ E$ . The subgroup $S = {(- u (a), i (a)) : a \in A}$ is normal: conjugation by $(b, e)$ sends its a-element to the one indexed by $p (e) a$ , since i(A) acts trivially on B and u is equivariant. Set $E_{u} = (B ⋊ E) / S$ . The map $B \to E_{u}$ , $b \mapsto [(b, 1)]$ , is injective, because intersection with S forces i(a)=1 and a=0. Projection to G is onto, and any kernel element $[(b, i (a))]$ equals $[(b + u (a), 1)]$ . Thus its kernel is exactly B, with the prescribed action.

givenalgebra

2.1

The section $g \mapsto [(0, s (g))]$ has product $[(0, s (g) s (h))] = [(u (f (g, h)), s (g h))]$ , hence factor set u f. It represents the coefficient map by F1. Replacing f by $f + δ c$ replaces the two resulting cocycles by $α^{*} f + δ (α^{*} c)$ and $u f + δ (u c)$ , respectively. Extension equivalences induce the same maps by $[(b, e)] \mapsto [(b, θ (e))]$ and $(e, h) \mapsto (θ (e), h)$ , so both constructions are independent of representatives. No injectivity of the coefficient map on H2 is claimed.

F1step 1.1step 1.2algebra∎

Depends on

Used by

Dependency tree · two levels

6 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

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)